theorem Hex.GraphIso.Nauty.breakout_go_shift {tv : Nat} (fuel : Nat) (lab : Array Nat) (i prev k : Nat) : (∀ (m : Nat), m < k → lab[i + m]! ≠ tv) → lab[i + k]! = tv → k < fuel → i + k < lab.size → ∀ (q : Nat), (breakout.go tv fuel lab i prev)[q]! = if q < i then lab[q]! else if q = i then prev else if q ≤ i + k then lab[q - 1]! else lab[q]!

The positional effect of individualization's rotation: the target vertex moves to the front of its cell and the displaced prefix shifts one place right.

theorem Hex.GraphIso.Nauty.mem_single {n tc v : Nat} (htc : tc < n) : (VSet.empty.insert tc).mem v = decide (v = tc)

Membership in a singleton.

theorem Hex.GraphIso.Nauty.cellEnd_congr_within {ptn : Array Nat} {level : Nat} {ptn' : Array Nat} {level' : Nat} (hsz : ptn'.size = ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (fuel j : Nat) : ptn.size ≤ fuel + j → j < ptn.size → (∀ (q : Nat), j ≤ q → q ≤ cellEnd ptn level j → (ptn'[q]! > level' ↔ ptn[q]! > level)) → cellEnd ptn' level' j = cellEnd ptn level j

Cell-end computations agree between two partitions that agree in openness along the walked run.

theorem Hex.GraphIso.Nauty.cellEnd_closed {ptn : Array Nat} {level : Nat} (hend : ptn[ptn.size - 1]! ≤ level) {i : Nat} (hi : i < ptn.size) : ptn[cellEnd ptn level i]! ≤ level

The end of a cell walk is closed.

theorem Hex.GraphIso.Nauty.cellEnd_lt_start {ptn : Array Nat} {level tc c : Nat} (hc : c < tc) (htcs : ptn[tc - 1]! ≤ level) : cellEnd ptn level c < tc

A start left of another start closes its cell before it.

theorem Hex.GraphIso.Nauty.target_open {n : Nat} {ptn : Array Nat} {level tc e : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hcell : (tc, e) ∈ cells ptn level n) (q : Nat) : tc ≤ q → q < e → ptn[q]! > level

The target cell's interior is open.

theorem Hex.GraphIso.Nauty.target_end_closed {n : Nat} {ptn : Array Nat} {level tc e : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hcell : (tc, e) ∈ cells ptn level n) : ptn[e]! ≤ level

The target cell's end is closed.

theorem Hex.GraphIso.Nauty.target_end_lt {n : Nat} {ptn : Array Nat} {level tc e : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hcell : (tc, e) ∈ cells ptn level n) : e < n

The target cell's end is in range.

theorem Hex.GraphIso.Nauty.child_cells_singleton {n : Nat} {ptn : Array Nat} {level tc e : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hcell : (tc, e) ∈ cells ptn level n) : (tc, tc) ∈ cells (ptn.set! tc (level + 1)) (level + 1) n

The split-off singleton is a cell of the child partition.

theorem Hex.GraphIso.Nauty.child_cells_rest {n : Nat} {ptn : Array Nat} {level tc e : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hcell : (tc, e) ∈ cells ptn level n) (hne : tc < e) : (tc + 1, e) ∈ cells (ptn.set! tc (level + 1)) (level + 1) n

The remainder is a cell of the child partition.

theorem Hex.GraphIso.Nauty.child_cells_old {n : Nat} {ptn : Array Nat} {level tc e : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hcell : (tc, e) ∈ cells ptn level n) (hne : tc < e) {c ce : Nat} (hmem : (c, ce) ∈ cells ptn level n) (hcne : c ≠ tc) : (c, ce) ∈ cells (ptn.set! tc (level + 1)) (level + 1) n

A parent cell away from the target survives into the child partition.

theorem Hex.GraphIso.Nauty.child_cells_cases {n : Nat} {ptn : Array Nat} {level tc e : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hcell : (tc, e) ∈ cells ptn level n) (hne : tc < e) {p : Nat × Nat} (hp : p ∈ cells (ptn.set! tc (level + 1)) (level + 1) n) : p = (tc, tc) ∨ p = (tc + 1, e) ∨ p ∈ cells ptn level n ∧ p.fst ≠ tc

Every cell of the child partition is the singleton, the remainder, or a parent cell away from the target.

theorem Hex.GraphIso.Nauty.breakout_lab_at {n : Nat} {lab ptn : Array Nat} {level tc o : Nat} (hinj : LabInj lab lab.size) (hto : tc + o < lab.size) (q : Nat) : (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst[q]! = if q < tc then lab[q]! else if q = tc then lab[tc + o]! else if q ≤ tc + o then lab[q - 1]! else lab[q]!

The rotated labelling positionally, at an injectively unique target vertex.

theorem Hex.GraphIso.Nauty.labInj_breakout {n : Nat} {lab ptn : Array Nat} {level tc o : Nat} (hinj : LabInj lab lab.size) (hto : tc + o < lab.size) : LabInj (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst lab.size

The rotated labelling stays injective.

theorem Hex.GraphIso.Nauty.worksetOf_breakout_full {n : Nat} {lab ptn : Array Nat} {level tc e o : Nat} (hinj : LabInj lab lab.size) (hto : tc + o < lab.size) (hoe : o ≤ e - tc) (hte : tc ≤ e) : worksetOf n (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst tc e = worksetOf n lab tc e

The full target window's vertex set survives the rotation.

theorem Hex.GraphIso.Nauty.worksetOf_breakout_outside {n : Nat} {lab ptn : Array Nat} {level tc o a b : Nat} (hinj : LabInj lab lab.size) (hto : tc + o < lab.size) (hout : b < tc ∨ tc + o < a) : worksetOf n (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst a b = worksetOf n lab a b

Vertex sets of windows away from the rotation are untouched.

theorem Hex.GraphIso.Nauty.activeUnion_breakout {n : Nat} {lab ptn : Array Nat} {level tc e o numcells : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hcell : (tc, e) ∈ cells ptn level n) (hne : tc < e) : activeUnion (level + 1) { lab := (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst, ptn := ptn.set! tc (level + 1), active := VSet.empty.insert tc, numcells := numcells + 1, hint := 0, maxpos := 0, longcode := numcells + 1 } = worksetOf n (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst tc tc

The active union of the child entry state is the split-off singleton's vertex.

theorem Hex.GraphIso.Nauty.saturated_breakout {n : Nat} {lab ptn : Array Nat} {level tc e o numcells : Nat} (hlsz : lab.size = n) (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hinj : LabInj lab n) (hcell : (tc, e) ∈ cells ptn level n) (hne : tc < e) (ho : o ≤ e - tc) : Saturated (level + 1) { lab := (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst, ptn := ptn.set! tc (level + 1), active := VSet.empty.insert tc, numcells := numcells + 1, hint := 0, maxpos := 0, longcode := numcells + 1 } (worksetOf n (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst tc tc)

The singleton's vertex saturates every child cell: it is the whole splitter set of the singleton and misses every other cell.

theorem Hex.GraphIso.Nauty.certInv_breakout {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level tc e o numcells : Nat} (hlsz : lab.size = n) (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hinj : LabInj lab n) (hcell : (tc, e) ∈ cells ptn level n) (hne : tc < e) (ho : o ≤ e - tc) (hE : Equitable ctx level lab ptn) : CertInv ctx (level + 1) { lab := (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst, ptn := ptn.set! tc (level + 1), active := VSet.empty.insert tc, numcells := numcells + 1, hint := 0, maxpos := 0, longcode := numcells + 1 }

The certificate invariant of the child entry state: the parent's equitability seeds every certificate, with the split-off singleton as the one active cell.

theorem Hex.GraphIso.Nauty.bcount_breakout_eq {ptn : Array Nat} {level tc nn : Nat} (hvals : ∀ (q : Nat), q < nn → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (htc : ptn[tc]! > level) (htcs : tc < ptn.size) (m : Nat) : m ≤ nn → bcount (ptn.set! tc (level + 1)) (level + 1) m = bcount ptn level m + if tc < m then 1 else 0

Splitting one open position advances the boundary count by exactly one at the next level.

theorem Hex.GraphIso.Nauty.equitable_breakout {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level tc e o numcells : Nat} (hlsz : lab.size = n) (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hlab : LabOk lab n) (hinj : LabInj lab n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hE : Equitable ctx level lab ptn) (hcell : (tc, e) ∈ cells ptn level n) (hne : tc < e) (ho : o ≤ e - tc) (hacc : bcount ptn level n = numcells) : Equitable ctx (level + 1) (refine ctx (level + 1) (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst (ptn.set! tc (level + 1)) (VSet.empty.insert tc) (numcells + 1)).lab (refine ctx (level + 1) (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst (ptn.set! tc (level + 1)) (VSet.empty.insert tc) (numcells + 1)).ptn

The descent theorem: individualizing any vertex of a nontrivial cell of an equitable partition and refining with the singleton active yields an equitable partition at the next level.

def Hex.GraphIso.Nauty.renamingOfFlip (f : Nat → Nat) (n : Nat) (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) : Renaming n

A bounded involution, extended by the identity beyond the vertex range, as a renaming.

Equations

• Hex.GraphIso.Nauty.renamingOfFlip f n hfb hinvol = { toFun := fun (v : Nat) => if v < n then f v else v, inj := ⋯, maps := ⋯ }

theorem Hex.GraphIso.Nauty.renamingOfFlip_at {f : Nat → Nat} {n : Nat} (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) {v : Nat} (hv : v < n) : (renamingOfFlip f n hfb hinvol).toFun v = f v

The extended flip agrees with the flip on vertices.

theorem Hex.GraphIso.Nauty.renamingOfFlip_invol {f : Nat → Nat} {n : Nat} (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) {v : Nat} (hv : v < n) : (renamingOfFlip f n hfb hinvol).toFun ((renamingOfFlip f n hfb hinvol).toFun v) = v

The involution of the flip extends to the renaming.

theorem Hex.GraphIso.Nauty.rowsMap_of_flip_rows {n : Nat} {ctx : Ctx n} {f : Nat → Nat} (hgsz : ctx.g.size = n) (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) (hrows : ∀ (v : Nat), v < n → ctx.g[f v]! = VSet.image f ctx.g[v]!) : RowsMap (renamingOfFlip f n hfb hinvol) ctx.g ctx.g

A row-preserving flip names a rows map of the graph onto itself: the packaging of flip_rows's conclusion that refine_map consumes.

theorem Hex.GraphIso.Nauty.getElem!_oob {arr : Array Nat} {q : Nat} (h : arr.size ≤ q) : arr[q]! = 0

Reads beyond the array bound default.

theorem Hex.GraphIso.Nauty.mem_cells_of_isCell {ptn : Array Nat} {level nn a len : Nat} (hnn : nn ≤ ptn.size) (hpe : ptn[ptn.size - 1]! ≤ level) (h : IsCell ptn level a len) (ha : a < nn) (hlen : a + len ≤ ptn.size) : (a, a + len - 1) ∈ cells ptn level nn

An in-range maximal run is a cell of the partition list.

theorem Hex.GraphIso.Nauty.isCell_oob {ptn : Array Nat} {level a len : Nat} (h : IsCell ptn level a len) (ha : ptn.size ≤ a) : len = 1

A maximal run beyond the array bound is a singleton.

theorem Hex.GraphIso.Nauty.isCell_no_cross {ptn : Array Nat} {level a len : Nat} (hpe : ptn[ptn.size - 1]! ≤ level) (h : IsCell ptn level a len) (ha : a < ptn.size) : a + len ≤ ptn.size

No maximal run crosses the array bound.

theorem Hex.GraphIso.Nauty.labOk_breakout {n : Nat} {lab ptn : Array Nat} {level tc o n' : Nat} (hinj : LabInj lab lab.size) (hto : tc + o < lab.size) (hlab : LabOk lab n') : LabOk (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst n'

The rotated labelling keeps every entry a vertex.

theorem Hex.GraphIso.Nauty.segN_map {arr : Array Nat} {g : Nat → Nat} {lo len : Nat} (h : lo + len ≤ arr.size) : segN (Array.map g arr) lo len = List.map g (segN arr lo len)

Segments of a mapped array are mapped segments.

theorem Hex.GraphIso.Nauty.array_eq_of_getElem! {a b : Array Nat} (hsz : a.size = b.size) (h : ∀ (q : Nat), q < a.size → a[q]! = b[q]!) : a = b

Arrays with equal sizes and equal defaulted reads are equal.

theorem Hex.GraphIso.Nauty.stPerm_lab_eq {n level : Nat} {st st' : RefineSt n} (h : StPerm level st st') (hdisc : ∀ (q : Nat), q < st.ptn.size → st.ptn[q]! ≤ level) (hsz : st.lab.size = st.ptn.size) : st'.lab = st.lab

At a discrete partition, cell-content agreement is pointwise agreement: the labellings of a StPerm pair coincide.