def Hex.GraphIso.Nauty.CellsReach {n k : Nat} (G : Colored n k) (lab : Array Nat) : Prop

The simulation-relation clause: lab is cell-content-reachable from the initial labelling relative to the initial partition. Every labelling the search visits satisfies this (individualization and refinement permute within the initial colour classes).

Equations

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

theorem Hex.GraphIso.Nauty.cellsReach_initial {n k : Nat} (G : Colored n k) : CellsReach G (initialPartition G).fst

The initial labelling reaches itself.

theorem Hex.GraphIso.Nauty.isPerm_of_cellsReach {n k : Nat} {G : Colored n k} {lab : Array Nat} (hsz : lab.size = n) (hn0 : 0 < n) (h : CellsReach G lab) : lab.toList.Perm (List.range n)

A reached labelling of full size is a permutation of [0, n): label well-formedness.

theorem Hex.GraphIso.Nauty.cellsReach_lt {n k : Nat} {G : Colored n k} {lab : Array Nat} (h : CellsReach G lab) (i : Nat) (hi : i < n) : lab[i]! < n

Every entry of a reached labelling is a valid vertex.

theorem Hex.GraphIso.Nauty.labelColorSorted_of_cellsReach {n k : Nat} {G : Colored n k} {lab : Array Nat} (hsz : lab.size = n) (h : CellsReach G lab) : labelColorSorted G lab = true

A reached labelling passes labelColorSorted: the transcription output's colours are nondecreasing, the certifyCanon?_isSome residual. The colour at each position matches sortedColorSeq (achieved_position_colors), which is sorted (pairwise_sortedColorSeq).

theorem Hex.GraphIso.Nauty.refine_cellsReach {n k : Nat} {G : Colored n k} {ctx : Ctx n} (hn0 : 0 < n) {lab ptn : Array Nat} {level : Nat} {active : VSet n} {numcells : Nat} (hreach : CellsReach G lab) (hlsz : lab.size = n) (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hcoarse : ∀ (q : Nat), (initPtn n (n + 2) (initialPartition G).snd)[q]! ≤ 1 → ptn[q]! ≤ level) : CellsReach G (refine ctx level lab ptn active numcells).lab

refine preserves CellsReach: it reorders labels within cells of its own (finer) partition, and the initial boundaries persist, so cell-content equivalence transfers to the initial partition.

theorem Hex.GraphIso.Nauty.breakout_cellsPerm {n : Nat} {lab ptn : Array Nat} {level tc len o : Nat} (hcell : IsCell ptn level tc len) (hsize : tc + len ≤ ptn.size) (hlsz : lab.size = ptn.size) (ho : o < len) : cellsPerm ptn level lab (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst

Individualization rotates the target vertex to the front of its cell, a permutation confined to that cell, so it preserves cell-content equivalence on the current partition.

theorem Hex.GraphIso.Nauty.breakout_cellsReach {n k : Nat} {G : Colored n k} {lab ptn : Array Nat} {level tc len o : Nat} (hn0 : 0 < n) (hreach : CellsReach G lab) (hcell : IsCell ptn level tc len) (hsize : tc + len ≤ ptn.size) (hlsz : lab.size = n) (hpsz : ptn.size = n) (ho : o < len) (hend : ptn[ptn.size - 1]! ≤ level) (hcoarse : ∀ (q : Nat), (initPtn n (n + 2) (initialPartition G).snd)[q]! ≤ 1 → ptn[q]! ≤ level) : CellsReach G (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst

breakout preserves CellsReach: individualization permutes within one cell of the current partition, which refines the initial one, so cell-content equivalence coarsens and transfers. The second operation-level preservation lemma.

theorem Hex.GraphIso.Nauty.bcount_succ (ptn : Array Nat) (level m : Nat) : bcount ptn level (m + 1) = bcount ptn level m + if ptn[m]! ≤ level then 1 else 0

theorem Hex.GraphIso.Nauty.bcount_congr {ptn ptn' : Array Nat} {level nn : Nat} : (∀ (q : Nat), q < nn → ptn'[q]! = ptn[q]!) → bcount ptn' level nn = bcount ptn level nn

theorem Hex.GraphIso.Nauty.bcount_set!_open {ptn : Array Nat} {level p : Nat} (hps : p < ptn.size) (hopen : ptn[p]! > level) {nn : Nat} : p < nn → bcount (ptn.set! p level) level nn = bcount ptn level nn + 1

Writing level at an open position adds exactly one boundary.

theorem Hex.GraphIso.Nauty.sum_eq_zero' {l : List Nat} : (∀ (x : Nat), x ∈ l → x = 0) → l.sum = 0

theorem Hex.GraphIso.Nauty.sum_map_indicator {c : Nat} {vs : List Nat} : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) vs → c ∈ vs → (List.map (fun (v : Nat) => if (c == v) = true then 1 else 0) vs).sum = 1

theorem Hex.GraphIso.Nauty.sum_map_countP (counts : List Nat) {vs : List Nat} : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) vs → (∀ (c : Nat), c ∈ counts → c ∈ vs) → (List.map (multOf counts) vs).sum = counts.length

theorem Hex.GraphIso.Nauty.countValues_pairwise (counts : List Nat) : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) (countValues counts)

theorem Hex.GraphIso.Nauty.sum_multOf_countValues (counts : List Nat) : (List.map (multOf counts) (countValues counts)).sum = counts.length

The value window's multiplicities cover the whole cell.

structure Hex.GraphIso.Nauty.FreezeInv {n : Nat} (level nn : Nat) (ptn0 : Array Nat) (nc0 : Nat) (st : RefineSt n) : Prop

Positions closed at level in the entry partition keep their exact values, and the boundary count stays in step with numcells.

• ptnSize : st.ptn.size = ptn0.size
• labPtn : st.lab.size = st.ptn.size
• frozen (q : Nat) : ptn0[q]! ≤ level → st.ptn[q]! = ptn0[q]!
• count : st.numcells + bcount ptn0 level nn = nc0 + bcount st.ptn level nn

theorem Hex.GraphIso.Nauty.FreezeInv.same {n level nn : Nat} {ptn0 : Array Nat} {nc0 : Nat} {st st' : RefineSt n} (h : FreezeInv level nn ptn0 nc0 st) (hp : st'.ptn = st.ptn) (hc : st'.numcells = st.numcells) (hl : st'.lab.size = st.lab.size) : FreezeInv level nn ptn0 nc0 st'

A step that touches neither the partition, the count, nor the labelling size preserves the invariant.

theorem Hex.GraphIso.Nauty.FreezeInv.write {n level nn : Nat} {ptn0 : Array Nat} {nc0 : Nat} {st st' : RefineSt n} {p : Nat} (h : FreezeInv level nn ptn0 nc0 st) (hp : st'.ptn = st.ptn.set! p level) (hc : st'.numcells = st.numcells + 1) (hl : st'.lab.size = st.lab.size) (hpn : p < nn) (hpsz : p < st.ptn.size) (hopen : st.ptn[p]! > level) : FreezeInv level nn ptn0 nc0 st'

One paired write: level at an open in-range position together with one numcells increment.

theorem Hex.GraphIso.Nauty.freezeInv_trivialSplit {n level nn : Nat} {ptn0 : Array Nat} {nc0 : Nat} {st : RefineSt n} {cell1 cell2 : Nat} {c1 c2 : Int} (hinv : FreezeInv level nn ptn0 nc0 st) (hbounds : Int.ofNat cell1 ≤ c2 → c1 ≤ Int.ofNat cell2 → cell1 ≤ c2.toNat ∧ c2.toNat < cell2) (hfresh : ∀ (p : Nat), cell1 ≤ p → p < cell2 → st.ptn[p]! > level) (hb : cell2 < nn) (hsz : cell2 < st.ptn.size) : FreezeInv level nn ptn0 nc0 (trivialSplit level cell1 cell2 c1 c2 st) ∧ ∀ (q : Nat), q < cell1 ∨ cell2 ≤ q → (trivialSplit level cell1 cell2 c1 c2 st).ptn[q]! = st.ptn[q]!

theorem Hex.GraphIso.Nauty.freezeInv_trivialCell {n level nn : Nat} {gRow : VSet n} {ptn0 : Array Nat} {nc0 : Nat} {st : RefineSt n} {cell1 cell2 : Nat} (hinv : FreezeInv level nn ptn0 nc0 st) (hfresh : ∀ (p : Nat), cell1 ≤ p → p < cell2 → st.ptn[p]! > level) (h12 : cell1 ≤ cell2) (hb : cell2 < nn) (hsz : cell2 < st.ptn.size) : FreezeInv level nn ptn0 nc0 (trivialCell level gRow cell1 cell2 st) ∧ ∀ (q : Nat), q < cell1 ∨ cell2 ≤ q → (trivialCell level gRow cell1 cell2 st).ptn[q]! = st.ptn[q]!

theorem Hex.GraphIso.Nauty.nc_windowStep_eq {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : (windowStep level cell1 cell2 v c1 c2 maxcell st).numcells = if c1 = cell1 then st.numcells else st.numcells + 1

theorem Hex.GraphIso.Nauty.windowScan_payload {n level nn cell1 cell2 : Nat} {counts : List Nat} (hb : cell2 < nn) (vs : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : cell1 ≤ c1 → c1 + (List.map (multOf counts) vs).sum = cell2 + 1 → cell2 < st.ptn.size → (∀ (p : Nat), c1 ≤ p → p < cell2 → st.ptn[p]! > level) → ((windowScan level cell1 cell2 counts vs c1 maxcell st).numcells + bcount st.ptn level nn = st.numcells + bcount (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn level nn + if c1 = cell1 ∨ (List.map (multOf counts) vs).sum = 0 then 0 else 1) ∧ (∀ (q : Nat), st.ptn[q]! ≤ level → (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn[q]! = st.ptn[q]!) ∧ (∀ (q : Nat), q < c1 ∨ cell2 ≤ q → (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn[q]! = st.ptn[q]!) ∧ (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn.size = st.ptn.size ∧ (windowScan level cell1 cell2 counts vs c1 maxcell st).lab = st.lab

The window scan's paired writes: each nonempty group except the final one writes one fresh boundary, and each nonempty group except the first counts one new cell, so over a whole cell the two balance.

theorem Hex.GraphIso.Nauty.nc_nontrivialFix {n : Nat} (cell1 : Nat) (st : RefineSt n) : (nontrivialFix cell1 st).numcells = st.numcells

theorem Hex.GraphIso.Nauty.freezeInv_nontrivialCell {n : Nat} {ctx : Ctx n} {level nn : Nat} {workset : VSet n} {ptn0 : Array Nat} {nc0 : Nat} {st : RefineSt n} {cell1 cell2 : Nat} (hinv : FreezeInv level nn ptn0 nc0 st) (hfresh : ∀ (p : Nat), cell1 ≤ p → p < cell2 → st.ptn[p]! > level) (h12 : cell1 ≤ cell2) (hb : cell2 < nn) (hsz : cell2 < st.ptn.size) : FreezeInv level nn ptn0 nc0 (nontrivialCell ctx level workset cell1 cell2 st) ∧ ∀ (q : Nat), q < cell1 ∨ cell2 ≤ q → (nontrivialCell ctx level workset cell1 cell2 st).ptn[q]! = st.ptn[q]!

def Hex.GraphIso.Nauty.CellsFresh {n : Nat} (level nn : Nat) (st : RefineSt n) : List (Nat × Nat) → Prop

The remaining cells of a pass: ordered left to right, in range, with open interiors in the current state.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.CellsFresh level nn st [] = True

theorem Hex.GraphIso.Nauty.cellsFresh_congr {n level nn b0 : Nat} {st st' : RefineSt n} (hagree : ∀ (q : Nat), b0 ≤ q → st'.ptn[q]! = st.ptn[q]!) {cs : List (Nat × Nat)} : (∀ (p : Nat × Nat), p ∈ cs → b0 ≤ p.fst) → CellsFresh level nn st cs → CellsFresh level nn st' cs

theorem Hex.GraphIso.Nauty.cells_go_ge {ptn : Array Nat} {level nn : Nat} (fuel c1 : Nat) (p : Nat × Nat) : p ∈ cells.go ptn level nn fuel c1 → c1 ≤ p.fst

theorem Hex.GraphIso.Nauty.cellsFresh_cells {n level nn : Nat} {st : RefineSt n} (hnn : st.ptn.size = nn) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (fuel c1 : Nat) : CellsFresh level nn st (cells.go st.ptn level nn fuel c1)

theorem Hex.GraphIso.Nauty.freezeInv_refineTrivial_go {n level nn : Nat} {gRow : VSet n} {ptn0 : Array Nat} {nc0 : Nat} (cs : List (Nat × Nat)) (st : RefineSt n) : FreezeInv level nn ptn0 nc0 st → nn ≤ st.ptn.size → CellsFresh level nn st cs → FreezeInv level nn ptn0 nc0 (refineTrivial.go level gRow cs st)

theorem Hex.GraphIso.Nauty.freezeInv_refineNontrivial_go {n : Nat} {ctx : Ctx n} {level nn : Nat} {workset : VSet n} {ptn0 : Array Nat} {nc0 : Nat} (cs : List (Nat × Nat)) (st : RefineSt n) : FreezeInv level nn ptn0 nc0 st → nn ≤ st.ptn.size → CellsFresh level nn st cs → FreezeInv level nn ptn0 nc0 (refineNontrivial.go ctx level workset cs st)

theorem Hex.GraphIso.Nauty.freezeInv_refineStep {n : Nat} {ctx : Ctx n} {level split1 : Nat} {ptn0 : Array Nat} {nc0 : Nat} {st : RefineSt n} (hinv : FreezeInv level n ptn0 nc0 st) (hnn : n = ptn0.size) (hend0 : ptn0[ptn0.size - 1]! ≤ level) : FreezeInv level n ptn0 nc0 (refineStep ctx level split1 st)

theorem Hex.GraphIso.Nauty.freezeInv_refineLoop {n : Nat} {ctx : Ctx n} {level : Nat} {ptn0 : Array Nat} {nc0 : Nat} (hnn : n = ptn0.size) (hend0 : ptn0[ptn0.size - 1]! ≤ level) (fuel : Nat) (st : RefineSt n) : FreezeInv level n ptn0 nc0 st → FreezeInv level n ptn0 nc0 (refineLoop ctx level fuel st)

theorem Hex.GraphIso.Nauty.refine_freezeInv {n : Nat} {ctx : Ctx n} {level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells : Nat} (hnn : n = ptn.size) (hls : lab.size = ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) : FreezeInv level n ptn numcells (refine ctx level lab ptn active numcells)

theorem Hex.GraphIso.Nauty.refine_frozen {n : Nat} {ctx : Ctx n} {level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells : Nat} (hnn : n = ptn.size) (hls : lab.size = ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) {q : Nat} (hq : ptn[q]! ≤ level) : (refine ctx level lab ptn active numcells).ptn[q]! = ptn[q]!

refine keeps every closed position's exact value.

theorem Hex.GraphIso.Nauty.refine_bcount {n : Nat} {ctx : Ctx n} {level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells : Nat} (hnn : n = ptn.size) (hls : lab.size = ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) : (refine ctx level lab ptn active numcells).numcells + bcount ptn level n = numcells + bcount (refine ctx level lab ptn active numcells).ptn level n

refine keeps an accurate cell count accurate.

theorem Hex.GraphIso.Nauty.exists_open_of_bcount_lt {ptn : Array Nat} {level nn : Nat} : bcount ptn level nn < nn → ∃ (q : Nat), q < nn ∧ ptn[q]! > level

A short boundary count exposes an open position.

theorem Hex.GraphIso.Nauty.exists_nontrivial_cell_of_open {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) {q : Nat} (hq : q < nn) (hopen : ptn[q]! > level) : ∃ (p : Nat × Nat), p ∈ cells ptn level nn ∧ p.fst ≠ p.snd

An open position lies in a nontrivial cell.

theorem Hex.GraphIso.Nauty.targetcell_open {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level tcLevel : Nat} {hint : Int} (_hn1 : 1 ≤ level) (hsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hex : ∃ (p : Nat × Nat), p ∈ cells ptn level n ∧ p.fst ≠ p.snd) : ∃ (p : Nat × Nat), p ∈ cells ptn level n ∧ p.fst ≠ p.snd ∧ targetcell ctx lab ptn level tcLevel hint = p.fst

The executable target cell of a live state is an in-range nontrivial cell start, whatever the hint.

theorem Hex.GraphIso.Nauty.maketargetcell_open {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level tcLevel : Nat} {hint : Int} (hn1 : 1 ≤ level) (hsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hlive : bcount ptn level n < n) : ∃ (tc : Nat), ∃ (len : Nat), maketargetcell ctx lab ptn level tcLevel hint = (tc, worksetOf n lab tc (tc + len - 1), len) ∧ IsCell ptn level tc len ∧ 2 ≤ len ∧ tc + len ≤ n

The executable maketargetcell of a live state: an open nontrivial cell with its exact extent and contents.

theorem Hex.GraphIso.Nauty.countP_eq_sum_map {α : Type} (p : α → Bool) (l : List α) : List.countP p l = (List.map (fun (x : α) => if p x = true then 1 else 0) l).sum

theorem Hex.GraphIso.Nauty.countP_mem_range {nn : Nat} {l : List Nat} : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) l → (∀ (e : Nat), e ∈ l → e < nn) → List.countP (fun (q : Nat) => decide (q ∈ l)) (List.range nn) = l.length

theorem Hex.GraphIso.Nauty.bcount_initPtn {n k : Nat} (G : Colored n k) : bcount (initPtn n (n + 2) (initialPartition G).snd) 1 n = (initialPartition G).snd.length

The initial partition's boundary count is its cell count.

structure Hex.GraphIso.Nauty.SearchOk {n k : Nat} (G : Colored n k) (level numcells : Nat) (st : SearchSt n) : Prop

The per-node invariant of the transcribed search at level with claimed cell count numcells.

• labSize : st.lab.size = n
• ptnSize : st.ptn.size = n
• reach : CellsReach G st.lab
• init1 (q : Nat) : (initPtn n (n + 2) (initialPartition G).snd)[q]! ≤ 1 → st.ptn[q]! ≤ 1
• vals (q : Nat) : q < n → st.ptn[q]! ≤ level ∨ st.ptn[q]! = n + 2
• count : numcells = bcount st.ptn level n
• bc : level ≤ bcount st.ptn level n
• canon : st.canonlab = Array.replicate n 0 ∨ st.canonlab.size = n ∧ CellsReach G st.canonlab

structure Hex.GraphIso.Nauty.SearchOut {n k : Nat} (G : Colored n k) (B lev : Nat) (st st' : SearchSt n) : Prop

What a quartet call leaves behind: sizes kept, reachability kept, the partition preserved exactly wherever it is (or becomes) closed at B, the labelling permuted only within cells of the entry partition at lev, and canonlab kept or installed reached.

• labSize : st'.lab.size = st.lab.size
• ptnSize : st'.ptn.size = st.ptn.size
• reach : CellsReach G st'.lab
• low (q : Nat) : st.ptn[q]! ≤ B ∨ st'.ptn[q]! ≤ B → st'.ptn[q]! = st.ptn[q]!
• perm : cellsPerm st.ptn lev st.lab st'.lab
• firstStore : st'.firstlab = st.firstlab ∨ st'.firstlab.size = st.lab.size ∧ cellsPerm st.ptn lev st.lab st'.firstlab
• canonStore : st'.canonlab = st.canonlab ∨ st'.canonlab.size = st.lab.size ∧ cellsPerm st.ptn lev st.lab st'.canonlab
• canon : st'.canonlab = st.canonlab ∨ st'.canonlab.size = n ∧ CellsReach G st'.canonlab

theorem Hex.GraphIso.Nauty.SearchOut.refl {n k : Nat} (G : Colored n k) (B lev : Nat) {st : SearchSt n} (hreach : CellsReach G st.lab) : SearchOut G B lev st st

theorem Hex.GraphIso.Nauty.SearchOut.atSingleton {n k : Nat} {G : Colored n k} {B lev : Nat} {st st' : SearchSt n} (h : SearchOut G B lev st st') {a : Nat} (hc : IsCell st.ptn lev a 1) : st'.lab[a]! = st.lab[a]!

A quartet call cannot move the entry of a singleton cell.

theorem Hex.GraphIso.Nauty.SearchOut.firstAtSingleton {n k : Nat} {G : Colored n k} {B lev : Nat} {st st' : SearchSt n} (h : SearchOut G B lev st st') {a : Nat} (hc : IsCell st.ptn lev a 1) (hold : st.firstlab[a]! = st.lab[a]!) : st'.firstlab[a]! = st.lab[a]!

A stored first leaf keeps the entry of a singleton cell, provided the incoming stored leaf already has that entry.

theorem Hex.GraphIso.Nauty.SearchOut.canonAtSingleton {n k : Nat} {G : Colored n k} {B lev : Nat} {st st' : SearchSt n} (h : SearchOut G B lev st st') {a : Nat} (hc : IsCell st.ptn lev a 1) (hold : st.canonlab[a]! = st.lab[a]!) : st'.canonlab[a]! = st.lab[a]!

A stored canonical leaf keeps the entry of a singleton cell, provided the incoming stored leaf already has that entry.

theorem Hex.GraphIso.Nauty.bcount_eq_of_low {ptn ptn' : Array Nat} {lev : Nat} (h : ∀ (q : Nat), ptn[q]! ≤ lev ∨ ptn'[q]! ≤ lev → ptn'[q]! = ptn[q]!) (nn : Nat) : bcount ptn' lev nn = bcount ptn lev nn

The exact-preservation clause fixes the boundary count.

theorem Hex.GraphIso.Nauty.isCell_of_low {ptn ptn' : Array Nat} {lev a len : Nat} (h : ∀ (q : Nat), ptn[q]! ≤ lev ∨ ptn'[q]! ≤ lev → ptn'[q]! = ptn[q]!) (hc : IsCell ptn lev a len) : IsCell ptn' lev a len

The exact-preservation clause keeps cells intact.

theorem Hex.GraphIso.Nauty.cellEnd_eq_of_low {ptn ptn' : Array Nat} {lev : Nat} (hsize : ptn'.size = ptn.size) (h : ∀ (q : Nat), ptn[q]! ≤ lev ∨ ptn'[q]! ≤ lev → ptn'[q]! = ptn[q]!) (i : Nat) : cellEnd ptn' lev i = cellEnd ptn lev i

The exact-preservation clause identifies every cell-end walk when the partition arrays have the same size.

theorem Hex.GraphIso.Nauty.cells_eq_of_low {ptn ptn' : Array Nat} {lev nn : Nat} (hsize : ptn'.size = ptn.size) (h : ∀ (q : Nat), ptn[q]! ≤ lev ∨ ptn'[q]! ≤ lev → ptn'[q]! = ptn[q]!) : cells ptn' lev nn = cells ptn lev nn

The exact-preservation clause identifies the ordered coarse-cell list when the partition arrays have the same size.

theorem Hex.GraphIso.Nauty.bcount_succ_of_vals {ptn : Array Nat} {lev nn : Nat} (hvals : ∀ (q : Nat), q < nn → ptn[q]! ≤ lev ∨ ptn[q]! = nn + 2) (hlev : lev + 1 < nn + 2) : bcount ptn (lev + 1) nn = bcount ptn lev nn

Under the level dichotomy, the boundary count is level-blind one step up.

theorem Hex.GraphIso.Nauty.SearchOut.trans {n k : Nat} {G : Colored n k} {B : Nat} {st1 st2 st3 : SearchSt n} (h12 : SearchOut G B B st1 st2) (h23 : SearchOut G B B st2 st3) : SearchOut G B B st1 st3

Compose two call effects at matching bounds.

theorem Hex.GraphIso.Nauty.SearchOut.mono {n k : Nat} {G : Colored n k} {B B' lev : Nat} {st st' : SearchSt n} (h : SearchOut G B lev st st') (hB : B' ≤ B) : SearchOut G B' lev st st'

Weaken the preservation bound.

theorem Hex.GraphIso.Nauty.mem_ne_empty {n : Nat} {s : VSet n} {v : Nat} (h : s.mem v = true) : s ≠ VSet.empty

theorem Hex.GraphIso.Nauty.mem_segN_iff {lab : Array Nat} {tc len v : Nat} : v ∈ segN lab tc len ↔ ∃ (o : Nat), o < len ∧ lab[tc + o]! = v

theorem Hex.GraphIso.Nauty.breakout_ptn {n : Nat} (lab ptn : Array Nat) (lev tc tv : Nat) : (breakout n lab ptn lev tc tv).snd.fst = ptn.set! tc lev

theorem Hex.GraphIso.Nauty.breakout_lab_size {n : Nat} (lab ptn : Array Nat) (lev tc tv : Nat) : (breakout n lab ptn lev tc tv).fst.size = lab.size

theorem Hex.GraphIso.Nauty.searchOk_end {n k : Nat} {G : Colored n k} {level numcells : Nat} {st : SearchSt n} (hn0 : 0 < n) (hok : SearchOk G level numcells st) (h1 : 1 ≤ level) : st.ptn[st.ptn.size - 1]! ≤ level

The end of the partition stays closed: position n - 1 is an initial boundary.

theorem Hex.GraphIso.Nauty.searchOk_of_out {n k : Nat} {G : Colored n k} {level numcells : Nat} {st st' : SearchSt n} (hok : SearchOk G level numcells st) (h1 : 1 ≤ level) (hout : SearchOut G level level st st') (hvals : ∀ (q : Nat), q < n → st'.ptn[q]! ≤ level ∨ st'.ptn[q]! = n + 2) : SearchOk G level numcells st'

The invariant survives an iteration whose net effect preserves the closed positions, provided the final partition satisfies the level dichotomy (which recover restores unconditionally).

theorem Hex.GraphIso.Nauty.breakout_searchOk {n k : Nat} {G : Colored n k} {level numcells tc len o : Nat} {st st' : SearchSt n} (hn0 : 0 < n) (hok : SearchOk G level numcells st) (h1 : 1 ≤ level) (hcell : IsCell st.ptn level tc len) (hlen2 : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hl : st'.lab = (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst) (hp : st'.ptn = st.ptn.set! tc (level + 1)) (hc : st'.canonlab = st.canonlab) : SearchOk G (level + 1) (numcells + 1) st'

Individualizing a target-cell vertex yields the child invariant one level down with one more cell.

theorem Hex.GraphIso.Nauty.breakout_child_out {n k : Nat} {G : Colored n k} {level numcells tc len o : Nat} {st stC stD : SearchSt n} (hn0 : 0 < n) (hok : SearchOk G level numcells st) (h1 : 1 ≤ level) (hcell : IsCell st.ptn level tc len) (hlen2 : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hCout : SearchOut G level (level + 1) stC stD) (hl : stC.lab = (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst) (hp : stC.ptn = st.ptn.set! tc (level + 1)) (hf : stC.firstlab = st.firstlab) (hc : stC.canonlab = st.canonlab) : SearchOut G level level st stD

The effect of individualization followed by a child call, in the parent loop's frame.

theorem Hex.GraphIso.Nauty.SearchOut.congr {n k : Nat} {G : Colored n k} {B lev : Nat} {st st' st'' : SearchSt n} (h : SearchOut G B lev st st') (hl : st''.lab = st'.lab) (hp : st''.ptn = st'.ptn) (hf : st''.firstlab = st'.firstlab) (hc : st''.canonlab = st'.canonlab) : SearchOut G B lev st st''

theorem Hex.GraphIso.Nauty.searchOut_id {n k : Nat} {G : Colored n k} (B lev : Nat) {stX : SearchSt n} {labR : Array Nat} (hl : stX.lab = labR) (hreach : CellsReach G labR) : SearchOut G B lev stX stX

theorem Hex.GraphIso.Nauty.match_option_or {α γ : Type} {P : γ → Prop} (x : Option α) (f : α → γ) (g : γ) (hf : ∀ (a : α), P (f a)) (hg : P g) : P (match x with | some a => f a | none => g)

theorem Hex.GraphIso.Nauty.refine_searchOk {n k : Nat} {G : Colored n k} {ctx : Ctx n} (hn0 : 0 < n) {level numcells : Nat} {st st2 : SearchSt n} (hok : SearchOk G level numcells st) (h1 : 1 ≤ level) (hl : st2.lab = (refine ctx level st.lab st.ptn st.active numcells).lab) (hp : st2.ptn = (refine ctx level st.lab st.ptn st.active numcells).ptn) (hcanon : st2.canonlab = st.canonlab ∨ st2.canonlab.size = n ∧ CellsReach G st2.canonlab) : SearchOk G level (refine ctx level st.lab st.ptn st.active numcells).numcells st2

The invariant after refine, for any state carrying the refined labelling and partition.

theorem Hex.GraphIso.Nauty.refine_loop_out {n k : Nat} {G : Colored n k} {ctx : Ctx n} (hn0 : 0 < n) {level numcells : Nat} {st STL stX : SearchSt n} (hok : SearchOk G level numcells st) (h1 : 1 ≤ level) (hl : STL.lab = (refine ctx level st.lab st.ptn st.active numcells).lab) (hp : STL.ptn = (refine ctx level st.lab st.ptn st.active numcells).ptn) (hfirst : STL.firstlab = st.firstlab ∨ STL.firstlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab STL.firstlab) (hcanonStore : STL.canonlab = st.canonlab ∨ STL.canonlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab STL.canonlab) (hcanon : STL.canonlab = st.canonlab ∨ STL.canonlab.size = n ∧ CellsReach G STL.canonlab) (hXout : SearchOut G level level STL stX) : SearchOut G (level - 1) level st stX

Compose the refine step with the rest of a node's work.