def Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf {n : Nat} (G : SparseGraph n) (tcLevel level : Nat) (root : RefineSt n) (targets : List Nat) (key : Key n) : Prop

A selected native descent ending in a parsed discrete leaf. The key retains every executed refinement code and the terminal sentinel; every child in its witness uses its own actual bounded scratch.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.leaf {n : Nat} {G : SparseGraph n} {tcLevel level : Nat} {st : RefineSt n} {label : Label n} (hd : discreteAt st.ptn level n = true) (hp : Label.ofArray? n st.lab = some label) : HasLeaf G tcLevel level st [] { codes := [st.longcode, codeSentinel], graph := G.relabel label.perm }

theorem Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.step {n : Nat} {G : SparseGraph n} {tcLevel level : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} {tc len o : Nat} {scratch : Scratch} (hc : IsCell st.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (hs : Scratch.Bounded n scratch) (ht : tc = targetcell (Graph.ofGraph G) st.lab st.ptn level tcLevel (-1)) (h : HasLeaf G tcLevel (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + o]! scratch) targets key) : HasLeaf G tcLevel level st (tc :: targets) { codes := st.longcode :: key.codes, graph := key.graph }

Prefixing the literal individualization and refinement preserves the selected target and the complete native leaf key.

theorem Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.nonempty {n : Nat} {G : SparseGraph n} {tcLevel level : Nat} {st : RefineSt n} (hr : RefineSt.Ready G level st) : ∃ (targets : List Nat), ∃ (key : Key n), HasLeaf G tcLevel level st targets key

Every valid native refined state has a selected discrete descendant. The existing depth bound suffices while each chosen child uses fresh bounded scratch as one permissible literal descent witness.

theorem Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.cases {n : Nat} {G : SparseGraph n} {tcLevel level : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} (h : HasLeaf G tcLevel level st targets key) : (∃ (label : Label n), discreteAt st.ptn level n = true ∧ Label.ofArray? n st.lab = some label ∧ targets = [] ∧ key = { codes := [st.longcode, codeSentinel], graph := G.relabel label.perm }) ∨ ∃ (tc : Nat), ∃ (len : Nat), ∃ (o : Nat), ∃ (scratch : Scratch), ∃ (rest : List Nat), ∃ (tail : Key n), IsCell st.ptn level tc len ∧ tc + len ≤ n ∧ 1 < len ∧ o < len ∧ Scratch.Bounded n scratch ∧ tc = targetcell (Graph.ofGraph G) st.lab st.ptn level tcLevel (-1) ∧ HasLeaf G tcLevel (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + o]! scratch) rest tail ∧ targets = tc :: rest ∧ key = { codes := st.longcode :: tail.codes, graph := tail.graph }

A selected leaf occurrence is either the current discrete node or an occurrence below one member of its actual unhinted target.

theorem Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.map {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j) {tcLevel level : Nat} {s t : RefineSt n} {targets : List Nat} {key : Key n} (hs : RefineSt.Ready G level s) (ht : RefineSt.Ready H level t) (he : RefineSt.Equiv (renamingOf p) level s t) (h : HasLeaf G tcLevel level s targets key) : HasLeaf H tcLevel level t targets key

Native descent transport preserves the complete leaf key under isomorphism, including independently allocated scratch at every child.

theorem Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.map_iff {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j) {tcLevel level : Nat} {s t : RefineSt n} {targets : List Nat} {key : Key n} (hs : RefineSt.Ready G level s) (ht : RefineSt.Ready H level t) (he : RefineSt.Equiv (renamingOf p) level s t) : HasLeaf G tcLevel level s targets key ↔ HasLeaf H tcLevel level t targets key

Isomorphic native refined states have exactly the same selected leaf keys and target sequences. The inverse transports every occurrence.

theorem Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.carried {n : Nat} {G : SparseGraph n} {tcLevel level : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} {tc len a b : Nat} {scratch other : Scratch} {gamma : Array Nat} (hr : RefineSt.Ready G level st) (hc : IsCell st.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ha : a < len) (hb' : b < len) (hs : Scratch.Bounded n scratch) (ht : Scratch.Bounded n other) (hcheck : checkAutom (Graph.context G).g gamma = true) (hstab : CellStab st.ptn level st.lab gamma) (hmove : gamma[st.lab[tc + a]!]! = st.lab[tc + b]!) (h : HasLeaf G tcLevel (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + a]! scratch) targets key) : HasLeaf G tcLevel (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + b]! other) targets key

A checked cell stabilizer carrying one chosen vertex to another transports every native leaf below those two literal cached children.