theorem Hex.GraphIso.Nauty.LabInj.eq_of_getElem! {lab : Array Nat} {n i j : Nat} (h : LabInj lab n) (hi : i < n) (hj : j < n) (heq : lab[i]! = lab[j]!) : i = j

Elimination form of LabInj, exported so downstream outcome modules need not unfold its opaque definition.

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

Both leaf references installed after the first descent are reached permutation labellings.

• firstSize : st.firstlab.size = n
• firstReach : CellsReach G st.firstlab
• canonSize : st.canonlab.size = n
• canonReach : CellsReach G st.canonlab

theorem Hex.GraphIso.Nauty.CellsReach.ofCellsPerm {n k : Nat} {G : Colored n k} {level numcells : Nat} {st : SearchSt n} {lab : Array Nat} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (hsize : lab.size = n) (hperm : cellsPerm st.ptn level st.lab lab) : CellsReach G lab

A permutation inside the cells of a reached search state is still reachable from the initial coloured partition.

theorem Hex.GraphIso.Nauty.LeafRefsOk.firstterminal {n k : Nat} {G : Colored n k} {level numcells : Nat} {st : SearchSt n} (hok : SearchOk G level numcells st) : LeafRefsOk G (Nauty.firstterminal level st)

Installing the first leaf seeds both valid leaf references.

theorem Hex.GraphIso.Nauty.SearchOut.leafRefs {n k : Nat} {G : Colored n k} {B level numcells : Nat} {st out : SearchSt n} (h : SearchOut G B level st out) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) : LeafRefsOk G out

Every verified search fragment preserves validity of both installed leaf references.

structure Hex.GraphIso.Nauty.CheapOk {n : Nat} (ctx : Ctx n) (rlab rptn : Array Nat) (level : Nat) (st : SearchSt n) : Prop

The implicit automorphism pair remains valid while search stays strictly below the level at which that pair was frozen. At the frozen level itself the implication is dormant: processnode does not insert an implicit pair there, and a failed cheap-automorphism guard will move the boundary before the next descent.

• positive : 0 < st.noncheaplevel
• labSize : st.lab.size = n
• ptnSize : st.ptn.size = n
• rootEnd : st.ptn[st.ptn.size - 1]! ≤ 1
• pair : st.noncheaplevel < level → PairOk ctx.g rptn rlab 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd

theorem Hex.GraphIso.Nauty.CheapOk.ready {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level : Nat} {st : SearchSt n} (h : CheapOk ctx rlab rptn level st) (hbound : st.noncheaplevel ≤ level) (hne : level ≠ st.noncheaplevel) : PairOk ctx.g rptn rlab 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd

At a node entry, the runtime bound turns the strict-boundary ledger invariant into the premise consumed by processnode.

theorem Hex.GraphIso.Nauty.CheapOk.ofFrames {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level : Nat} {st out : SearchSt n} (h : CheapOk ctx rlab rptn level st) (hlab : out.lab = st.lab) (hptn : out.ptn = st.ptn) (hncl : out.noncheaplevel = st.noncheaplevel) : CheapOk ctx rlab rptn level out

The cheap-boundary invariant depends only on the current labelling, partition, and boundary level.

theorem Hex.GraphIso.Nauty.recover_fmptn {n : Nat} {st : SearchSt n} {inf level saved : Nat} (hsize : n ≤ st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ saved) (hsaved : saved ≤ level) (hinf : level < inf) : fmptn (recover n inf level st).lab (recover n inf level st).ptn saved n = fmptn st.lab st.ptn saved n

Reopening below level preserves every fmptn frozen at or above the root and at or below level.

theorem Hex.GraphIso.Nauty.CheapOk.recover {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {current level inf : Nat} {st : SearchSt n} (h : CheapOk ctx rlab rptn current st) (hle : level ≤ current) (hlevel : 1 ≤ level) (hinf : level < inf) : CheapOk ctx rlab rptn level (Nauty.recover n inf level st)

Recovery either parks the boundary just below the next child, where the strict pair condition is dormant, or retains an older frozen pair.

theorem Hex.GraphIso.Nauty.CheapOk.processnode {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level numcells : Nat} {st : SearchSt n} (h : CheapOk ctx rlab rptn level st) : CheapOk ctx rlab rptn level (Nauty.processnode ctx level numcells st).snd

Leaf processing does not move the frozen pair's defining fields.

theorem Hex.GraphIso.Nauty.CheapOk.firstterminal {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level : Nat} {st : SearchSt n} (h : CheapOk ctx rlab rptn level st) : CheapOk ctx rlab rptn level (Nauty.firstterminal level st)

Installing the first leaf does not move the frozen pair's defining fields.

theorem Hex.GraphIso.Nauty.CheapOk.otherNodePrep {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level code : Nat} {st : SearchSt n} (h : CheapOk ctx rlab rptn level st) : CheapOk ctx rlab rptn level (Nauty.otherNodePrep level code st)

The comparison preparation step does not move the frozen pair's defining fields.

theorem Hex.GraphIso.Nauty.CheapOk.park {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {old current boundary : Nat} {st : SearchSt n} (h : CheapOk ctx rlab rptn old st) (hpos : 0 < boundary) (hcurrent : current ≤ boundary) : CheapOk ctx rlab rptn current { 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 := boundary, 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 }

Writing a boundary at or above the logical level suspends the pair condition without changing the partition facts needed to revive it.

theorem Hex.GraphIso.Nauty.CheapOk.next {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level : Nat} {st : SearchSt n} (h : CheapOk ctx rlab rptn level st) (hpair : st.noncheaplevel = level → PairOk ctx.g rptn rlab 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd) : CheapOk ctx rlab rptn (level + 1) st

A valid pair at the current boundary extends the invariant through the next logical level.

theorem Hex.GraphIso.Nauty.CheapOk.refine {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level numcells : Nat} {st out : SearchSt n} (h : CheapOk ctx rlab rptn level st) (hlevel : 1 ≤ level) (hlab : out.lab = (Nauty.refine ctx level st.lab st.ptn st.active numcells).lab) (hptn : out.ptn = (Nauty.refine ctx level st.lab st.ptn st.active numcells).ptn) (hncl : out.noncheaplevel = st.noncheaplevel) : CheapOk ctx rlab rptn level out

Refinement only splits at the current level and permutes within the old current cells, so every pair frozen at a strictly smaller level is unchanged.

theorem Hex.GraphIso.Nauty.CheapOk.breakout {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level tc len o : Nat} {st out : SearchSt n} (h : CheapOk ctx rlab rptn (level + 1) st) (hlevel : 1 ≤ level) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hlab : out.lab = (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst) (hptn : out.ptn = st.ptn.set! tc (level + 1)) (hncl : out.noncheaplevel = st.noncheaplevel) : CheapOk ctx rlab rptn (level + 1) out

Individualizing inside a current cell does not change the implicit pair frozen at an older cheap boundary.

theorem Hex.GraphIso.Nauty.CheapOk.root {n k : Nat} {G : Colored n k} {ctx : Ctx n} {numcells : Nat} {st : SearchSt n} (hn0 : 0 < n) (hok : SearchOk G 1 numcells st) (hncl : st.noncheaplevel = 1) : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) 1 st

The initial search boundary is one, so its strict pair condition is empty at the root.

structure Hex.GraphIso.Nauty.RunInv {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel level : Nat) (cs bs fs : List Nat) (numcells : Nat) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) : Prop

The semantic state available after the first leaf has been installed.

The explicit level makes the package usable both at node entries and inside their child loops. At a node entry, level = cs.length + 1 recovers DomOk. A loop instead carries the code path through its current node, so its path has length level. The comparison sign is unrestricted: an internal node whose code first exceeds the incumbent can enter its child loop with sign one. Consumers that read the mutable incumbent or return an event supply the appropriate sign premise.

• searchOk : SearchOk G level 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
• genTraceOk : GenTraceOk ctx st (ColorMap G)
• autosOk : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos
• workspace : WorkspaceOk st
• cheap : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) level st
• leafRefs : LeafRefsOk G st
• guides : GuideStore ctx tcLevel level st best trail
• trailOk : TrailOk ctx level st trail
• firstPositive : 0 < st.gcaFirst
• canonPositive : 0 < st.gcaCanon
• firstBound : st.gcaFirst ≤ level
• canonBound : st.gcaCanon ≤ level
• bestCodes : bs ≠ []
• incumbent : best = some (incKey ctx bs st.canonlab)

theorem Hex.GraphIso.Nauty.RunInv.dom {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunInv G ctx tcLevel level cs bs fs numcells st best trail) (hpath : level = cs.length + 1) (hstab : ∀ (γ : Array Nat), γ ∈ st.genTrace → CellStab st.ptn level st.lab γ) : DomOk G ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) cs bs fs numcells st

At a node boundary the stable package supplies the existing DomOk record consumed by the leaf-event theorems.

theorem Hex.GraphIso.Nauty.RunInv.read {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunInv G ctx tcLevel level cs bs fs numcells st best trail) (hne : st.compCanon ≠ 1) : stInc ctx st = best

The semantic incumbent threaded by the induction agrees with the stable imperative state.

structure Hex.GraphIso.Nauty.RunPrep {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel level : Nat) (cs bs fs : List Nat) (numcells : Nat) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) : Prop

The semantic state after refinement and otherNodePrep, before processnode restores the stable comparison sign. This differs from RunInv only in omitting compCanon ≤ 0: comparing the freshly appended refinement code may set the sign to one.

• searchOk : SearchOk G level 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
• genTraceOk : GenTraceOk ctx st (ColorMap G)
• autosOk : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos
• workspace : WorkspaceOk st
• cheap : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) level st
• leafRefs : LeafRefsOk G st
• guides : GuideStore ctx tcLevel level st best trail
• trailOk : TrailOk ctx level st trail
• firstPositive : 0 < st.gcaFirst
• canonPositive : 0 < st.gcaCanon
• firstBound : st.gcaFirst ≤ level
• canonBound : st.gcaCanon ≤ level
• bestCodes : bs ≠ []
• incumbent : best = some (incKey ctx bs st.canonlab)

theorem Hex.GraphIso.Nauty.RunPrep.run {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunPrep G ctx tcLevel level cs bs fs numcells st best trail) : RunInv G ctx tcLevel level cs bs fs numcells st best trail

Once no immediate comparison prune is pending, the prepared state is the ordinary state carried into a child sweep. The two records are kept separate because RunPrep is also consumed by the leaf classifiers.

theorem Hex.GraphIso.Nauty.Equitable.ofCellsPerm {n : Nat} {ctx : Ctx n} {level : Nat} {lab lab' ptn : Array Nat} (heq : Equitable ctx level lab ptn) (hperm : cellsPerm ptn level lab lab') (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) : Equitable ctx level lab' ptn

Equitability depends only on the vertex sets of the partition cells, not on their order inside each cell.

structure Hex.GraphIso.Nauty.NodeInv {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel level : Nat) (cs bs fs : List Nat) (numcells : Nat) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) : Prop

The extra certificate state needed exactly where a node is about to call refine. RunInv is weaker because it also describes recovered parent-loop states, whose stale active field is never refined again.

• run : RunInv G ctx tcLevel level cs bs fs numcells st best trail
• cert : CertInv ctx level { lab := st.lab, ptn := st.ptn, active := st.active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }
• activeStarts (v : Nat) : st.active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level
• firstBelow : st.gcaFirst < level
• canonBelow : st.gcaCanon < level
• shortClear : st.needshortprune = false

theorem Hex.GraphIso.Nauty.NodeInv.refined {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hn0 : 0 < n) (hlevel : 1 ≤ level) (h : NodeInv G ctx tcLevel level cs bs fs numcells st best trail) : have r := refine ctx level st.lab st.ptn st.active numcells; IterOk ctx level r ∧ Equitable ctx level r.lab r.ptn ∧ bcount r.ptn level n = r.numcells

Refining a valid node entry produces the equitable frame used by its target-cell selection and child sweep.

theorem Hex.GraphIso.Nauty.NodeInv.target {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hn0 : 0 < n) (hlevel : 1 ≤ level) (h : NodeInv G ctx tcLevel level cs bs fs numcells st best trail) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells ≠ n) : have r := refine ctx level st.lab st.ptn st.active numcells; ∃ (tc : Nat), ∃ (len : Nat), maketargetcell ctx r.lab r.ptn level tcLevel (-1) = (tc, worksetOf n r.lab tc (tc + len - 1), len) ∧ specMaketargetcell ctx r.lab r.ptn level tcLevel = (tc, worksetOf n r.lab tc (tc + len - 1), len) ∧ IsCell r.ptn level tc len ∧ 2 ≤ len ∧ tc + len ≤ n

The unhinted executable target record of an internal node is exactly the specification target record, together with its nontrivial-cell geometry.

theorem Hex.GraphIso.Nauty.NodeInv.children {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (_h : NodeInv G ctx tcLevel level cs bs fs numcells st best trail) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = false) (hspec : specMaketargetcell ctx (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn level tcLevel = (tc, worksetOf n (refine ctx level st.lab st.ptn st.active numcells).lab tc (tc + len - 1), len)) (hlen : 2 ≤ len) : nodeKey ctx tcLevel (specFuel + 1) level cs st numcells = keysMax (sweepKey ctx tcLevel specFuel level (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn tc (refine ctx level st.lab st.ptn st.active numcells).numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn tc (refine ctx level st.lab st.ptn st.active numcells).numcells (o + 1)) (List.range (len - 1)))

The target record supplied by NodeInv.target exposes the node key as the exact maximum swept by the executable child loop.

theorem Hex.GraphIso.Nauty.RunInv.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells tc len o coset : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail childTrail : FrameTrail} (hn0 : 0 < n) (hlevel : 1 ≤ level) (h : RunInv G ctx tcLevel level cs bs fs numcells st best trail) (heq : Equitable ctx level st.lab st.ptn) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hshort : st.needshortprune = false) (hcheap : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) (level + 1) st) (hguides : GuideStore ctx tcLevel (level + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + o]!, 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 := coset, 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 } best childTrail) (htrail : TrailOk ctx (level + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + o]!, 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 := coset, 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 } childTrail) : NodeInv G ctx tcLevel (level + 1) cs bs fs (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + o]!, 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 := coset, 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 } best childTrail

Individualization carries a stable loop state into a valid recursive node entry. The loop supplies the two facts that depend on its history: the cheap-boundary state selected by the guard and the newly active guide store. Parent equitability seeds the child's refinement certificate.

theorem Hex.GraphIso.Nauty.RunInv.otherLeaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hpath : level = cs.length + 1) (h : RunInv G ctx tcLevel level cs bs fs numcells st best trail) : RunPrep G ctx tcLevel level (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) bs fs (refine ctx level st.lab st.ptn st.active numcells).numcells (otherLeafSt ctx level numcells st) best trail

Refinement followed by the off-path comparison step enters RunPrep. Generator validity is global, while stabilization is proved only at the loop frame where a generator is consumed.

theorem Hex.GraphIso.Nauty.firstterminal_state {n : Nat} (level : Nat) (st : SearchSt n) : (firstterminal level st).lab = st.lab ∧ (firstterminal level st).ptn = st.ptn ∧ (firstterminal level st).gcaFirst = level ∧ (firstterminal level st).gcaCanon = level ∧ (firstterminal level st).compCanon = 0

The state fields needed to enter the stable induction immediately after firstterminal.

theorem Hex.GraphIso.Nauty.firstterminal_short {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (firstterminal level (firstLeafSt ctx level numcells st)).needshortprune = st.needshortprune

Neither first-leaf preparation nor installation raises a short-prune request.

theorem Hex.GraphIso.Nauty.SearchOk.firstterminal {n k : Nat} {G : Colored n k} {level numcells : Nat} {st : SearchSt n} (h : SearchOk G level numcells st) : SearchOk G level numcells (Nauty.firstterminal level st)

Installing the first leaf preserves the search skeleton and records a reached canonical labelling.

theorem Hex.GraphIso.Nauty.RunInv.firstterminal {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs : List Nat} {st : SearchSt n} {trail : FrameTrail} (hpath : level = cs.length) (hok : SearchOk G level numcells st) (hfirstSize : st.firstcode.size = n + 2) (hcanonSize : st.canoncode.size = n + 2) (hbound : cs.length ≤ n) (hcodes : ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!) (hlt : ∀ (c : Nat), c ∈ cs → c < codeSentinel) (hcanong : st.canong.size = n) (hgen : st.genTrace = #[]) (hautos : st.autos = #[]) (hworkspace : WorkspaceOk st) (hcheap : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) cs.length st) (htrail : TrailOk ctx level st trail) (hne : cs ≠ []) : RunInv G ctx tcLevel level cs cs cs numcells (Nauty.firstterminal level st) (some (pathLeafKey ctx cs st.lab)) trail

The first leaf changes the pre-incumbent descent into the stable post-install invariant. Both mutable stores are still empty at this point. The ordinary node induction handles all later store growth.

theorem Hex.GraphIso.Nauty.recover_gcaCanon (n inf level : Nat) (st : SearchSt n) : (recover n inf level st).gcaCanon = if level < st.gcaCanon then level else st.gcaCanon

recover clamps the canonical guide target to the receiving level.

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

Parent recovery leaves the one-shot short-prune request unchanged.

theorem Hex.GraphIso.Nauty.recover_clearShort (n inf level : Nat) (st : SearchSt n) : recover n inf level { 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, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } = have __src := recover n inf level st; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace }

Clearing the one-shot prune request commutes with parent recovery.

theorem Hex.GraphIso.Nauty.LeafRefsOk.recover {n k : Nat} {G : Colored n k} {inf level : Nat} {st : SearchSt n} (h : LeafRefsOk G st) : LeafRefsOk G (Nauty.recover n inf level st)

Recovering a parent frame preserves both installed leaf references.

theorem Hex.GraphIso.Nauty.GuideStore.recover {n : Nat} {ctx : Ctx n} {tcLevel current : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {inf level : Nat} (h : GuideStore ctx tcLevel current st best trail) (hle : level ≤ current) : GuideStore ctx tcLevel level (Nauty.recover n inf level st) best trail

Recovering to an ancestor drops any guide aimed at the receiving frame and preserves every strictly older located guide.

theorem Hex.GraphIso.Nauty.GuideStore.processnode {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st out : SearchSt n} {before best : Option (Key n)} {trail : FrameTrail} (h : GuideStore ctx tcLevel level st before trail) (hinc : IncGrows before best) (hfirst : out.gcaFirst = st.gcaFirst) (hfirstlab : out.firstlab = st.firstlab) (hcanon : out.gcaCanon < level → out.gcaCanon = st.gcaCanon ∧ out.canonlab = st.canonlab) : GuideStore ctx tcLevel level out best trail

A leaf event preserves every older guide when the first reference is unchanged and any changed canonical reference is installed at the current level.

structure Hex.GraphIso.Nauty.RunEvent {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel current : Nat) (cs bs fs : List Nat) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) : Prop

State returned by a node event before its caller applies recover. The second comparison-machine case is the row-rejection reset: the mutable sign is negative while the retained proof is stated at sign zero, exactly as required by recover_codeInv_reset.

• machines : st.compCanon ≤ 0 ∧ CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon ∨ st.compCanon < 0 ∧ CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon 0
• firstInv : FirstCodeInv n cs fs st.firstcode st.eqlevFirst
• canongInv : CanongInv ctx st.canong st.canonlab st.samerows
• genTraceOk : GenTraceOk ctx st (ColorMap G)
• autosOk : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos
• workspace : WorkspaceOk st
• cheap : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) current st
• leafRefs : LeafRefsOk G st
• guides : GuideStore ctx tcLevel current st best trail
• trailOk : TrailOk ctx current st trail
• firstPositive : 0 < st.gcaFirst
• canonPositive : 0 < st.gcaCanon
• firstBound : st.gcaFirst ≤ current
• canonBound : st.gcaCanon ≤ current
• bestCodes : bs ≠ []
• incumbent : best = some (incKey ctx bs st.canonlab)

theorem Hex.GraphIso.Nauty.RunInv.event {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunInv G ctx tcLevel level cs bs fs numcells st best trail) (hnp : st.compCanon ≤ 0) : RunEvent G ctx tcLevel level cs bs fs st best trail

A stable state is already a valid event state.

theorem Hex.GraphIso.Nauty.recover_nonpositive {n inf level : Nat} {st : SearchSt n} (h : st.compCanon ≤ 0) : (recover n inf level st).compCanon ≤ 0

A nonpositive comparison sign remains nonpositive when recover either leaves it alone or resets it to zero.

theorem Hex.GraphIso.Nauty.RunEvent.recover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel current level inf numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunEvent G ctx tcLevel current cs bs fs st best trail) (hle : level ≤ current) (hlevel : 1 ≤ level) (hinf : level < inf) (hpath : level ≤ cs.length) (hfirst : st.gcaFirst ≤ level) (hok : SearchOk G level numcells (Nauty.recover n inf level st)) : RunInv G ctx tcLevel level (List.take level cs) bs fs numcells (Nauty.recover n inf level st) best trail

Applying recover to an event state restores the ordinary stable invariant at the selected ancestor prefix. Search reachability and cell stabilization are supplied by the surrounding loop, whose frozen frame determines the recovered partition.

theorem Hex.GraphIso.Nauty.LeafRefsOk.processnodeGen {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hn0 : 0 < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) (hcanong : CanongInv ctx st.canong st.canonlab st.samerows) (hgen : GenTraceOk ctx st (ColorMap G)) : GenTraceOk ctx (Nauty.processnode ctx level numcells st).snd (ColorMap G)

Valid installed leaf references, a valid current search labelling, and the row store are the exact hypotheses needed to preserve the generator store through processnode. This avoids packaging the post-refinement state in DomOk, whose path index describes a node before its next refinement code is appended.

theorem Hex.GraphIso.Nauty.LeafRefsOk.processnodeCarrier {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hn0 : 0 < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) (hcanong : CanongInv ctx st.canong st.canonlab st.samerows) : (Nauty.processnode ctx level numcells st).snd.genTrace = st.genTrace ∨ LabelCarrier ctx st.firstlab st.lab (Nauty.processnode ctx level numcells st).snd.genTrace ∨ LabelCarrier ctx st.canonlab st.lab (Nauty.processnode ctx level numcells st).snd.genTrace

The same correctly indexed leaf-state hypotheses identify any newly admitted generator as a checked carrier from the first or canonical leaf.

theorem Hex.GraphIso.Nauty.processnode_canonRef {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (processnode ctx level numcells st).snd.canonlab = st.canonlab ∨ (processnode ctx level numcells st).snd.canonlab = st.lab

processnode either retains the canonical reference or installs the current reached labelling.

theorem Hex.GraphIso.Nauty.processnode_canonGuide {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (processnode ctx level numcells st).snd.gcaCanon = st.gcaCanon ∧ (processnode ctx level numcells st).snd.canonlab = st.canonlab ∨ (processnode ctx level numcells st).snd.gcaCanon = level ∧ (processnode ctx level numcells st).snd.canonlab = st.lab

processnode either preserves the canonical guide and its reference, or installs the current leaf with the guide parked at the current level.

theorem Hex.GraphIso.Nauty.LeafRefsOk.processnode {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (h : LeafRefsOk G st) (hok : SearchOk G level numcells st) : LeafRefsOk G (Nauty.processnode ctx level numcells st).snd

Leaf-reference validity crosses every processnode outcome.

theorem Hex.GraphIso.Nauty.processnode_installed {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hlevel : 0 < level) (hold : st.canonlevel ≠ 0) : (processnode ctx level numcells st).snd.canonlevel ≠ 0

Once an incumbent exists, processnode either retains its positive level or replaces it by the current positive level.