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

Every leaf below a refined state has the same key and target-position sequence. This is stronger than equality of maximal subtree keys.

Equations

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

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

A discrete node has exactly its own leaf key.

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

Uniform target children with a common suffix make their parent uniform, retaining the refinement code and target hint.

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

Each child of a uniform node has the same uniform suffix.

theorem Hex.GraphIso.Nauty.Generation.Uniform.carriers {n : Nat} {ctx : Ctx n} {tcLevel level tc e oGuide : Nat} {rs : RefineSt n} {targets : List Nat} {key : Key n} (hok : IterOk ctx level rs) (hlvl : level < n) (hgsz : ctx.g.size = n) (hcell : (tc, e) ∈ cells rs.ptn level n) (hne : tc < e) (htarget : tc = specTargetcell ctx rs.lab rs.ptn level tcLevel) (hoGuide : oGuide ≤ e - tc) (hcarriers : ∀ (o : Nat), o ≤ e - tc → ∃ (γ : Array Nat), checkAutom ctx.g γ = true ∧ CellStab rs.ptn level rs.lab γ ∧ γ[rs.lab[tc + o]!]! = rs.lab[tc + oGuide]!) (hguide : Uniform ctx tcLevel (level + 1) (childSt ctx level rs tc rs.lab[tc + oGuide]!) targets key) : Uniform ctx tcLevel level rs (tc :: targets) { codes := rs.longcode :: key.codes, rows := key.rows }

Checked cell stabilizers carrying every child to one uniform child make the whole target subtree uniform.

theorem Hex.GraphIso.Nauty.Generation.Uniform.orbit {n k : Nat} {G : Colored n k} {base : List (Fin n)} {rs : RefineSt n} {st : SearchSt n} {tcLevel level tc e oGuide : Nat} {targets : List Nat} {key : Key n} {guide : Fin n} (hok : IterOk { g := rowsOf G } level rs) (hlvl : level < n) (hpath : PathStab { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st) (hlab : st.lab = rs.lab) (hptn : st.ptn = rs.ptn) (hbase : ∀ (b : Fin n), st.fixedpts.mem ↑b = true → b ∈ base) (hcell : (tc, e) ∈ cells rs.ptn level n) (hne : tc < e) (htarget : tc = specTargetcell { g := rowsOf G } rs.lab rs.ptn level tcLevel) (hoGuide : oGuide ≤ e - tc) (hatGuide : rs.lab[tc + oGuide]! = ↑guide) (horbits : ∀ (o : Nat), o ≤ e - tc → ∃ (hv : rs.lab[tc + o]! < n), Aut.Orbit G base guide ⟨rs.lab[tc + o]!, hv⟩) (hguide : Uniform { g := rowsOf G } tcLevel (level + 1) (childSt { g := rowsOf G } level rs tc rs.lab[tc + oGuide]!) targets key) : Uniform { g := rowsOf G } tcLevel level rs (tc :: targets) { codes := rs.longcode :: key.codes, rows := key.rows }

Transitivity on the target cell extends the uniform first child to all children. The carriers need only be true automorphisms fixing the current path; no completeness theorem is used.