theorem Hex.GraphIso.Nauty.breakout_segN_target {n : Nat} {lab ptn : Array Nat} {level tc len tv : Nat} (hw : ∃ (k : Nat), tc ≤ k ∧ k < tc + len ∧ k < lab.size ∧ lab[k]! = tv) (hsz : tc + len ≤ lab.size) : segN (breakout n lab ptn level tc tv).fst tc len = tv :: (segN lab tc len).erase tv

The rotated target window.

theorem Hex.GraphIso.Nauty.breakout_getElem!_front {n : Nat} {lab ptn : Array Nat} {level tc len tv : Nat} (hw : ∃ (k : Nat), tc ≤ k ∧ k < tc + len ∧ k < lab.size ∧ lab[k]! = tv) (hlen : 0 < len) (hsz : tc + len ≤ lab.size) : (breakout n lab ptn level tc tv).fst[tc]! = tv

The individualized vertex lands at the front of its cell.

theorem Hex.GraphIso.Nauty.breakout_segN_rest {n : Nat} {lab ptn : Array Nat} {level tc len tv : Nat} (hw : ∃ (k : Nat), tc ≤ k ∧ k < tc + len ∧ k < lab.size ∧ lab[k]! = tv) (hlen : 0 < len) (hsz : tc + len ≤ lab.size) : segN (breakout n lab ptn level tc tv).fst (tc + 1) (len - 1) = (segN lab tc len).erase tv

The remainder window after the rotation: the cell with its first occurrence of the value erased.

theorem Hex.GraphIso.Nauty.breakout_segN_outside {n : Nat} {lab ptn : Array Nat} {level tc len tv a alen : Nat} (hw : ∃ (k : Nat), tc ≤ k ∧ k < tc + len ∧ k < lab.size ∧ lab[k]! = tv) (hout : a + alen ≤ tc ∨ tc + len ≤ a) : segN (breakout n lab ptn level tc tv).fst a alen = segN lab a alen

Windows outside the rotated cell are untouched.

theorem Hex.GraphIso.Nauty.breakout_cellsPerm_map {n : Nat} {σ : Renaming n} {labV labU ptn : Array Nat} {level tc e oV oU : Nat} (hpsz : ptn.size = n) (hVsz : labV.size = n) (hUsz : labU.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hcp : cellsPerm ptn level labV (Array.map σ.toFun labU)) (hcell : (tc, e) ∈ cells ptn level n) (hne : tc < e) (hoV : oV ≤ e - tc) (hoU : oU ≤ e - tc) (hvv : labV[tc + oV]! = σ.toFun labU[tc + oU]!) : cellsPerm (ptn.set! tc (level + 1)) (level + 1) (breakout n labV ptn (level + 1) tc labV[tc + oV]!).fst (Array.map σ.toFun (breakout n labU ptn (level + 1) tc labU[tc + oU]!).fst)

Individualizing corresponding vertices preserves the renamed cell equivalence on the split partition.

theorem Hex.GraphIso.Nauty.labOk_map {n : Nat} (σ : Renaming n) {lab : Array Nat} (h : LabOk lab n) : LabOk (Array.map σ.toFun lab) n

A renaming keeps every entry a vertex.

theorem Hex.GraphIso.Nauty.labInj_map {n : Nat} (σ : Renaming n) {lab : Array Nat} (h : LabInj lab n) (hsz : lab.size = n) : LabInj (Array.map σ.toFun lab) n

A renaming keeps a labelling injective.

theorem Hex.GraphIso.Nauty.labOk_of_perm {lab lab' : Array Nat} {nn : Nat} (hp : (segN lab' 0 nn).Perm (segN lab 0 nn)) (h : LabOk lab nn) (hsz : lab.size = nn) (hsz' : lab'.size = nn) : LabOk lab' nn

A whole-segment permutation keeps every entry a vertex.

def Hex.GraphIso.Nauty.childSt {n : Nat} (ctx : Ctx n) (level : Nat) (st : RefineSt n) (tc tv : Nat) : RefineSt n

One individualize-and-refine step of the search subtree.

Equations

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

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

The facts carried at every node of the subtree: state well-formedness, an injective labelling, and the partition-value dichotomy (closed at the level or the open marker).

• ok : StOk n level st
• inj : LabInj st.lab n
• vals (q : Nat) : q < n → st.ptn[q]! ≤ level ∨ st.ptn[q]! = n + 2
• lvl : level ≤ n

theorem Hex.GraphIso.Nauty.IterOk.valsWeak {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level : Nat} (h : IterOk ctx level st) (q : Nat) : q < n → st.ptn[q]! ≤ level ∨ level + 1 < st.ptn[q]!

The weak value dichotomy the classification lemmas consume.

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

The node invariant survives one subtree step.

theorem Hex.GraphIso.Nauty.iterOk_of_stPerm {n : Nat} {ctx : Ctx n} {σ : Renaming n} {V U : RefineSt n} {level : Nat} (hU : IterOk ctx level U) (hsp : StPerm level V (mapSt σ U)) : IterOk ctx level V

The node invariant transports across the renamed cell equivalence.

theorem Hex.GraphIso.Nauty.stPerm_child {n : Nat} {ctx : Ctx n} {σ : Renaming n} {V U : RefineSt n} {level tc e oV oU : Nat} (hg : RowsMap σ ctx.g ctx.g) (hsp : StPerm level V (mapSt σ U)) (hU : IterOk ctx level U) (hcell : (tc, e) ∈ cells U.ptn level n) (hne : tc < e) (hoV : oV ≤ e - tc) (hoU : oU ≤ e - tc) (hvv : V.lab[tc + oV]! = σ.toFun U.lab[tc + oU]!) : StPerm (level + 1) (childSt ctx level V tc V.lab[tc + oV]!) (mapSt σ (childSt ctx level U tc U.lab[tc + oU]!))

Cell equivalence up to a row-preserving renaming survives individualizing corresponding vertices and refining.

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

A descent: a sequence of individualize-and-refine steps, each at a nontrivial cell of the current partition.

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

theorem Hex.GraphIso.Nauty.descends_iterOk {n : Nat} {ctx : Ctx n} {level level' : Nat} {st st' : RefineSt n} (h : Descends ctx level st level' st') (hok : IterOk ctx level st) : IterOk ctx level' st'

The node invariant holds along every descent.