def Hex.GraphIso.Nauty.nodeKey {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (cs : List Nat) (st : SearchSt n) (numcells : Nat) : Key n

The subtree key of a node, under its path codes.

Equations

• Hex.GraphIso.Nauty.nodeKey ctx tcLevel fuel level cs st numcells = Hex.GraphIso.Nauty.prefixKey cs (Hex.GraphIso.Nauty.specNode ctx tcLevel fuel level st.lab st.ptn st.active numcells)

def Hex.GraphIso.Nauty.bestCodesOf {n : Nat} (st : SearchSt n) : List Nat

The incumbent's code list, as runTraced reports it.

Equations

• Hex.GraphIso.Nauty.bestCodesOf st = List.map (fun (i : Nat) => st.canoncode[i]!) (List.range' 1 st.canonlevel)

def Hex.GraphIso.Nauty.stInc {n : Nat} (ctx : Ctx n) (st : SearchSt n) : Option (Key n)

The incumbent a state carries, or none before the first install.

Equations

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

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

The semantic incumbent represented by the comparison machine's ghost code list.

Equations

• Hex.GraphIso.Nauty.ghostInc ctx bs canonlab = if bs = [] then none else some (Hex.GraphIso.Nauty.incKey ctx bs canonlab)

theorem Hex.GraphIso.Nauty.bestCodesOf_eq {n nn : Nat} {cs bs : List Nat} {st : SearchSt n} {compCanon : Int} (hinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon compCanon) (hne : compCanon ≠ 1) : bestCodesOf st = bs

Outside the upward overwrite window, canoncode contains exactly the ghost incumbent codes.

theorem Hex.GraphIso.Nauty.stInc_eq_ghost {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {st : SearchSt n} {compCanon : Int} (hinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon compCanon) (hne : compCanon ≠ 1) : stInc ctx st = ghostInc ctx bs st.canonlab

At a stable comparison state, reading the mutable incumbent agrees with the semantic ghost incumbent.

theorem Hex.GraphIso.Nauty.firstScatter_get {flab lab : Array Nat} {nn : Nat} (hinj : ∀ (a b : Nat), a < nn → b < nn → flab[a]! = flab[b]! → a = b) (hlt : ∀ (i : Nat), i < nn → flab[i]! < nn) {j : Nat} : j < nn → (firstScatter nn flab lab)[flab[j]!]! = lab[j]!

The generator processnode records maps the first-path labelling onto the current one pointwise, given only that the first-path labelling is injective and bounded. Nothing about codes, code lengths, or where the first path went discrete is used.

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

Individualizing offset o puts that offset's vertex at the target position.

theorem Hex.GraphIso.Nauty.isCell_breakout_target {n : Nat} {lab ptn : Array Nat} {level tc tv : Nat} (hlt : tc < ptn.size) (hstart : tc = 0 ∨ ptn[tc - 1]! ≤ level) : IsCell (breakout n lab ptn (level + 1) tc tv).snd.fst (level + 1) tc 1

Individualizing closes the target position, so it becomes a singleton cell one level down. This is what makes the transport below apply from the child onwards.

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

refine leaves a singleton cell's position exactly where it was: it permutes cell contents, and a singleton cell has only one.

theorem Hex.GraphIso.Nauty.singleton_outside_cell {ptn : Array Nat} {level a tc len o : Nat} (hca : IsCell ptn level a 1) (hct : IsCell ptn level tc len) (hne : a ≠ tc) (ho : o < len) : a < tc ∨ tc + o < a

A singleton cell lies outside any other cell, so outside the window a breakout at that other cell rotates.

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

A breakout at a different cell leaves a singleton cell's position alone. Together with refine_fixes_singleton this is the whole content of the descent's position bookkeeping, one operation at a time.

def Hex.GraphIso.Nauty.rootSt (n : Nat) (lab0 : Array Nat) (cellEnds : List Nat) : SearchSt n

The root state runTraced starts from.

Equations

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

def Hex.GraphIso.Nauty.rootOut (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : SearchSt n

The state the root call returns.

Equations

• Hex.GraphIso.Nauty.rootOut n g lab0 cellEnds = (Hex.GraphIso.Nauty.firstPathNode { g := g } (n + 2) 100 (n + 2) 1 cellEnds.length (Hex.GraphIso.Nauty.rootSt n lab0 cellEnds)).snd

theorem Hex.GraphIso.Nauty.bestCodes_runTraced {n : Nat} {g : Array (VSet n)} {lab0 : Array Nat} {cellEnds : List Nat} (hn0 : n ≠ 0) : (runTraced n g lab0 cellEnds).bestCodes = bestCodesOf (rootOut n g lab0 cellEnds)

runTraced's reported codes are the returned state's own reading.

theorem Hex.GraphIso.Nauty.canonlab_runTraced {n : Nat} {g : Array (VSet n)} {lab0 : Array Nat} {cellEnds : List Nat} (hn0 : n ≠ 0) : (runTraced n g lab0 cellEnds).result.canonlab = (rootOut n g lab0 cellEnds).canonlab

runTraced's reported labelling is the returned state's.

theorem Hex.GraphIso.Nauty.stInc_final {n k : Nat} {G : Colored n k} (hn0 : n ≠ 0) (hinst : (rootOut n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).canonlevel ≠ 0) : stInc { g := rowsOf G } (rootOut n (rowsOf G) (initialPartition G).fst (initialPartition G).snd) = some (tracedKey G)

The traced key is the final state's incumbent, once anything has been installed.

theorem Hex.GraphIso.Nauty.nodeKey_root {n k : Nat} {G : Colored n k} (hn0 : n ≠ 0) : nodeKey { g := rowsOf G } 100 n 1 [] (rootSt n (initialPartition G).fst (initialPartition G).snd) (initialPartition G).snd.length = canonSpecKey G

The root's node key is the specification's canonical key.

theorem Hex.GraphIso.Nauty.stInc_congr {n : Nat} {ctx : Ctx n} {st st' : SearchSt n} (hlv : st'.canonlevel = st.canonlevel) (hcc : st'.canoncode = st.canoncode) (hcl : st'.canonlab = st.canonlab) : stInc ctx st' = stInc ctx st

The incumbent reading depends on canonlevel, canoncode and canonlab, and on nothing else.

theorem Hex.GraphIso.Nauty.stInc_numnodes {n : Nat} {ctx : Ctx n} (st : SearchSt n) (m : Nat) : stInc ctx { 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 := st.eqlevFirst, 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 := m, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } = stInc ctx st

Counting a node leaves the incumbent alone.

theorem Hex.GraphIso.Nauty.stInc_refined {n : Nat} {ctx : Ctx n} (st : SearchSt n) (lab ptn : Array Nat) (active : VSet n) : stInc ctx { lab := lab, ptn := ptn, active := 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 := st.eqlevFirst, 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 } = stInc ctx st

Refining leaves the incumbent alone: it writes the labelling, the partition and the active set.

theorem Hex.GraphIso.Nauty.stInc_firstcode {n : Nat} {ctx : Ctx n} (st : SearchSt n) (fc : Array Nat) : stInc ctx { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := fc, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, 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 } = stInc ctx st

Recording this node's refinement code leaves the incumbent alone. firstcode is the first path's ledger, not the incumbent's.

theorem Hex.GraphIso.Nauty.stInc_firsttc {n : Nat} {ctx : Ctx n} (st : SearchSt n) (ftc : Array Int) : stInc ctx { 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 := ftc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, 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 } = stInc ctx st

Recording this node's target cell leaves the incumbent alone.

theorem Hex.GraphIso.Nauty.stInc_tctotal {n : Nat} {ctx : Ctx n} (st : SearchSt n) (m : Nat) : stInc ctx { 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 := st.eqlevFirst, 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 := m, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } = stInc ctx st

Accumulating the target-cell total leaves the incumbent alone.

theorem Hex.GraphIso.Nauty.stInc_noncheaplevel {n : Nat} {ctx : Ctx n} (st : SearchSt n) (m : Nat) : stInc ctx { 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 := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := m, 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 } = stInc ctx st

Raising the cheap-automorphism level leaves the incumbent alone.

theorem Hex.GraphIso.Nauty.stInc_allsamelevel {n : Nat} {ctx : Ctx n} (st : SearchSt n) (m : Nat) : stInc ctx { 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 := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := m, 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 } = stInc ctx st

The node's exit adjustment leaves the incumbent alone. This is the allsamelevel decrement firstPathNode performs when its target cell was exhausted, and it is the only write between the child loop's return and the node's own.

theorem Hex.GraphIso.Nauty.stInc_otherNodePrep {n : Nat} (level code : Nat) (st : SearchSt n) : (otherNodePrep level code st).canonlevel = st.canonlevel ∧ (otherNodePrep level code st).canonlab = st.canonlab

The comparison bookkeeping otherNode performs before choosing its target cell leaves the incumbent alone, except through canoncode, which it rewrites exactly when the current node's code beats the incumbent's at this level. Stated as the three fields so the caller can see which one moves.

theorem Hex.GraphIso.Nauty.firstterminal_canonlevel {n : Nat} (level : Nat) (st : SearchSt n) : (firstterminal level st).canonlevel = level

A first-path leaf installs itself: the incumbent's level is this node's.

theorem Hex.GraphIso.Nauty.firstterminal_canonlab {n : Nat} (level : Nat) (st : SearchSt n) : (firstterminal level st).canonlab = st.lab

A first-path leaf installs its own labelling.

theorem Hex.GraphIso.Nauty.firstterminal_firstlab {n : Nat} (level : Nat) (st : SearchSt n) : (firstterminal level st).firstlab = st.lab

A first-path leaf also records its labelling as the first reference leaf.

theorem Hex.GraphIso.Nauty.firstterminal_installed {n level : Nat} (hlev : level ≠ 0) (st : SearchSt n) : (firstterminal level st).canonlevel ≠ 0

A first-path leaf at a positive level leaves something installed.