structure Hex.GraphIso.Nauty.FirstInv {n k : Nat} (G : Colored n k) (ctx : Ctx n) (level : Nat) (cs : List Nat) (numcells : Nat) (st : SearchSt n) (trail : FrameTrail) : Prop

State carried by the unique descent before the first leaf exists.

• searchOk : SearchOk G level numcells st
• codes : DescentCodes n cs st
• cheap : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) level st
• 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
• trailOk : TrailOk ctx level st trail
• frameSize (target : Nat) (entry : TrailEntry) : target < level → trail target = some entry → entry.frame.rsLab.size = n
• genEmpty : st.genTrace = #[]
• autosEmpty : st.autos = #[]
• workspace : WorkspaceOk st
• canongSize : st.canong.size = n
• orbitId (v : Nat) : v < n → st.orbits[v]! = v
• shortClear : st.needshortprune = false

theorem Hex.GraphIso.Nauty.FirstInv.root {n k : Nat} {G : Colored n k} (hn0 : 0 < n) : FirstInv G { g := rowsOf G } 1 [] (initialPartition G).snd.length (rootSt n (initialPartition G).fst (initialPartition G).snd) FrameTrail.empty

A nonempty root starts the first descent with empty stores, identity orbits, and no active ancestor frame.

theorem Hex.GraphIso.Nauty.FirstInv.refined {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {cs : List Nat} {st : SearchSt n} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hn0 : 0 < n) (hlevel : 1 ≤ level) (h : FirstInv G ctx level cs numcells st 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 first-descent node produces the well-formed equitable state from which either the first leaf or the next child is selected.

theorem Hex.GraphIso.Nauty.FirstInv.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {specFuel level numcells tc len o : Nat} {cs : List Nat} {st : SearchSt n} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hn0 : 0 < n) (hpath : level = cs.length + 1) (hlt : level < n) (h : FirstInv G ctx level cs numcells st trail) (hcell : IsCell (refine ctx level st.lab st.ptn st.active numcells).ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) : have r := refine ctx level st.lab st.ptn st.active numcells; have full := cs ++ [r.longcode]; have pre0 := { lab := r.lab, ptn := r.ptn, active := r.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode.set! level r.longcode, canoncode := st.canoncode, firsttc := st.firsttc.set! level (Int.ofNat tc), 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 + 1, tctotal := st.tctotal + len, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; have pre := if pre0.noncheaplevel ≥ level ∧ ¬cheapautom pre0.ptn level n = true then { lab := pre0.lab, ptn := pre0.ptn, active := pre0.active, orbits := pre0.orbits, fixedpts := pre0.fixedpts, autos := pre0.autos, wsCap := pre0.wsCap, firstcode := pre0.firstcode, canoncode := pre0.canoncode, firsttc := pre0.firsttc, firstlab := pre0.firstlab, canonlab := pre0.canonlab, canong := pre0.canong, samerows := pre0.samerows, compCanon := pre0.compCanon, eqlevFirst := pre0.eqlevFirst, eqlevCanon := pre0.eqlevCanon, gcaFirst := pre0.gcaFirst, gcaCanon := pre0.gcaCanon, canonlevel := pre0.canonlevel, noncheaplevel := level + 1, allsamelevel := pre0.allsamelevel, cosetindex := pre0.cosetindex, stabvertex := pre0.stabvertex, needshortprune := pre0.needshortprune, numnodes := pre0.numnodes, tctotal := pre0.tctotal, canupdates := pre0.canupdates, numorbits := pre0.numorbits, numgenerators := pre0.numgenerators, numbadleaves := pre0.numbadleaves, maxlevel := pre0.maxlevel, genTrace := pre0.genTrace } else pre0; have child := { lab := (breakout n pre.lab pre.ptn (level + 1) tc pre.lab[tc + o]!).fst, ptn := (breakout n pre.lab pre.ptn (level + 1) tc pre.lab[tc + o]!).snd.fst, active := (breakout n pre.lab pre.ptn (level + 1) tc pre.lab[tc + o]!).snd.snd, orbits := pre.orbits, fixedpts := pre.fixedpts.insert pre.lab[tc + o]!, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.lab[tc + o]!, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; FirstInv G ctx (level + 1) full (r.numcells + 1) child (trail.push level { frame := sweepFrame specFuel full r.lab r.ptn tc r.numcells, offset := o })

The selected target-cell child preserves the pre-incumbent invariant and records its exact parent sweep position in the active trail.

theorem Hex.GraphIso.Nauty.FirstInv.terminal {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {cs : List Nat} {st : SearchSt n} {trail : FrameTrail} (hn0 : 0 < n) (hlevel : level = cs.length + 1) (h : FirstInv G ctx level cs numcells st trail) : have rs := refine ctx level st.lab st.ptn st.active numcells; have full := cs ++ [rs.longcode]; RunInv G ctx tcLevel level full full full rs.numcells (firstterminal level (firstLeafSt ctx level numcells st)) (some (pathLeafKey ctx full rs.lab)) trail

Reaching a discrete node installs the first leaf and enters the stable post-incumbent invariant.

theorem Hex.GraphIso.Nauty.FirstInv.terminalReceipt {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {cs : List Nat} {st : SearchSt n} {trail : FrameTrail} (hn0 : 0 < n) (hlevel : level = cs.length + 1) (h : FirstInv G ctx level cs numcells st trail) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) : have rs := refine ctx level st.lab st.ptn st.active numcells; have full := cs ++ [rs.longcode]; have out := firstPathNode ctx inf tcLevel (fuel + 1) level numcells st; NodeReceipt trail ctx tcLevel (specFuel + 1) (fuel + 1) level cs st out.snd numcells none (some (pathLeafKey ctx full rs.lab)) out.fst ∧ RunInv G ctx tcLevel level full full full rs.numcells out.snd (some (pathLeafKey ctx full rs.lab)) trail

A discrete node on the first descent returns an exact located receipt and the stable state installed by that leaf.

theorem Hex.GraphIso.Nauty.worksetOf_eq_windowSet {n : Nat} (lab : Array Nat) (tc len : Nat) (hlen : 1 ≤ len) : worksetOf n lab tc (tc + len - 1) = windowSet n lab tc len

The target-cell representation used by maketargetcell is the same bitset as the length-indexed window representation used by sweep coverage.

theorem Hex.GraphIso.Nauty.RunPrep.setTctotal {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells value : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunPrep G ctx tcLevel level codes bs fs numcells st best trail) : RunPrep G ctx tcLevel level codes bs fs 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 := 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 := value, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } best trail

Charging target-cell statistics changes no logical search field.

theorem Hex.GraphIso.Nauty.RunInv.park {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunInv G ctx tcLevel level codes bs fs numcells st best trail) (hcheap : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) 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 := level + 1, 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 }) : RunInv G ctx tcLevel level codes bs fs 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 := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := level + 1, 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 } best trail

Parking the cheap-automorphism boundary changes only the CheapOk component of the stable invariant.

structure Hex.GraphIso.Nauty.FrameRefs {n : Nat} (ctx : Ctx n) (tcLevel specFuel level : Nat) (codes : List Nat) (rsLab rsPtn : Array Nat) (tc len numcells : Nat) (st : SearchSt n) (best : Option (Key n)) : Prop

First and canonical controls that point at the current loop level are backed by children already absorbed into the semantic incumbent.

• first : st.gcaFirst = level → ∃ (o : Nat), o < len ∧ ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells best o ∧ st.firstlab[tc]! = rsLab[tc + o]! ∧ cellsPerm rsPtn level rsLab st.firstlab
• canon : st.gcaCanon = level → ∃ (o : Nat), o < len ∧ ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells best o ∧ st.canonlab[tc]! = rsLab[tc + o]! ∧ cellsPerm rsPtn level rsLab st.canonlab

theorem Hex.GraphIso.Nauty.FrameRefs.grow {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {codes : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {st : SearchSt n} {best best' : Option (Key n)} (h : FrameRefs ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells st best) (hinc : IncGrows best best') : FrameRefs ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells st best'

Frame references survive an incumbent increase.

theorem Hex.GraphIso.Nauty.SearchOut.recoverOk {n k : Nat} {G : Colored n k} {level numcells inf : Nat} {base out : SearchSt n} (hinf : inf = n + 2) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells base) (hout : SearchOut G level level base out) : SearchOut G level level base (recover n inf level out) ∧ SearchOk G level numcells (recover n inf level out)

Recovering a state related to a valid loop entry restores the full parent invariant as well as the composable parent-level effect.

structure Hex.GraphIso.Nauty.LoopInv {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel specFuel level : Nat) (codes bs fs : List Nat) (numcells : Nat) (rsLab rsPtn : Array Nat) (tc len : Nat) (tcell : VSet n) (cursor : Option Nat) (base st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) : Prop

Invariant of one imperative child loop. base is the refined state whose labelling and partition were frozen for specNode. st is the current recovered state after zero or more children and pruning steps.

• nonempty : 0 < n
• positive : 1 ≤ level
• baseOk : SearchOk G level numcells base
• run : RunInv G ctx tcLevel level codes bs fs numcells st best trail
• effect : SearchOut G level level base st
• baseLab : base.lab = rsLab
• basePtn : base.ptn = rsPtn
• equitable : Equitable ctx level rsLab rsPtn
• cell : IsCell rsPtn level tc len
• lenTwo : 2 ≤ len
• range : tc + len ≤ n
• values (q : Nat) : rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2
• members (v : Nat) : tcell.mem v = true → v ∈ segN rsLab tc len
• cover : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell cursor best
• refs : FrameRefs ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells st best
• shortClear : st.needshortprune = false
• fuelBound : level + 1 + specFuel ≤ n + 1

theorem Hex.GraphIso.Nauty.LoopInv.start {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hlevel : 1 ≤ level) (h : RunInv G ctx tcLevel level codes bs fs numcells st best trail) (hfirst : st.gcaFirst < level) (hcanon : st.gcaCanon < level) (heq : Equitable ctx level st.lab st.ptn) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (hvals : ∀ (q : Nat), st.ptn[q]! ≤ level ∨ st.ptn[q]! = n + 2) (hshort : st.needshortprune = false) (hfuel : level + 1 + specFuel ≤ n + 1) : LoopInv G ctx tcLevel specFuel level codes bs fs numcells st.lab st.ptn tc len (windowSet n st.lab tc len) none st st best trail

A fresh sweep freezes the current equitable target-cell frame. The strict guide bounds make current-level frame references vacuous before the first child is explored.

theorem Hex.GraphIso.Nauty.LoopInv.frozenLabSize {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) : rsLab.size = n

theorem Hex.GraphIso.Nauty.LoopInv.frozenPtnSize {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) : rsPtn.size = n

theorem Hex.GraphIso.Nauty.LoopInv.frozenLabOk {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) : LabOk rsLab n

theorem Hex.GraphIso.Nauty.LoopInv.frozenEnd {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) : rsPtn[rsPtn.size - 1]! ≤ level

theorem Hex.GraphIso.Nauty.LoopInv.frozenVals {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (q : Nat) : rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2

theorem Hex.GraphIso.Nauty.LoopInv.ptnEq {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) : st.ptn = rsPtn

The current recovered partition is exactly the frozen partition.

theorem Hex.GraphIso.Nauty.LoopInv.labPerm {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) : cellsPerm rsPtn level rsLab st.lab

Recovery may reorder a cell, but cannot change its vertex set.

theorem Hex.GraphIso.Nauty.LoopInv.currentEquitable {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) : Equitable ctx level st.lab st.ptn

theorem Hex.GraphIso.Nauty.LoopInv.currentCell {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) : IsCell st.ptn level tc len

theorem Hex.GraphIso.Nauty.LoopInv.recoverChild {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {currentOffset inf : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st out : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hinf : inf = n + 2) (hcurrent : currentOffset < len) (hout : SearchOut G level (level + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + currentOffset]!, 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 } out) : have cleaned := { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase st.lab[tc + currentOffset]!, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }; have recovered := recover n inf level cleaned; SearchOut G level level base recovered ∧ SearchOk G level numcells recovered

A recursive child effect, followed by temporary fixed-point cleanup and recover, composes back into the frozen parent frame.

theorem Hex.GraphIso.Nauty.LoopInv.nextOffsets {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {tv : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hnext : tcell.nextElem cursor = some tv) : ∃ (offset : Nat), ∃ (currentOffset : Nat), offset < len ∧ currentOffset < len ∧ rsLab[tc + offset]! = tv ∧ st.lab[tc + currentOffset]! = tv

A vertex selected from the mutable bitset has both its frozen specification offset and its current executable offset.

theorem Hex.GraphIso.Nauty.LoopInv.nextLt {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {tv : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hnext : tcell.nextElem cursor = some tv) : tv < n

Every vertex returned by a verified sibling sweep lies in the graph vertex range. This is the cursor bound used by the fuel induction, and it is derived from the frozen target-cell membership rather than from the mutable bitset alone.

theorem Hex.GraphIso.Nauty.LoopInv.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {tv coset : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hnext : tcell.nextElem cursor = some tv) (hcheap : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) (level + 1) st) : ∃ (offset : Nat), ∃ (currentOffset : Nat), offset < len ∧ currentOffset < len ∧ rsLab[tc + offset]! = tv ∧ st.lab[tc + currentOffset]! = tv ∧ NodeInv G ctx tcLevel (level + 1) codes bs fs (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + currentOffset]!, 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 (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })

The next mutable-loop selection enters a valid recursive node while recording the corresponding frozen specification offset in the trail.

theorem Hex.GraphIso.Nauty.LoopInv.NodeInv.otherSweep {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (h : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells ≠ n) (hgate : (otherLeafSt ctx level numcells st).eqlevFirst = level ∨ (otherLeafSt ctx level numcells st).compCanon ≥ 0) (hfuel : level + 1 + specFuel ≤ n + 1) : have r := refine ctx level st.lab st.ptn st.active numcells; have full := codes ++ [r.longcode]; have pre := otherLeafSt ctx level numcells st; ∃ (tc : Nat), ∃ (len : Nat), have tcell := worksetOf n r.lab tc (tc + len - 1); have base := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + len, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; have start := if cheapautom base.ptn level n = true then base else { lab := base.lab, ptn := base.ptn, active := base.active, orbits := base.orbits, fixedpts := base.fixedpts, autos := base.autos, wsCap := base.wsCap, firstcode := base.firstcode, canoncode := base.canoncode, firsttc := base.firsttc, firstlab := base.firstlab, canonlab := base.canonlab, canong := base.canong, samerows := base.samerows, compCanon := base.compCanon, eqlevFirst := base.eqlevFirst, eqlevCanon := base.eqlevCanon, gcaFirst := base.gcaFirst, gcaCanon := base.gcaCanon, canonlevel := base.canonlevel, noncheaplevel := level + 1, allsamelevel := base.allsamelevel, cosetindex := base.cosetindex, stabvertex := base.stabvertex, needshortprune := base.needshortprune, numnodes := base.numnodes, tctotal := base.tctotal, canupdates := base.canupdates, numorbits := base.numorbits, numgenerators := base.numgenerators, numbadleaves := base.numbadleaves, maxlevel := base.maxlevel, genTrace := base.genTrace }; maketargetcell ctx r.lab r.ptn level tcLevel (-1) = (tc, tcell, len) ∧ processnode ctx level r.numcells base = (Int.ofNat level, base) ∧ nodeKey ctx tcLevel (specFuel + 1) level codes st numcells = keysMax (sweepKey ctx tcLevel specFuel level full r.lab r.ptn tc r.numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level full r.lab r.ptn tc r.numcells (o + 1)) (List.range (len - 1))) ∧ LoopInv G ctx tcLevel specFuel level full bs fs r.numcells r.lab r.ptn tc len tcell none start start best trail

An internal off-path node reaches a fresh verified child sweep after the executable refinement, comparison, target-accounting, and cheap-rule bookkeeping. The returned target is simultaneously the executable and specification target, so the accompanying equality exposes the whole node key as this sweep's bound.

theorem Hex.GraphIso.Nauty.LoopInv.otherNode_park_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n) (hnonneg : have r := refine ctx level st.lab st.ptn st.active numcells; have pre := otherNodePrep level r.longcode { lab := r.lab, ptn := r.ptn, active := r.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 + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; pre.compCanon ≥ 0) (hshort : have r := refine ctx level st.lab st.ptn st.active numcells; have pre := otherNodePrep level r.longcode { lab := r.lab, ptn := r.ptn, active := r.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 + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; have mt := maketargetcell ctx pre.lab pre.ptn level tcLevel (-1); have base := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + mt.snd.snd, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; (processnode ctx level r.numcells base).snd.needshortprune = false) (hcheap : have r := refine ctx level st.lab st.ptn st.active numcells; have pre := otherNodePrep level r.longcode { lab := r.lab, ptn := r.ptn, active := r.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 + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; have mt := maketargetcell ctx pre.lab pre.ptn level tcLevel (-1); have base := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + mt.snd.snd, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; cheapautom (processnode ctx level r.numcells base).snd.ptn level n = false) : have r := refine ctx level st.lab st.ptn st.active numcells; have pre := otherNodePrep level r.longcode { lab := r.lab, ptn := r.ptn, active := r.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 + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; have mt := maketargetcell ctx pre.lab pre.ptn level tcLevel (-1); have base := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + mt.snd.snd, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; have pr := processnode ctx level r.numcells base; have parked := have __src := pr.snd; { 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 := level + 1, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace }; have L := otherChildLoop ctx inf tcLevel fuel (n + 1) level r.numcells mt.fst ((mt.snd.fst.nextElem none).getD 0) (mt.snd.fst.nextElem none) mt.snd.fst parked; otherNode ctx inf tcLevel (fuel + 1) level numcells st = if pr.fst < Int.ofNat level then pr else match L.fst with | some rtn => (rtn, L.snd) | none => (Int.ofNat level - 1, L.snd)

The nonnegative internal branch with a failed cheap-automorphism test parks the boundary before entering its child loop.