theorem Hex.GraphIso.Nauty.cells_length_eq_bcount {ptn : Array Nat} {level nn : Nat} (hps : ptn.size = nn) (hend : ptn[ptn.size - 1]! ≤ level) : (cells ptn level nn).length = bcount ptn level nn

The number of cells is the number of boundaries.

def Hex.GraphIso.Nauty.SmallShape (n level : Nat) (ptn : Array Nat) : Prop

The first-branch shape: every cell is a singleton, a pair, or the unique triple.

Equations

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

def Hex.GraphIso.Nauty.NodeShape (n level : Nat) (ptn : Array Nat) : Prop

The two shapes a passing cheapautom guard admits: the first-branch shape, or a defect of at most four. Both yield flip data at every cell, and both descend through individualization, which is why the invariant carries the disjunction rather than either disjunct. A defect-four node need not have the first-branch shape: the four-vertex empty graph's root is a single cell of size four.

Equations

• Hex.GraphIso.Nauty.NodeShape n level ptn = (Hex.GraphIso.Nauty.SmallShape n level ptn ∨ n - (Hex.GraphIso.Nauty.cells ptn level n).length ≤ 4)

structure Hex.GraphIso.Nauty.SubtreeOk {n : Nat} (ctx : Ctx n) (level : Nat) (st : RefineSt n) : Prop

The facts every deviation below a cheapautom node consumes, carried at each node of the subtree.

• it : IterOk ctx level st
• eqt : Equitable ctx level st.lab st.ptn
• acc : bcount st.ptn level n = st.numcells
• shape : NodeShape n level st.ptn

theorem Hex.GraphIso.Nauty.childSt_cell_parent {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc e o : Nat} (hIt : IterOk ctx level st) (hlvl : level < n) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) (f : Nat × Nat) : f ∈ cells (childSt ctx level st tc st.lab[tc + o]!).ptn (level + 1) n → ∃ (q : Nat × Nat), q ∈ cells (st.ptn.set! tc (level + 1)) (level + 1) n ∧ q.fst ≤ f.fst ∧ f.snd ≤ q.snd

Every cell of the child partition sits inside a cell of the split partition: refinement only adds boundaries.

theorem Hex.GraphIso.Nauty.smallShape_child {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc e o : Nat} (hIt : IterOk ctx level st) (hlvl : level < n) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) (hsmall : SmallShape n level st.ptn) : SmallShape n (level + 1) (childSt ctx level st tc st.lab[tc + o]!).ptn

The first-branch shape descends to the child: sizes only shrink under containment, and a child triple fills the unique parent triple's window exactly.

theorem Hex.GraphIso.Nauty.nodeShape_child {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc e o : Nat} (hIt : IterOk ctx level st) (hlvl : level < n) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) (hsh : NodeShape n level st.ptn) : NodeShape n (level + 1) (childSt ctx level st tc st.lab[tc + o]!).ptn

The node shape descends: the first-branch shape by containment, and a defect of at most four because individualization splits a cell while the vertex count stays fixed, so the cell count strictly grows.

theorem Hex.GraphIso.Nauty.refined_child {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc e o : Nat} (hit : IterOk ctx level st) (heqt : Equitable ctx level st.lab st.ptn) (hcount : bcount st.ptn level n = st.numcells) (hlvl : level < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) : have child := childSt ctx level st tc st.lab[tc + o]!; IterOk ctx (level + 1) child ∧ Equitable ctx (level + 1) child.lab child.ptn ∧ bcount child.ptn (level + 1) n = child.numcells ∧ st.numcells < child.numcells

Individualization and refinement preserve the refined-state invariants and strictly increase the number of cells. No small-cell shape is needed.

theorem Hex.GraphIso.Nauty.subtreeOk_child {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc e o : Nat} (h : SubtreeOk ctx level st) (hlvl : level < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) : SubtreeOk ctx (level + 1) (childSt ctx level st tc st.lab[tc + o]!)

The node invariant descends through one subtree step.

inductive Hex.GraphIso.Nauty.DescPath {n : Nat} (ctx : Ctx n) : Nat → RefineSt n → List (Nat × Nat) → Nat → RefineSt n → Prop

A descent recording its target-and-offset path.

• refl {n : Nat} {ctx : Ctx n} (level : Nat) (st : RefineSt n) : DescPath ctx level st [] level st
• step {n : Nat} {ctx : Ctx n} {level level' : Nat} {st st' : RefineSt n} {path : List (Nat × Nat)} (tc e o : Nat) (hlvl : level < n) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) (htail : DescPath ctx (level + 1) (childSt ctx level st tc st.lab[tc + o]!) path level' st') : DescPath ctx level st ((tc, o) :: path) level' st'

theorem Hex.GraphIso.Nauty.DescPath.descends {n : Nat} {ctx : Ctx n} {level level' : Nat} {st st' : RefineSt n} {p : List (Nat × Nat)} (h : DescPath ctx level st p level' st') : Descends ctx level st level' st'

Forgetting the path gives a plain descent.

theorem Hex.GraphIso.Nauty.descPath_nil {n : Nat} {ctx : Ctx n} {level level' : Nat} {st st' : RefineSt n} (h : DescPath ctx level st [] level' st') : level' = level ∧ st' = st

An empty path is the trivial descent.

theorem Hex.GraphIso.Nauty.descPath_transport {n : Nat} {ctx : Ctx n} {σ : Renaming n} (hg : RowsMap σ ctx.g ctx.g) {level level' : Nat} {p : List (Nat × Nat)} {U U' V : RefineSt n} : DescPath ctx level U p level' U' → IterOk ctx level U → StPerm level V (mapSt σ U) → ∃ (V' : RefineSt n), ∃ (q : List (Nat × Nat)), DescPath ctx level V q level' V' ∧ List.map Prod.fst q = List.map Prod.fst p ∧ StPerm level' V' (mapSt σ U')

The path-preserving bisimulation: a descent below one state mirrors below any renamed-equivalent state along the same target cells.

theorem Hex.GraphIso.Nauty.descPath_leafRows {n : Nat} {ctx : Ctx n} {σ : Renaming n} (hg : RowsMap σ ctx.g ctx.g) {level level' : Nat} {p : List (Nat × Nat)} {U U' V : RefineSt n} (h : DescPath ctx level U p level' U') (hU : IterOk ctx level U) (hsp : StPerm level V (mapSt σ U)) (hdisc : ∀ (q : Nat), q < n → U'.ptn[q]! ≤ level') : ∃ (V' : RefineSt n), ∃ (q : List (Nat × Nat)), DescPath ctx level V q level' V' ∧ List.map Prod.fst q = List.map Prod.fst p ∧ leafRows ctx V'.lab = leafRows ctx U'.lab ∧ V'.ptn = U'.ptn

The path-preserving leaf collapse: a descent to a discrete state mirrors along the same target cells with equal leaf rows and the same final partition.

theorem Hex.GraphIso.Nauty.descPath_deviation_self {n : Nat} {ctx : Ctx n} {σ : Renaming n} {st : RefineSt n} {level tc e oU oV level' : Nat} {U' : RefineSt n} {p : List (Nat × Nat)} (hIt : IterOk ctx level st) (hlvl : level < n) (hg : RowsMap σ ctx.g ctx.g) (hsp : StPerm level st (mapSt σ st)) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hoU : oU ≤ e - tc) (hoV : oV ≤ e - tc) (hvv : st.lab[tc + oV]! = σ.toFun st.lab[tc + oU]!) (hdesc : DescPath ctx (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) p level' U') (hdisc : ∀ (q : Nat), q < n → U'.ptn[q]! ≤ level') : ∃ (V' : RefineSt n), ∃ (q : List (Nat × Nat)), DescPath ctx (level + 1) (childSt ctx level st tc st.lab[tc + oV]!) q level' V' ∧ List.map Prod.fst q = List.map Prod.fst p ∧ leafRows ctx V'.lab = leafRows ctx U'.lab ∧ V'.ptn = U'.ptn

The path-preserving single-deviation door: a self-symmetry of the node carrying one child's individualized vertex to another's mirrors any discrete descent below the first child along the same target cells.

theorem Hex.GraphIso.Nauty.stabilizer_transitive {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc te oU oV : Nat} (hS : SubtreeOk ctx level st) (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hcell : (tc, te) ∈ cells st.ptn level n) (hne : tc < te) (hoU : oU ≤ te - tc) (hoV : oV ≤ te - tc) (hone : oU ≠ oV) : ∃ (σ : Renaming n), RowsMap σ ctx.g ctx.g ∧ StPerm level st (mapSt σ st) ∧ st.lab[tc + oV]! = σ.toFun st.lab[tc + oU]!

Any two distinct members of a cell are related by an automorphism that preserves every cell of the node's partition.

theorem Hex.GraphIso.Nauty.descPath_leafRows_all {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (tcs : List Nat) {level : Nat} {st : RefineSt n} {p₁ p₂ : List (Nat × Nat)} {level₁ level₂ : Nat} {U V : RefineSt n} : SubtreeOk ctx level st → DescPath ctx level st p₁ level₁ U → List.map Prod.fst p₁ = tcs → (∀ (q : Nat), q < n → U.ptn[q]! ≤ level₁) → DescPath ctx level st p₂ level₂ V → List.map Prod.fst p₂ = tcs → (∀ (q : Nat), q < n → V.ptn[q]! ≤ level₂) → level₂ = level₁ ∧ leafRows ctx V.lab = leafRows ctx U.lab

Two discrete descents below a cheapautom node with the same target-cell path have equal final levels and leaf rows.

theorem Hex.GraphIso.Nauty.childSt_eq_search_step {n : Nat} {ctx : Ctx n} (r : RefineSt n) (level tc tv : Nat) : refine ctx (level + 1) (breakout n r.lab r.ptn (level + 1) tc tv).fst (breakout n r.lab r.ptn (level + 1) tc tv).snd.fst (breakout n r.lab r.ptn (level + 1) tc tv).snd.snd (r.numcells + 1) = childSt ctx level r tc tv

The search's child loops perform breakout at the parent and then the child node's refine on the returned labelling, split partition, and singleton active set. That composite is childSt of the parent's post-refine state.

theorem Hex.GraphIso.Nauty.maketargetcell_mem {n : Nat} {ctx : Ctx n} {r : RefineSt n} {level tcLevel : Nat} {hint : Int} {tcPos size tv : Nat} {cellSet : VSet n} (hn1 : 1 ≤ level) (hsz : r.ptn.size = n) (hend : r.ptn[r.ptn.size - 1]! ≤ level) (hlive : bcount r.ptn level n < n) (hmk : maketargetcell ctx r.lab r.ptn level tcLevel hint = (tcPos, cellSet, size)) (htv : cellSet.mem tv = true) : ∃ (e : Nat), ∃ (o : Nat), (tcPos, e) ∈ cells r.ptn level n ∧ tcPos < e ∧ o ≤ e - tcPos ∧ r.lab[tcPos + o]! = tv

A surviving target-cell vertex is a window member: any vertex of the cell set maketargetcell returns sits at some offset of the target cell, in the shape a DescPath step consumes.

theorem Hex.GraphIso.Nauty.cheapautom_shape_or_exotic {n : Nat} {ptn : Array Nat} {level : Nat} (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hch : cheapautom ptn level n = true) : SmallShape n level ptn ∨ n - (cells ptn level n).length ≤ 4

A passing guard gives the first-branch shape or the exotic defect-at-most-four configuration: a cell of size four or five, or two triples. The defect-four flip analogues discharge the second disjunct.

theorem Hex.GraphIso.Nauty.subtreeOk_of_cheapautom {n : Nat} {ctx : Ctx n} {r : RefineSt n} {level : Nat} (hIt : IterOk ctx level r) (heqt : Equitable ctx level r.lab r.ptn) (hacc : bcount r.ptn level n = r.numcells) (hch : cheapautom r.ptn level n = true) : SubtreeOk ctx level r

The node invariant at a guard-passing node. The guard's two branches are exactly the invariant's two shapes, so nothing is left over: a defect-four node keeps its own shape rather than being forced into the first-branch one, which it need not have.

theorem Hex.GraphIso.Nauty.leafRows_eq_of_descPaths {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) {r : RefineSt n} {level : Nat} (hS : SubtreeOk ctx level r) {p₁ p₂ : List (Nat × Nat)} {level₁ level₂ : Nat} {U V : RefineSt n} (hU : DescPath ctx level r p₁ level₁ U) (hV : DescPath ctx level r p₂ level₂ V) (htcs : List.map Prod.fst p₂ = List.map Prod.fst p₁) (hUd : ∀ (q : Nat), q < n → U.ptn[q]! ≤ level₁) (hVd : ∀ (q : Nat), q < n → V.ptn[q]! ≤ level₂) : leafRows ctx V.lab = leafRows ctx U.lab

The tie's central consequence: two discrete same-target descents below a first-branch node end with equal leaf rows. The run-level bookkeeping (gcaFirst, eqlevFirst, firsttc) supplies the two descents with the same target path; this theorem turns them into the rows equality the admission exits consume.

theorem Hex.GraphIso.Nauty.checkAutom_scatter_of_descPaths {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) {r : RefineSt n} {level : Nat} (hS : SubtreeOk ctx level r) {p₁ p₂ : List (Nat × Nat)} {level₁ level₂ : Nat} {U V : RefineSt n} (hU : DescPath ctx level r p₁ level₁ U) (hV : DescPath ctx level r p₂ level₂ V) (htcs : List.map Prod.fst p₂ = List.map Prod.fst p₁) (hUd : ∀ (q : Nat), q < n → U.ptn[q]! ≤ level₁) (hVd : ∀ (q : Nat), q < n → V.ptn[q]! ≤ level₂) {γ : Array Nat} (hγsz : γ.size = n) (hsc : ∀ (i : Nat), i < n → γ[U.lab[i]!]! = V.lab[i]!) : checkAutom ctx.g γ = true

The code-1 admission is a checked automorphism: the scatter of the second descent's leaf labelling over the first's passes checkAutom, with no isautom scan.