theorem Hex.GraphIso.Nauty.recover_lab (n inf level : Nat) (st : SearchSt n) : (recover n inf level st).lab = st.lab

recover never changes the current labelling.

theorem Hex.GraphIso.Nauty.recover_ptn (n inf level : Nat) (st : SearchSt n) (q : Nat) : (recover n inf level st).ptn[q]! = if q < n ∧ st.ptn[q]! > level then inf else st.ptn[q]!

recover reopens exactly the entries above its receiving level.

theorem Hex.GraphIso.Nauty.recover_ptn_size (n inf level : Nat) (st : SearchSt n) : (recover n inf level st).ptn.size = st.ptn.size

Reopening a partition preserves its array size.

theorem Hex.GraphIso.Nauty.recover_out {n k : Nat} {G : Colored n k} {level : Nat} {st : SearchSt n} (hlev : level + 1 < n + 2) (hreach : CellsReach G st.lab) : SearchOut G level level st (recover n (n + 2) level st)

One recover step satisfies the exit contract at its own level.

theorem Hex.GraphIso.Nauty.processnode_searchOk {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level nc pnl pnn : Nat} {st4 st5 : SearchSt n} (hok4 : SearchOk G level nc st4) (hl : st5.lab = (processnode ctx pnl pnn st4).snd.lab) (hp : st5.ptn = (processnode ctx pnl pnn st4).snd.ptn) (hc : st5.canonlab = (processnode ctx pnl pnn st4).snd.canonlab) : SearchOk G level nc st5

processnode preserves the node invariant, installing at most a reached labelling.

theorem Hex.GraphIso.Nauty.canonlab_or_of {n k : Nat} {G : Colored n k} {ctx : Ctx n} {pnl pnn : Nat} {st4 stO : SearchSt n} {cl rl : Array Nat} (hO : stO.canonlab = (processnode ctx pnl pnn st4).snd.canonlab) (hc : st4.canonlab = cl) (hl : st4.lab = rl) (hsz : rl.size = n) (hre : CellsReach G rl) : stO.canonlab = cl ∨ stO.canonlab.size = n ∧ CellsReach G stO.canonlab

Transport the processnode canonlab dichotomy along projection equations, keyed on the output state.

theorem Hex.GraphIso.Nauty.firstPathNode_ok {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf : Nat) (hinf : inf = n + 2) (tcLevel : Nat) (hn0 : 0 < n) (fuel level numcells : Nat) (st : SearchSt n) (hok : SearchOk G level numcells st) (h1 : 1 ≤ level) (hfuel : n + 1 ≤ level + fuel) : SearchOut G (level - 1) level st (firstPathNode ctx inf tcLevel fuel level numcells st).snd ∧ ((∀ (v : Nat), v < n → st.orbits[v]! = v) → (firstPathNode ctx inf tcLevel fuel level numcells st).snd.canonlab.size = n ∧ CellsReach G (firstPathNode ctx inf tcLevel fuel level numcells st).snd.canonlab)

theorem Hex.GraphIso.Nauty.firstChildLoop_ok {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf : Nat) (hinf : inf = n + 2) (tcLevel : Nat) (hn0 : 0 < n) (fuel cfuel level numcells tc tv1 : Nat) (tv? : Option Nat) (tcell0 : VSet n) (index0 : Nat) (st0 : SearchSt n) (len : Nat) (hok : SearchOk G level numcells st0) (h1 : 1 ≤ level) (hfuel : n + 1 ≤ level + 1 + fuel) (hcell : tcell0 ≠ VSet.empty → IsCell st0.ptn level tc len ∧ 2 ≤ len ∧ tc + len ≤ n) (hmem : ∀ (v : Nat), tcell0.mem v = true → v ∈ segN st0.lab tc len) (htv : ∀ (v : Nat), tv? = some v → tcell0.mem v = true) : SearchOut G level level st0 (firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell0 index0 st0).snd.snd ∧ ((∀ (v : Nat), v < n → st0.orbits[v]! = v) → tv? = some tv1 → 1 ≤ cfuel → (firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell0 index0 st0).snd.snd.canonlab.size = n ∧ CellsReach G (firstChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell0 index0 st0).snd.snd.canonlab)

theorem Hex.GraphIso.Nauty.otherNode_ok {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf : Nat) (hinf : inf = n + 2) (tcLevel : Nat) (hn0 : 0 < n) (fuel level numcells : Nat) (st : SearchSt n) (hok : SearchOk G level numcells st) (h1 : 1 ≤ level) (hfuel : n + 1 ≤ level + fuel) : SearchOut G (level - 1) level st (otherNode ctx inf tcLevel fuel level numcells st).snd

theorem Hex.GraphIso.Nauty.otherChildLoop_ok {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf : Nat) (hinf : inf = n + 2) (tcLevel : Nat) (hn0 : 0 < n) (fuel cfuel level numcells tc tv1 : Nat) (tv? : Option Nat) (tcell0 : VSet n) (st0 : SearchSt n) (len : Nat) (hok : SearchOk G level numcells st0) (h1 : 1 ≤ level) (hfuel : n + 1 ≤ level + 1 + fuel) (hcell : tcell0 ≠ VSet.empty → IsCell st0.ptn level tc len ∧ 2 ≤ len ∧ tc + len ≤ n) (hmem : ∀ (v : Nat), tcell0.mem v = true → v ∈ segN st0.lab tc len) (htv : ∀ (v : Nat), tv? = some v → tcell0.mem v = true) : SearchOut G level level st0 (otherChildLoop ctx inf tcLevel fuel cfuel level numcells tc tv1 tv? tcell0 st0).snd

theorem Hex.GraphIso.Nauty.root_searchOk {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : SearchOk G 1 (initialPartition G).snd.length { lab := (initialPartition G).fst, ptn := initPtn n (n + 2) (initialPartition G).snd, active := initActive n (initialPartition G).snd, orbits := Array.ofFn fun (i : Fin n) => ↑i, firstcode := Array.replicate (n + 2) 0, canoncode := Array.replicate (n + 2) 0, firsttc := Array.replicate (n + 2) (-1), firstlab := Array.replicate n 0, canonlab := Array.replicate n 0, canong := Array.replicate n VSet.empty, numorbits := n }

The root state satisfies the search invariant.

theorem Hex.GraphIso.Nauty.canonlab_size {n k : Nat} (G : Colored n k) : (runColored G).canonlab.size = n

The transcribed search's canonical labelling has full size.

theorem Hex.GraphIso.Nauty.canonlab_cellsReach {n k : Nat} (G : Colored n k) : CellsReach G (runColored G).canonlab

The transcribed search's canonical labelling is reached: it fills every cell of the initial partition with that cell's own vertices. This is the simulation clause the rest of the correctness argument shares, and it supplies the transcription-side residuals of certifyCanon?_isSome.

theorem Hex.GraphIso.Nauty.labelColorSorted_canonlab {n k : Nat} (G : Colored n k) : labelColorSorted G (runColored G).canonlab = true

The transcribed search's canonical labelling passes the colour monotonicity check: one of the two transcription-side residuals of certifyCanon?_isSome.

theorem Hex.GraphIso.Nauty.canonlab_perm_range {n k : Nat} (G : Colored n k) : (runColored G).canonlab.toList.Perm (List.range n)

The transcribed search's canonical labelling is a permutation of the vertices: the label well-formedness residual of certifyCanon?_isSome.