def Hex.GraphIso.Nauty.Generation.HasLeaf {n : Nat} (ctx : Ctx n) (tcLevel level : Nat) (st : RefineSt n) (targets : List Nat) (key : Key n) : Prop

A specific leaf key occurs below a refined state, following the specification's target cells. Both the key and the target-position sequence are retained, so the occurrence can justify the executable reference hints independently of whether the key is the maximum of the subtree.

Equations

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

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.leaf {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st : RefineSt n} (hdisc : ∀ (q : Nat), q < n → st.ptn[q]! ≤ level) : HasLeaf ctx tcLevel level st [] { codes := [st.longcode, codeSentinel], rows := leafRows ctx st.lab }

A discrete state supplies its own leaf.

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.step {n : Nat} {ctx : Ctx n} {tcLevel level tc e o : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} (hlvl : level < n) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) (htarget : tc = specTargetcell ctx st.lab st.ptn level tcLevel) (h : HasLeaf ctx tcLevel (level + 1) (childSt ctx level st tc st.lab[tc + o]!) targets key) : HasLeaf ctx tcLevel level st (tc :: targets) { codes := st.longcode :: key.codes, rows := key.rows }

A child occurrence supplies the corresponding parent occurrence.

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.cases {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} (h : HasLeaf ctx tcLevel level st targets key) : (∀ (q : Nat), q < n → st.ptn[q]! ≤ level) ∧ targets = [] ∧ key = { codes := [st.longcode, codeSentinel], rows := leafRows ctx st.lab } ∨ ∃ (tc : Nat), ∃ (e : Nat), ∃ (o : Nat), ∃ (rest : List Nat), ∃ (tail : Key n), level < n ∧ (tc, e) ∈ cells st.ptn level n ∧ tc < e ∧ o ≤ e - tc ∧ tc = specTargetcell ctx st.lab st.ptn level tcLevel ∧ HasLeaf ctx tcLevel (level + 1) (childSt ctx level st tc st.lab[tc + o]!) rest tail ∧ targets = tc :: rest ∧ key = { codes := st.longcode :: tail.codes, rows := tail.rows }

An occurring key comes from this discrete state or from one child of the specified target cell.

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.transport {n : Nat} {ctx : Ctx n} {σ : Renaming n} (hg : RowsMap σ ctx.g ctx.g) {tcLevel level : Nat} {U V : RefineSt n} {targets : List Nat} {key : Key n} (hU : IterOk ctx level U) (hsp : StPerm level V (mapSt σ U)) (h : HasLeaf ctx tcLevel level U targets key) : HasLeaf ctx tcLevel level V targets key

Leaf occurrence transports through a row-preserving renaming and cell equivalence. In particular, this applies to implicit pruning carriers without requiring them to be recorded generators.

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.carried {n : Nat} {ctx : Ctx n} {tcLevel level tc e oU oV : Nat} {st : RefineSt n} {γ : Array Nat} {targets : List Nat} {key : Key n} (hok : IterOk ctx level st) (hlvl : level < n) (hgsz : ctx.g.size = n) (hcheck : checkAutom ctx.g γ = true) (hstab : CellStab st.ptn level st.lab γ) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hoU : oU ≤ e - tc) (hoV : oV ≤ e - tc) (hmap : γ[st.lab[tc + oU]!]! = st.lab[tc + oV]!) (h : HasLeaf ctx tcLevel (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) targets key) : HasLeaf ctx tcLevel (level + 1) (childSt ctx level st tc st.lab[tc + oV]!) targets key

A checked carrier between two children preserves occurrence of every specific leaf key, not only equality of the maximal child keys.

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.carried_iff {n : Nat} {ctx : Ctx n} {tcLevel level tc e oU oV : Nat} {st : RefineSt n} {γ : Array Nat} {targets : List Nat} {key : Key n} (hok : IterOk ctx level st) (hlvl : level < n) (hgsz : ctx.g.size = n) (hcheck : checkAutom ctx.g γ = true) (hstab : CellStab st.ptn level st.lab γ) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hoU : oU ≤ e - tc) (hoV : oV ≤ e - tc) (hmap : γ[st.lab[tc + oU]!]! = st.lab[tc + oV]!) : HasLeaf ctx tcLevel (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) targets key ↔ HasLeaf ctx tcLevel (level + 1) (childSt ctx level st tc st.lab[tc + oV]!) targets key

A checked automorphism identifies the sets of leaf keys below the two children it relates. The reverse carrier is a forward word in the same permutation, using finite permutation cycles.

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.head {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} (h : HasLeaf ctx tcLevel level st targets key) : ∃ (tail : List Nat), key.codes = st.longcode :: tail

The first code of every occurring leaf is the current refinement code, even when another leaf has a larger key.

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.discrete {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} (hok : IterOk ctx level st) (hdisc : ∀ (q : Nat), q < n → st.ptn[q]! ≤ level) (h : HasLeaf ctx tcLevel level st targets key) : targets = [] ∧ key = { codes := [st.longcode, codeSentinel], rows := leafRows ctx st.lab }

A discrete node cannot hide a deeper matching leaf.