def Hex.GraphIso.Nauty.incKey {n : Nat} (ctx : Ctx n) (bs : List Nat) (canonlab : Array Nat) : Key n

The incumbent's key: the ghost code list with the sentinel stamped, and the stored best leaf's rows.

Equations

• Hex.GraphIso.Nauty.incKey ctx bs canonlab = { codes := bs ++ [Hex.GraphIso.Nauty.codeSentinel], rows := Hex.GraphIso.Nauty.leafRows ctx canonlab }

def Hex.GraphIso.Nauty.pathLeafKey {n : Nat} (ctx : Ctx n) (cs : List Nat) (lab : Array Nat) : Key n

A leaf key of the current path.

Equations

• Hex.GraphIso.Nauty.pathLeafKey ctx cs lab = { codes := cs ++ [Hex.GraphIso.Nauty.codeSentinel], rows := Hex.GraphIso.Nauty.leafRows ctx lab }

theorem Hex.GraphIso.Nauty.codeInv_tied_le {nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 0) : cs.length ≤ bs.length

Under full agreement the path is never deeper than the incumbent.

theorem Hex.GraphIso.Nauty.tied_short_keyCmp_gt {n nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 0) (hshort : cs.length < bs.length) (r1 r2 : List (VSet n)) : keyCmp { codes := cs ++ [codeSentinel], rows := r1 } { codes := bs ++ [codeSentinel], rows := r2 } = Ordering.gt

A code-tied leaf strictly above the incumbent's depth compares above it: the leaf's sentinel meets a real incumbent code.

theorem Hex.GraphIso.Nauty.tied_full_keyCmp {n nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 0) (hlen : cs.length = bs.length) (r1 r2 : List (VSet n)) : keyCmp { codes := cs ++ [codeSentinel], rows := r1 } { codes := bs ++ [codeSentinel], rows := r2 } = listCmp VSet.rowCmp r1 r2

A code-tied leaf at the incumbent's depth hands the comparison to the rows.

theorem Hex.GraphIso.Nauty.frozen_lt_keyCmp {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {lab canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) : keyCmp (pathLeafKey ctx cs lab) (incKey ctx bs canonlab) = Ordering.lt

The downward-frozen verdict at a leaf, in incumbent-key form.

theorem Hex.GraphIso.Nauty.frozen_gt_keyCmp {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {lab canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 1) : keyCmp (pathLeafKey ctx cs lab) (incKey ctx bs canonlab) = Ordering.gt

The upward-frozen verdict at a leaf, in incumbent-key form.

def Hex.GraphIso.Nauty.pruneReturn (noncheaplevel allsamelevel : Nat) (eqlevCanon : Int) : Int

The unwind level of the shared prune tail.

Equations

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

theorem Hex.GraphIso.Nauty.CodeCmpInv.eqlev_nonneg {nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon compCanon : Int} (h : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon compCanon) : 0 ≤ eqlevCanon

A faithful comparison machine records its agreement or divergence at a genuine path level.

theorem Hex.GraphIso.Nauty.pruneReturn_split {noncheaplevel allsamelevel : Nat} {eqlevCanon : Int} (heqlev : 0 ≤ eqlevCanon) : Int.ofNat eqlevCanon.toNat ≤ pruneReturn noncheaplevel allsamelevel eqlevCanon ∨ pruneReturn noncheaplevel allsamelevel eqlevCanon = Int.ofNat noncheaplevel - 1

The shared prune tail either returns no lower than the frozen code divergence or jumps to the level immediately above the saved cheap-cell boundary. These are the two logically different early-return modes.

theorem Hex.GraphIso.Nauty.pruneReturn_lt {noncheaplevel allsamelevel : Nat} {eqlevCanon : Int} : pruneReturn noncheaplevel allsamelevel eqlevCanon < Int.ofNat noncheaplevel

The shared prune tail always returns below its positive saved cheap-cell boundary.

theorem Hex.GraphIso.Nauty.pruneReturn_nonneg {noncheaplevel allsamelevel : Nat} {eqlevCanon : Int} (hpositive : 0 < noncheaplevel) (heqlev : 0 ≤ eqlevCanon) : 0 ≤ pruneReturn noncheaplevel allsamelevel eqlevCanon

A nonnegative comparison depth and positive saved boundary make the shared prune return a genuine natural-number level.

theorem Hex.GraphIso.Nauty.processnode_fast {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) : (processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ∧ (processnode ctx level numcells st).snd.compCanon = st.compCanon ∧ (processnode ctx level numcells st).snd.eqlevCanon = st.eqlevCanon ∧ (processnode ctx level numcells st).snd.canoncode = st.canoncode ∧ (processnode ctx level numcells st).snd.canonlevel = st.canonlevel ∧ (processnode ctx level numcells st).snd.canonlab = st.canonlab ∧ (processnode ctx level numcells st).snd.canong = st.canong ∧ (processnode ctx level numcells st).snd.samerows = st.samerows

The frozen-downward fast arm: the comparison state is untouched and the shared prune tail decides the unwind level.

theorem Hex.GraphIso.Nauty.processnode_fast_short {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) : (processnode ctx level numcells st).snd.needshortprune = if level ≠ st.noncheaplevel ∧ pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ≠ Int.ofNat st.gcaFirst then true else st.needshortprune

The frozen-downward arm raises a short-prune request exactly when it admits an implicit pair and does not return to the first-path guide.

theorem Hex.GraphIso.Nauty.processnode_fast_short_ne {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) (hclear : st.needshortprune = false) (hshort : (processnode ctx level numcells st).snd.needshortprune = true) : level ≠ st.noncheaplevel

A fresh short-prune request in the frozen-downward arm proves that the implicit pair was actually admitted below the saved boundary.

theorem Hex.GraphIso.Nauty.processnode_shortInstall {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hlt : level < st.canonlevel) : (processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat level) ∧ (processnode ctx level numcells st).snd.compCanon = 0 ∧ (processnode ctx level numcells st).snd.eqlevCanon = Int.ofNat level ∧ (processnode ctx level numcells st).snd.canoncode = st.canoncode.set! (level + 1) codeSentinel ∧ (processnode ctx level numcells st).snd.canonlevel = level ∧ (processnode ctx level numcells st).snd.canonlab = st.lab ∧ (processnode ctx level numcells st).snd.canong = st.canong ∧ (processnode ctx level numcells st).snd.samerows = 0

The short-leaf install: a code-tied leaf strictly above the incumbent's depth installs itself with no row comparison.

theorem Hex.GraphIso.Nauty.processnode_upInstall {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 1) : (processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat level) ∧ (processnode ctx level numcells st).snd.compCanon = 0 ∧ (processnode ctx level numcells st).snd.eqlevCanon = Int.ofNat level ∧ (processnode ctx level numcells st).snd.canoncode = st.canoncode.set! (level + 1) codeSentinel ∧ (processnode ctx level numcells st).snd.canonlevel = level ∧ (processnode ctx level numcells st).snd.canonlab = st.lab ∧ (processnode ctx level numcells st).snd.canong = st.canong ∧ (processnode ctx level numcells st).snd.samerows = 0

The upward-frozen install: a leaf reached with compCanon = 1 installs itself directly.

theorem Hex.GraphIso.Nauty.processnode_rowInstall {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (hgt : 0 < (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst) : (processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat level) ∧ (processnode ctx level numcells st).snd.compCanon = 0 ∧ (processnode ctx level numcells st).snd.eqlevCanon = Int.ofNat level ∧ (processnode ctx level numcells st).snd.canoncode = st.canoncode.set! (level + 1) codeSentinel ∧ (processnode ctx level numcells st).snd.canonlevel = level ∧ (processnode ctx level numcells st).snd.canonlab = st.lab ∧ (processnode ctx level numcells st).snd.canong = updatecan ctx st.canong st.canonlab st.samerows ∧ (processnode ctx level numcells st).snd.samerows = (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).snd

The row-decided install: a code-tied leaf at the incumbent's depth whose rows compare above installs itself.

theorem Hex.GraphIso.Nauty.processnode_rowReject {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (hlt : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst < 0) : (processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ∧ (processnode ctx level numcells st).snd.compCanon = (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst ∧ (processnode ctx level numcells st).snd.eqlevCanon = st.eqlevCanon ∧ (processnode ctx level numcells st).snd.canoncode = st.canoncode ∧ (processnode ctx level numcells st).snd.canonlevel = st.canonlevel ∧ (processnode ctx level numcells st).snd.canonlab = st.canonlab ∧ (processnode ctx level numcells st).snd.canong = updatecan ctx st.canong st.canonlab st.samerows ∧ (processnode ctx level numcells st).snd.samerows = n

The row-decided rejection: a code-tied leaf at the incumbent's depth whose rows compare below is discarded, freezing the downward comparison.

theorem Hex.GraphIso.Nauty.processnode_frames {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (processnode ctx level numcells st).snd.lab = st.lab ∧ (processnode ctx level numcells st).snd.ptn = st.ptn ∧ (processnode ctx level numcells st).snd.eqlevFirst = st.eqlevFirst ∧ (processnode ctx level numcells st).snd.firstcode = st.firstcode ∧ (processnode ctx level numcells st).snd.firstlab = st.firstlab ∧ (processnode ctx level numcells st).snd.firsttc = st.firsttc ∧ (processnode ctx level numcells st).snd.gcaFirst = st.gcaFirst ∧ (processnode ctx level numcells st).snd.noncheaplevel = st.noncheaplevel ∧ (processnode ctx level numcells st).snd.allsamelevel = st.allsamelevel

The fields processnode never writes: the labelling pair, the first-path data, and the level bookkeeping consumed by the child loops.

theorem Hex.GraphIso.Nauty.processnode_rowTie {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) : ((processnode ctx level numcells st).fst = Int.ofNat st.gcaFirst ∨ (processnode ctx level numcells st).fst = Int.ofNat st.gcaCanon) ∧ (processnode ctx level numcells st).snd.compCanon = 0 ∧ (processnode ctx level numcells st).snd.eqlevCanon = st.eqlevCanon ∧ (processnode ctx level numcells st).snd.canoncode = st.canoncode ∧ (processnode ctx level numcells st).snd.canonlevel = st.canonlevel ∧ (processnode ctx level numcells st).snd.canonlab = st.canonlab ∧ (processnode ctx level numcells st).snd.canong = updatecan ctx st.canong st.canonlab st.samerows ∧ (processnode ctx level numcells st).snd.samerows = n

The row-tied arm: a code-tied leaf at the incumbent's depth whose rows equal the incumbent's is an automorphism candidate (nauty's code 2); the incumbent survives unchanged and the unwind returns to one of the guiding ancestors.

theorem Hex.GraphIso.Nauty.processnode_leaf {n nn : Nat} {ctx : Ctx n} {cs bs : List Nat} {numcells : Nat} {st : SearchSt n} (hcinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hginv : CanongInv ctx st.canong st.canonlab st.samerows) (hcsn : cs.length ≤ nn) (hef : ¬(st.eqlevFirst == cs.length) = true) (hnc : (numcells == n) = true) : ∃ (bs' : List Nat), incKey ctx bs' (processnode ctx cs.length numcells st).snd.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ CanongInv ctx (processnode ctx cs.length numcells st).snd.canong (processnode ctx cs.length numcells st).snd.canonlab (processnode ctx cs.length numcells st).snd.samerows ∧ ((processnode ctx cs.length numcells st).snd.compCanon ≤ 0 ∧ CodeCmpInv nn cs bs' (processnode ctx cs.length numcells st).snd.canoncode (processnode ctx cs.length numcells st).snd.canonlevel (processnode ctx cs.length numcells st).snd.eqlevCanon (processnode ctx cs.length numcells st).snd.compCanon ∨ (processnode ctx cs.length numcells st).snd.compCanon < 0 ∧ CodeCmpInv nn cs bs' (processnode ctx cs.length numcells st).snd.canoncode (processnode ctx cs.length numcells st).snd.canonlevel (processnode ctx cs.length numcells st).snd.eqlevCanon 0) ∧ ((processnode ctx cs.length numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ∨ (processnode ctx cs.length numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat cs.length) ∨ (processnode ctx cs.length numcells st).fst = Int.ofNat st.gcaFirst ∨ (processnode ctx cs.length numcells st).fst = Int.ofNat st.gcaCanon)

The full leaf event off the first path: at a discrete node, processnode leaves the incumbent at the key maximum of the entry incumbent and the current leaf, re-establishes the store invariant, and hands back a comparison machine for the unwind. That machine is intact when the comparison stayed frozen or was re-seeded by an install, and in the reset form when a row rejection repurposed compCanon (recover_codeInv_reset consumes it). The return level is one of the four unwind forms.

theorem Hex.GraphIso.Nauty.recover_machines {n nn inf : Nat} {cs bs fs : List Nat} {st : SearchSt n} {lvl : Nat} (hc : st.compCanon ≤ 0 ∧ CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon ∨ CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon 0) (hf : FirstCodeInv nn cs fs st.firstcode st.eqlevFirst) (hlvl : lvl ≤ cs.length) : CodeCmpInv nn (List.take lvl cs) bs (recover n inf lvl st).canoncode (recover n inf lvl st).canonlevel (recover n inf lvl st).eqlevCanon (recover n inf lvl st).compCanon ∧ FirstCodeInv nn (List.take lvl cs) fs (recover n inf lvl st).firstcode (recover n inf lvl st).eqlevFirst

One recover step after a node event: the comparison machine survives the unwind in whichever mode the event left it (live with compCanon ≤ 0, or the reset mode a row rejection leaves behind), and the first-path machine is clamped. The induction applies this at every return to a child loop.

def Hex.GraphIso.Nauty.firstScatter (n : Nat) (firstlab lab : Array Nat) : Array Nat

nauty's workperm at a first-path-agreeing leaf: the scatter of the current leaf's labelling over the first leaf's.

Equations

• Hex.GraphIso.Nauty.firstScatter n firstlab lab = List.foldl (fun (w : Array Nat) (i : Nat) => w.set! firstlab[i]! lab[i]!) (Array.replicate n 0) (List.range n)

theorem Hex.GraphIso.Nauty.firstScatter_size (n : Nat) (lab₁ lab₂ : Array Nat) : (firstScatter n lab₁ lab₂).size = n

A first-to-current scatter preserves its fixed n-slot workspace size.

theorem Hex.GraphIso.Nauty.scatter_eq_of_full {lab₁ lab₂ base base' : Array Nat} {nn : Nat} (hbase : base.size = nn) (hbase' : base'.size = nn) (hsize : lab₁.size = nn) (hok : LabOk lab₁ nn) (hinj : LabInj lab₁ nn) : List.foldl (fun (r : Array Nat) (i : Nat) => r.set! lab₁[i]! lab₂[i]!) base (List.range nn) = List.foldl (fun (r : Array Nat) (i : Nat) => r.set! lab₁[i]! lab₂[i]!) base' (List.range nn)

A full scatter from a permutation labelling overwrites every slot, so its result is independent of the initial workspace contents.

theorem Hex.GraphIso.Nauty.processnode_auto {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (heq : (st.eqlevFirst == level) = true) (hsent : st.firstcode[level + 1]! = codeSentinel) (hnc : (numcells == n) = true) (hpass : isautom ctx (firstScatter n st.firstlab st.lab) = true) : (processnode ctx level numcells st).fst = Int.ofNat st.gcaFirst ∧ (processnode ctx level numcells st).snd.compCanon = st.compCanon ∧ (processnode ctx level numcells st).snd.eqlevCanon = st.eqlevCanon ∧ (processnode ctx level numcells st).snd.canoncode = st.canoncode ∧ (processnode ctx level numcells st).snd.canonlevel = st.canonlevel ∧ (processnode ctx level numcells st).snd.canonlab = st.canonlab ∧ (processnode ctx level numcells st).snd.canong = st.canong ∧ (processnode ctx level numcells st).snd.samerows = st.samerows

The code-1 arm: a first-path-agreeing leaf passing the admission test records a generator and unwinds to gcaFirst with the whole comparison state untouched.

theorem Hex.GraphIso.Nauty.processnode_auto_gcaCanon {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (heq : (st.eqlevFirst == level) = true) (hsent : st.firstcode[level + 1]! = codeSentinel) (hnc : (numcells == n) = true) (hpass : isautom ctx (firstScatter n st.firstlab st.lab) = true) : (processnode ctx level numcells st).snd.gcaCanon = st.gcaCanon

A successful code-one admission does not change the canonical GCA control.

theorem Hex.GraphIso.Nauty.processnode_auto_short {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (heq : (st.eqlevFirst == level) = true) (hsent : st.firstcode[level + 1]! = codeSentinel) (hnc : (numcells == n) = true) (hpass : isautom ctx (firstScatter n st.firstlab st.lab) = true) : (processnode ctx level numcells st).snd.needshortprune = st.needshortprune

A code-one admission does not create a short-prune request.

theorem Hex.GraphIso.Nauty.processnode_auto_autos {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (heq : (st.eqlevFirst == level) = true) (hsent : st.firstcode[level + 1]! = codeSentinel) (hnc : (numcells == n) = true) (hpass : isautom ctx (firstScatter n st.firstlab st.lab) = true) : (processnode ctx level numcells st).snd.autos = (pushAuto st (fmperm (firstScatter n st.firstlab st.lab) n)).autos

The code-one arm stores the same first-to-current scatter that it appends to the generator trace.

def Hex.GraphIso.Nauty.canonScatter (n : Nat) (canonlab lab : Array Nat) : Array Nat

The scatter built from the installed canonical leaf to the current leaf.

Equations

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

theorem Hex.GraphIso.Nauty.canonScatter_eq_firstScatter (n : Nat) (canonlab lab : Array Nat) : canonScatter n canonlab lab = firstScatter n canonlab lab

def Hex.GraphIso.Nauty.pruneAutos {n : Nat} (level : Nat) (st : SearchSt n) : Array (VSet n × VSet n)

The bounded-ledger effect of the shared code-three/code-four tail.

Equations

• Hex.GraphIso.Nauty.pruneAutos level st = if level = st.noncheaplevel then st.autos else (Hex.GraphIso.Nauty.pushAuto st (Hex.GraphIso.Nauty.fmptn st.lab st.ptn st.noncheaplevel n)).autos

theorem Hex.GraphIso.Nauty.pruneAutos_back {n level : Nat} {st : SearchSt n} (hworkspace : WorkspaceOk st) (hne : level ≠ st.noncheaplevel) : (pruneAutos level st).back? = some (fmptn st.lab st.ptn st.noncheaplevel n)

Whenever the shared tail admits its implicit pair, bounded workspace capacity makes that pair the exact newest entry read by shortprune.

theorem Hex.GraphIso.Nauty.processnode_fast_autos {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) : (processnode ctx level numcells st).snd.autos = pruneAutos level st

The frozen-downward fast arm has exactly the shared prune-tail ledger effect.

theorem Hex.GraphIso.Nauty.processnode_shortInstall_autos {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hlt : level < st.canonlevel) : (processnode ctx level numcells st).snd.autos = pruneAutos level st

The short-leaf install has exactly the shared prune-tail ledger effect.

theorem Hex.GraphIso.Nauty.processnode_upInstall_autos {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 1) : (processnode ctx level numcells st).snd.autos = pruneAutos level st

The upward-frozen install has exactly the shared prune-tail ledger effect.

theorem Hex.GraphIso.Nauty.processnode_rowInstall_autos {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (hgt : 0 < (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst) : (processnode ctx level numcells st).snd.autos = pruneAutos level st

A row-decided install has exactly the shared prune-tail ledger effect.

theorem Hex.GraphIso.Nauty.processnode_rowReject_autos {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (hlt : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst < 0) : (processnode ctx level numcells st).snd.autos = pruneAutos level st

A row-decided rejection has exactly the shared prune-tail ledger effect.

theorem Hex.GraphIso.Nauty.processnode_rowTie_orbit {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) : (processnode ctx level numcells st).fst = Int.ofNat st.gcaCanon ∨ (processnode ctx level numcells st).fst = Int.ofNat st.gcaFirst ∧ (processnode ctx level numcells st).snd.orbits[(processnode ctx level numcells st).snd.cosetindex]! < (processnode ctx level numcells st).snd.cosetindex

A row-tied code-two return either uses the canonical ancestor, or its special first-ancestor return is backed by a strictly smaller orbit pointer in the output state.

theorem Hex.GraphIso.Nauty.processnode_rowTie_short {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) (hclear : st.needshortprune = false) (hshort : (processnode ctx level numcells st).snd.needshortprune = true) : (processnode ctx level numcells st).fst = Int.ofNat st.gcaCanon

A fresh short-prune request from the code-two arm accompanies the canonical-guide return; the special first-guide orbit return never raises the flag.

theorem Hex.GraphIso.Nauty.processnode_rowTie_gcaCanon {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) : (processnode ctx level numcells st).snd.gcaCanon = st.gcaCanon

The code-two arm leaves the canonical guide untouched.

theorem Hex.GraphIso.Nauty.processnode_rowTie_autos {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) : (processnode ctx level numcells st).snd.autos = (pushAuto st (fmperm (canonScatter n st.canonlab st.lab) n)).autos

The code-two arm stores the same incumbent-to-current scatter that it appends to the generator trace.

theorem Hex.GraphIso.Nauty.processnode_gateFail_eq {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (heq : (st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hfail : st.firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n st.firstlab st.lab) = false) : ((processnode ctx level numcells st).fst = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).fst ∨ (processnode ctx level numcells st).fst = Int.ofNat st.gcaFirst ∨ (processnode ctx level numcells st).fst = Int.ofNat st.gcaCanon) ∧ (processnode ctx level numcells st).snd.compCanon = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).snd.compCanon ∧ (processnode ctx level numcells st).snd.eqlevCanon = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).snd.eqlevCanon ∧ (processnode ctx level numcells st).snd.canoncode = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).snd.canoncode ∧ (processnode ctx level numcells st).snd.canonlevel = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).snd.canonlevel ∧ (processnode ctx level numcells st).snd.canonlab = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).snd.canonlab ∧ (processnode ctx level numcells st).snd.canong = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).snd.canong ∧ (processnode ctx level numcells st).snd.samerows = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).snd.samerows

A first-path-agreeing leaf failing the admission test behaves, in the return level and the whole comparison state, exactly as the same state entered off the first path. The only effect of the test is the skipped generator.

theorem Hex.GraphIso.Nauty.processnode_gateFail_autos {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hcanonSize : st.canonlab.size = n) (hcanonOk : LabOk st.canonlab n) (hcanonInj : LabInj st.canonlab n) (heq : (st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hfail : st.firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n st.firstlab st.lab) = false) : (processnode ctx level numcells st).snd.autos = (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := level + 1, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }).snd.autos

Failing the first-path admission test has the same autos-ledger effect as entering the ordinary off-path comparison arm.

theorem Hex.GraphIso.Nauty.processnode_leafFirst {n nn : Nat} {ctx : Ctx n} {cs bs : List Nat} {numcells : Nat} {st : SearchSt n} (hcinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hginv : CanongInv ctx st.canong st.canonlab st.samerows) (hcsn : cs.length ≤ nn) (heq : (st.eqlevFirst == cs.length) = true) (hnc : (numcells == n) = true) (hfail : st.firstcode[cs.length + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n st.firstlab st.lab) = false) : ∃ (bs' : List Nat), incKey ctx bs' (processnode ctx cs.length numcells st).snd.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ CanongInv ctx (processnode ctx cs.length numcells st).snd.canong (processnode ctx cs.length numcells st).snd.canonlab (processnode ctx cs.length numcells st).snd.samerows ∧ ((processnode ctx cs.length numcells st).snd.compCanon ≤ 0 ∧ CodeCmpInv nn cs bs' (processnode ctx cs.length numcells st).snd.canoncode (processnode ctx cs.length numcells st).snd.canonlevel (processnode ctx cs.length numcells st).snd.eqlevCanon (processnode ctx cs.length numcells st).snd.compCanon ∨ (processnode ctx cs.length numcells st).snd.compCanon < 0 ∧ CodeCmpInv nn cs bs' (processnode ctx cs.length numcells st).snd.canoncode (processnode ctx cs.length numcells st).snd.canonlevel (processnode ctx cs.length numcells st).snd.eqlevCanon 0) ∧ ((processnode ctx cs.length numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ∨ (processnode ctx cs.length numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat cs.length) ∨ (processnode ctx cs.length numcells st).fst = Int.ofNat st.gcaFirst ∨ (processnode ctx cs.length numcells st).fst = Int.ofNat st.gcaCanon)

The leaf event at a first-path-agreeing leaf that fails the admission test: identical to processnode_leaf, by the reduction processnode_gateFail_eq.

theorem Hex.GraphIso.Nauty.auto_keyMax {n : Nat} {ctx : Ctx n} {cs fs bs : List Nat} {lab firstlab canonlab : Array Nat} (hcs : cs = fs) (hrows : leafRows ctx lab = leafRows ctx firstlab) (hfirst : keyLe (pathLeafKey ctx fs firstlab) (incKey ctx bs canonlab)) : keyMax (incKey ctx bs canonlab) (pathLeafKey ctx cs lab) = incKey ctx bs canonlab

The code-1 skip is sound at key level: with the codes agreeing with the first path outright and the rows transported by the admitted automorphism, the leaf's key is the first leaf's key, and an incumbent dominating the first leaf absorbs it.

theorem Hex.GraphIso.Nauty.otherNodePrep_frames {n : Nat} (level code : Nat) (st : SearchSt n) : (otherNodePrep level code st).canonlab = st.canonlab ∧ (otherNodePrep level code st).canong = st.canong ∧ (otherNodePrep level code st).samerows = st.samerows ∧ (otherNodePrep level code st).canonlevel = st.canonlevel ∧ (otherNodePrep level code st).firstlab = st.firstlab ∧ (otherNodePrep level code st).firsttc = st.firsttc ∧ (otherNodePrep level code st).gcaFirst = st.gcaFirst ∧ (otherNodePrep level code st).gcaCanon = st.gcaCanon ∧ (otherNodePrep level code st).noncheaplevel = st.noncheaplevel ∧ (otherNodePrep level code st).allsamelevel = st.allsamelevel ∧ (otherNodePrep level code st).orbits = st.orbits ∧ (otherNodePrep level code st).lab = st.lab ∧ (otherNodePrep level code st).ptn = st.ptn

The fields otherNodePrep never writes: everything the store invariant, the first-path data, and the unwind bookkeeping read.

theorem Hex.GraphIso.Nauty.recover_frames (n inf level : Nat) (st : SearchSt n) : (recover n inf level st).canonlab = st.canonlab ∧ (recover n inf level st).canong = st.canong ∧ (recover n inf level st).samerows = st.samerows ∧ (recover n inf level st).canonlevel = st.canonlevel ∧ (recover n inf level st).firstlab = st.firstlab ∧ (recover n inf level st).firsttc = st.firsttc ∧ (recover n inf level st).gcaFirst = st.gcaFirst ∧ (recover n inf level st).allsamelevel = st.allsamelevel ∧ (recover n inf level st).orbits = st.orbits ∧ (recover n inf level st).lab = st.lab

The fields recover never writes: the store invariant's data, the first-path arrays, and the unwind targets.

theorem Hex.GraphIso.Nauty.canongInv_otherNodePrep {n : Nat} {ctx : Ctx n} {level code : Nat} {st : SearchSt n} (h : CanongInv ctx st.canong st.canonlab st.samerows) : CanongInv ctx (otherNodePrep level code st).canong (otherNodePrep level code st).canonlab (otherNodePrep level code st).samerows

CanongInv passes through otherNodePrep untouched.

theorem Hex.GraphIso.Nauty.canongInv_recover {n : Nat} {ctx : Ctx n} {inf level : Nat} {st : SearchSt n} (h : CanongInv ctx st.canong st.canonlab st.samerows) : CanongInv ctx (recover n inf level st).canong (recover n inf level st).canonlab (recover n inf level st).samerows

CanongInv passes through recover untouched.

theorem Hex.GraphIso.Nauty.otherNodePrep_store {n : Nat} (level code : Nat) (st : SearchSt n) : (otherNodePrep level code st).genTrace = st.genTrace ∧ (otherNodePrep level code st).autos = st.autos

The store fields no internal step writes: the generator trace and the bounded autos workspace pass through otherNodePrep and recover untouched, so both ledger clauses ride the unwind and the comparison step by frame.

theorem Hex.GraphIso.Nauty.recover_store (n inf level : Nat) (st : SearchSt n) : (recover n inf level st).genTrace = st.genTrace ∧ (recover n inf level st).autos = st.autos

theorem Hex.GraphIso.Nauty.firstterminal_firstCodeInv {n nn : Nat} {cs : List Nat} {st : SearchSt n} (hsize : st.firstcode.size = nn + 2) (hLnn : cs.length ≤ nn) (hfc : ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!) (hclt : ∀ (c : Nat), c ∈ cs → c < codeSentinel) : FirstCodeInv nn cs cs (firstterminal cs.length st).firstcode (firstterminal cs.length st).eqlevFirst

firstterminal seeds the first-path machine: the just-installed first leaf agrees with itself at full depth.

theorem Hex.GraphIso.Nauty.firstterminal_canongInv {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} (hg : st.canong.size = n) : CanongInv ctx (firstterminal level st).canong (firstterminal level st).canonlab (firstterminal level st).samerows

firstterminal seeds the store invariant: the installed canonlab with samerows = 0 is vacuously consistent.

theorem Hex.GraphIso.Nauty.firstterminal_store {n : Nat} (level : Nat) (st : SearchSt n) : (firstterminal level st).genTrace = st.genTrace ∧ (firstterminal level st).autos = st.autos

firstterminal installs the first leaf without touching either store, so both ledger clauses are carried across the seed.

def Hex.GraphIso.Nauty.prefixKey {n : Nat} (cs : List Nat) (kk : Key n) : Key n

The absolute key of a spec subtree below the path codes cs.

Equations

• Hex.GraphIso.Nauty.prefixKey cs kk = { codes := cs ++ kk.codes, rows := kk.rows }

theorem Hex.GraphIso.Nauty.prefixKey_nil {n : Nat} (kk : Key n) : prefixKey [] kk = kk

theorem Hex.GraphIso.Nauty.prefixKey_keyMax {n : Nat} (cs : List Nat) (k1 k2 : Key n) : prefixKey cs (keyMax k1 k2) = keyMax (prefixKey cs k1) (prefixKey cs k2)

Prefixing by common path codes commutes with the key maximum.

theorem Hex.GraphIso.Nauty.prefixKey_leafKey {n : Nat} (ctx : Ctx n) (cs : List Nat) (code : Nat) (r : Array Nat) : prefixKey cs { codes := [code, codeSentinel], rows := leafRows ctx r } = pathLeafKey ctx (cs ++ [code]) r

A spec leaf's key under the path prefix is the path leaf key of the extended path.

theorem Hex.GraphIso.Nauty.specNode_discrete {n : Nat} {ctx : Ctx n} {tcLevel fuel level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells : Nat} (hdisc : discreteAt (refine ctx level lab ptn active numcells).ptn level n = true) : specNode ctx tcLevel (fuel + 1) level lab ptn active numcells = { codes := [(refine ctx level lab ptn active numcells).longcode, codeSentinel], rows := leafRows ctx (refine ctx level lab ptn active numcells).lab }

The discrete arm of specNode, isolated: at a node whose refinement is discrete, the subtree key is the leaf key.

theorem Hex.GraphIso.Nauty.prefixKey_cons {n : Nat} (cs : List Nat) (code : Nat) (K : Key n) : prefixKey cs { codes := code :: K.codes, rows := K.rows } = prefixKey (cs ++ [code]) K

Prefixing a common code moves it into the path.

theorem Hex.GraphIso.Nauty.prefixKey_keysMax {n : Nat} (l : List (Key n)) (b : Key n) (cs : List Nat) : prefixKey cs (keysMax b l) = keysMax (prefixKey cs b) (List.map (prefixKey cs) l)

Prefixing distributes over the seeded list maximum.

def Hex.GraphIso.Nauty.specChild {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells o : Nat) : Key n

One child key of a spec node: the subtree below individualizing the o-th target-cell vertex of the refined state.

Equations

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

theorem Hex.GraphIso.Nauty.specNode_internal {n : Nat} {ctx : Ctx n} {tcLevel fuel level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells len : Nat} (cs : List Nat) (hdisc : discreteAt (refine ctx level lab ptn active numcells).ptn level n = false) (hlen : (specMaketargetcell ctx (refine ctx level lab ptn active numcells).lab (refine ctx level lab ptn active numcells).ptn level tcLevel).snd.snd = len + 1) : prefixKey cs (specNode ctx tcLevel (fuel + 1) level lab ptn active numcells) = keysMax (prefixKey (cs ++ [(refine ctx level lab ptn active numcells).longcode]) (specChild ctx tcLevel fuel level lab ptn active numcells 0)) (List.map (fun (o : Nat) => prefixKey (cs ++ [(refine ctx level lab ptn active numcells).longcode]) (specChild ctx tcLevel fuel level lab ptn active numcells (o + 1))) (List.range len))

The internal arm of specNode, isolated: at a non-discrete node the subtree key under the path prefix is the maximum of the children's keys under the path extended by the node's own code.

theorem Hex.GraphIso.Nauty.discreteAt_iff_bcount {ptn : Array Nat} {level nn : Nat} (hnn : nn = ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) : discreteAt ptn level nn = true ↔ bcount ptn level nn = nn

Discreteness is exactly a full boundary count.

structure Hex.GraphIso.Nauty.DomOk {n k : Nat} (G : Colored n k) (ctx : Ctx n) (rlab rptn : Array Nat) (cs bs fs : List Nat) (numcells : Nat) (st : SearchSt n) : Prop

The entry invariant of the maximality induction at a node about to refine at level = cs.length + 1: the search skeleton, both comparison machines, the store invariant, cell stabilization of every recorded generator at this node, and the two ledgers the pruning arms consume.

genTraceOk is store validity: every recorded generator is a checked automorphism, which is what childKey_of_carried needs of the carriers the gca returns hand up. autosOk is the (fix, mcr) ledger of Invariant/Autos, anchored at the root partition rptn/rlab where it is unconditional; the shortprune/longprune arms move a single pair down the path with pairOk_descend at the point of use.

• searchOk : SearchOk G (cs.length + 1) numcells st
• codeInv : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon
• firstInv : FirstCodeInv n cs fs st.firstcode st.eqlevFirst
• canongInv : CanongInv ctx st.canong st.canonlab st.samerows
• stab (γ : Array Nat) : γ ∈ st.genTrace → CellStab st.ptn (cs.length + 1) st.lab γ
• genTraceOk : GenTraceOk ctx st (ColorMap G)
• autosOk : AutosOk ctx.g rptn rlab 1 st.autos

theorem Hex.GraphIso.Nauty.genTraceOk_of_eq {n : Nat} {ctx : Ctx n} {st st' : SearchSt n} {P : Array Nat → Prop} (h : st'.genTrace = st.genTrace) (hok : GenTraceOk ctx st P) : GenTraceOk ctx st' P

Store validity crosses a frame-preserving step.

theorem Hex.GraphIso.Nauty.autosOk_of_eq {n : Nat} {g : Array (VSet n)} {rptn rlab : Array Nat} {st st' : SearchSt n} (h : st'.autos = st.autos) (hok : AutosOk g rptn rlab 1 st.autos) : AutosOk g rptn rlab 1 st'.autos

The (fix, mcr) ledger crosses a frame-preserving step.

theorem Hex.GraphIso.Nauty.rows_eq_of_testcanlab_tie {n : Nat} {ctx : Ctx n} {st : SearchSt n} (hinv : CanongInv ctx st.canong st.canonlab st.samerows) (h : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) : leafRows ctx st.canonlab = leafRows ctx st.lab

A testcanlab tie against the updated store says the leaf's rows are the incumbent's: this is the harm3 hypothesis of genTraceOk_processnode, supplied from DomOk.canongInv.

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

A reached labelling lands in the vertex range.

theorem Hex.GraphIso.Nauty.labInj_of_reach {n k : Nat} {G : Colored n k} {lab : Array Nat} (hsz : lab.size = n) (hn0 : 0 < n) (h : CellsReach G lab) : LabInj lab n

A reached labelling is injective: it is a permutation of the vertex range, hence duplicate-free.

theorem Hex.GraphIso.Nauty.codeInv_take_listCmp_lt {nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) {M : Nat} (hM : eqlevCanon.toNat < M) (hMcs : M ≤ cs.length) (ext : List Nat) : listCmp compare (List.take M cs ++ ext) (bs ++ [codeSentinel]) = Ordering.lt

The frozen divergence survives truncation: with the divergence recorded at level eqlevCanon + 1, the path prefix down to any level at or beyond it still compares below the incumbent, whatever comes after.

theorem Hex.GraphIso.Nauty.frozen_take_keyCmp_lt {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) {M : Nat} (hM : eqlevCanon.toNat < M) (hMcs : M ≤ cs.length) (K : Key n) : keyCmp (prefixKey (List.take M cs) K) (incKey ctx bs canonlab) = Ordering.lt

The key-level truncated verdict: every subtree hanging below the truncated path is dominated once the machine froze downward at or above the truncation level.

theorem Hex.GraphIso.Nauty.frozen_take_keyLe {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) {M : Nat} (hM : eqlevCanon.toNat < M) (hMcs : M ≤ cs.length) (K : Key n) : keyLe (prefixKey (List.take M cs) K) (incKey ctx bs canonlab)

frozen_take_keyCmp_lt in the keyLe form the absorption consumes.

theorem Hex.GraphIso.Nauty.frozen_keyLe {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) (K : Key n) : keyLe (prefixKey cs K) (incKey ctx bs canonlab)

The whole-path instance: with the machine frozen downward, every subtree below the current path is dominated.

theorem Hex.GraphIso.Nauty.childKey_of_carried {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {γ : Array Nat} (hAut : checkAutom ctx.g γ = true) (tcLevel fuel level : Nat) {rsLab rsPtn : Array Nat} {tc lenT numcells o o' : Nat} (hstab : CellStab rsPtn level rsLab γ) (hs : rsLab.size = n) (hok : LabOk rsLab n) (hsp : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hic : IsCell rsPtn level tc lenT) (hrange : tc + lenT ≤ n) (ho : o < lenT) (ho' : o' < lenT) (hlf : level + 1 + fuel ≤ n + 1) (hcarry : γ[rsLab[tc + o']!]! = rsLab[tc + o]!) : childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o = childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o'

A checked automorphism stabilizing the refined node's cells and carrying one target-cell vertex onto another identifies the two children's subtree keys.