def Hex.GraphIso.Nauty.FixedCells {n : Nat} (level : Nat) (st : SearchSt n) : Prop

Every vertex recorded as fixed occupies a singleton cell of the current partition. This is the executable path fact that makes erasing a completed child's temporary fixed vertex restore its parent set exactly.

Equations

• Hex.GraphIso.Nauty.FixedCells level st = ∀ (v : Nat), v < n → st.fixedpts.mem v = true → ∃ (q : Nat), q < n ∧ st.lab[q]! = v ∧ Hex.GraphIso.Nauty.IsCell st.ptn level q 1

theorem Hex.GraphIso.Nauty.FixedCells.root {n k : Nat} {G : Colored n k} : FixedCells 1 (rootSt n (initialPartition G).fst (initialPartition G).snd)

The initial search has no fixed vertices.

theorem Hex.GraphIso.Nauty.FixedCells.fresh {n level tc len o : Nat} {st : SearchSt n} (h : FixedCells level st) (hok : LabOk st.lab n) (hinj : LabInj st.lab n) (hsize : st.lab.size = n) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) : st.fixedpts.mem st.lab[tc + o]! = false

A vertex in a non-singleton target cell is not already fixed.

theorem Hex.GraphIso.Nauty.FixedCells.ofCellsPerm {n level : Nat} {st out : SearchSt n} (h : FixedCells level st) (hfixed : out.fixedpts = st.fixedpts) (hptn : out.ptn = st.ptn) (hperm : cellsPerm st.ptn level st.lab out.lab) : FixedCells level out

Reordering vertices within unchanged cells preserves fixed singletons.

theorem Hex.GraphIso.Nauty.FixedCells.ofSearchOut {n k : Nat} {G : Colored n k} {level numcells : Nat} {st out : SearchSt n} (h : FixedCells level st) (hfixed : out.fixedpts = st.fixedpts) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (heffect : SearchOut G level level st out) : FixedCells level out

A parent-level search effect preserves fixed singletons when it preserves the fixed-point bitset.

theorem Hex.GraphIso.Nauty.FixedCells.refine {n : Nat} {ctx : Ctx n} {level : Nat} {active : VSet n} {numcells : Nat} {st : SearchSt n} (h : FixedCells level st) (hsize : st.lab.size = n) (hpsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : FixedCells level { lab := (Nauty.refine ctx level st.lab st.ptn active numcells).lab, ptn := (Nauty.refine ctx level st.lab st.ptn active numcells).ptn, active := (Nauty.refine ctx level st.lab st.ptn active numcells).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 }

Refinement preserves every existing fixed singleton.

theorem Hex.GraphIso.Nauty.FixedCells.breakout {n level tc len o : Nat} {st : SearchSt n} (h : FixedCells level st) (hinj : LabInj st.lab n) (hsize : st.lab.size = n) (hpsize : st.ptn.size = n) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) : FixedCells (level + 1) { lab := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (Nauty.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 := 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 }

Individualizing a fresh target vertex adds exactly one fixed singleton and preserves every older fixed singleton.

theorem Hex.GraphIso.Nauty.fixTest_mono {n : Nat} {small large fix : VSet n} (hsub : ∀ (v : Nat), small.mem v = true → large.mem v = true) (hfix : large.subset fix = true) : small.subset fix = true

Passing a fix test for a larger fixed set implies passing it for any pointwise smaller set.

def Hex.GraphIso.Nauty.LocalAutos {n : Nat} (ctx : Ctx n) (level : Nat) (st : SearchSt n) : Prop

The bounded automorphism workspace is valid at the current frame for every entry whose fixed set covers the current search path.

Equations

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

theorem Hex.GraphIso.Nauty.LocalAutos.empty {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} (h : st.autos = #[]) : LocalAutos ctx level st

An empty workspace is locally valid.

theorem Hex.GraphIso.Nauty.LocalAutos.reindexStab {ptn lab lab' gamma : Array Nat} {level n : Nat} (h : CellStab ptn level lab gamma) (hperm : cellsPerm ptn level lab lab') (hpsize : ptn.size = n) (hsize : lab.size = n) (hsize' : lab'.size = n) (hend : ptn[ptn.size - 1]! ≤ level) : CellStab ptn level lab' gamma

Cell stabilization is independent of the ordering chosen inside each cell.

theorem Hex.GraphIso.Nauty.LocalAutos.reindexPair {n : Nat} {ctx : Ctx n} {ptn lab lab' : Array Nat} {level : Nat} {fix mcr : VSet n} (h : PairOk ctx.g ptn lab level fix mcr) (hperm : cellsPerm ptn level lab lab') (hpsize : ptn.size = n) (hsize : lab.size = n) (hsize' : lab'.size = n) (hend : ptn[ptn.size - 1]! ≤ level) : PairOk ctx.g ptn lab' level fix mcr

A locally valid pair remains valid after reordering the frame within its cells.

theorem Hex.GraphIso.Nauty.LocalAutos.ofCellsPerm {n : Nat} {ctx : Ctx n} {level : Nat} {st out : SearchSt n} (h : LocalAutos ctx level st) (hautos : out.autos = st.autos) (hfixed : out.fixedpts = st.fixedpts) (hptn : out.ptn = st.ptn) (hperm : cellsPerm st.ptn level st.lab out.lab) (hpsize : st.ptn.size = n) (hsize : st.lab.size = n) (hsize' : out.lab.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : LocalAutos ctx level out

Local ledger validity transports across unchanged partition cells and a within-cell labelling permutation.

theorem Hex.GraphIso.Nauty.LocalAutos.breakout {n : Nat} {ctx : Ctx n} {level tc len o : Nat} {st : SearchSt n} (h : LocalAutos ctx level st) (hcell : IsCell st.ptn level tc len) (hrange : tc + len ≤ st.ptn.size) (hsize : st.lab.size = st.ptn.size) (hlab : LabOk st.lab n) (ho : o < len) (hlen : 2 ≤ len) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), st.ptn[q]! ≠ level + 1) : LocalAutos ctx (level + 1) { lab := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (Nauty.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 := 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 }

The conditional local ledger descends through one individualization. A pair applicable to the enlarged fixed set fixes the selected vertex, exactly the premise needed by cellStab_breakout.

theorem Hex.GraphIso.Nauty.LocalAutos.refine {n : Nat} {ctx : Ctx n} {level : Nat} {active : VSet n} {numcells : Nat} {st : SearchSt n} (h : LocalAutos ctx level st) (hgsz : ctx.g.size = n) (hsize : st.lab.size = n) (hlab : LabOk st.lab n) (hpsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level) : LocalAutos ctx level { lab := (Nauty.refine ctx level st.lab st.ptn active numcells).lab, ptn := (Nauty.refine ctx level st.lab st.ptn active numcells).ptn, active := (Nauty.refine ctx level st.lab st.ptn active numcells).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 }

The conditional local ledger is preserved by equitable refinement.

def Hex.GraphIso.Nauty.PathStab {n : Nat} (ctx : Ctx n) (rootPtn rootLab : Array Nat) (level : Nat) (st : SearchSt n) : Prop

A root-stabilizing checked automorphism that fixes every vertex on the current individualized path stabilizes the current partition. Keeping the root frame explicit lets the existing root autos ledger supply the same witness at every pruning site.

Equations

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

theorem Hex.GraphIso.Nauty.PathStab.same {n : Nat} {ctx : Ctx n} {st : SearchSt n} : PathStab ctx st.ptn st.lab 1 st

A frame is its own path-stabilization seed.

theorem Hex.GraphIso.Nauty.PathStab.ofCellsPerm {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {st out : SearchSt n} (h : PathStab ctx rootPtn rootLab level st) (hfixed : out.fixedpts = st.fixedpts) (hptn : out.ptn = st.ptn) (hperm : cellsPerm st.ptn level st.lab out.lab) (hpsize : st.ptn.size = n) (hsize : st.lab.size = n) (hsize' : out.lab.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : PathStab ctx rootPtn rootLab level out

Reordering the current labelling within unchanged cells preserves path stabilization.

theorem Hex.GraphIso.Nauty.PathStab.ofSearchOut {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level numcells : Nat} {st out : SearchSt n} (h : PathStab ctx rootPtn rootLab level st) (hfixed : out.fixedpts = st.fixedpts) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (heffect : SearchOut G level level st out) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : PathStab ctx rootPtn rootLab level out

A parent-level search effect preserves path stabilization when it restores the parent's fixed-point set.

theorem Hex.GraphIso.Nauty.PathStab.refine {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {active : VSet n} {numcells : Nat} {st : SearchSt n} (h : PathStab ctx rootPtn rootLab level st) (hgsz : ctx.g.size = n) (hsize : st.lab.size = n) (hlab : LabOk st.lab n) (hpsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level) : PathStab ctx rootPtn rootLab level { lab := (Nauty.refine ctx level st.lab st.ptn active numcells).lab, ptn := (Nauty.refine ctx level st.lab st.ptn active numcells).ptn, active := (Nauty.refine ctx level st.lab st.ptn active numcells).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 }

Equitable refinement preserves path stabilization.

theorem Hex.GraphIso.Nauty.PathStab.breakout {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level tc len o : Nat} {st : SearchSt n} (h : PathStab ctx rootPtn rootLab level st) (hcell : IsCell st.ptn level tc len) (hrange : tc + len ≤ st.ptn.size) (hsize : st.lab.size = st.ptn.size) (hlab : LabOk st.lab n) (ho : o < len) (hlen : 2 ≤ len) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), st.ptn[q]! ≠ level + 1) : PathStab ctx rootPtn rootLab (level + 1) { lab := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (Nauty.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 := 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 }

Individualization extends path stabilization because an automorphism fixing the enlarged path fixes the selected target vertex.

theorem Hex.GraphIso.Nauty.PathStab.toLocal {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {st : SearchSt n} (h : PathStab ctx rootPtn rootLab level st) (hroot : AutosOk ctx.g rootPtn rootLab 1 st.autos) : LocalAutos ctx level st

The root autos ledger and path stabilization reconstruct the conditional ledger consumed by the two pruning filters.

theorem Hex.GraphIso.Nauty.pushAuto_fixedpts {n : Nat} (st : SearchSt n) (pair : VSet n × VSet n) : (pushAuto st pair).fixedpts = st.fixedpts

theorem Hex.GraphIso.Nauty.processnode_fixedpts {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (processnode ctx level numcells st).snd.fixedpts = st.fixedpts

Leaf processing never changes the individualized path.

theorem Hex.GraphIso.Nauty.otherNodePrep_fixedpts {n : Nat} (level code : Nat) (st : SearchSt n) : (otherNodePrep level code st).fixedpts = st.fixedpts

Comparison preparation never changes the individualized path.

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

Recovery never changes the individualized path.

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

First-leaf installation never changes the individualized path.

theorem Hex.GraphIso.Nauty.firstFinish_fixedpts {n : Nat} (level size index : Nat) (st : SearchSt n) : (firstFinish level size index st).fixedpts = st.fixedpts

First-path sweep cleanup never changes the individualized path.

structure Hex.GraphIso.Nauty.PathOk {n : Nat} (ctx : Ctx n) (rootPtn rootLab : Array Nat) (level : Nat) (st : SearchSt n) : Prop

The two path facts carried by the mutual induction: fixed vertices are singleton cells, and root-valid automorphisms fixing them stabilize the current cells.

• fixed : FixedCells level st
• stab : PathStab ctx rootPtn rootLab level st

theorem Hex.GraphIso.Nauty.PathOk.root {n k : Nat} {G : Colored n k} : PathOk { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (rootSt n (initialPartition G).fst (initialPartition G).snd)

The nonempty root seeds both path facts.

theorem Hex.GraphIso.Nauty.PathOk.refine {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {active : VSet n} {numcells : Nat} {st : SearchSt n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hgsz : ctx.g.size = n) (hok : SearchOk G level numcells st) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level) (h : PathOk ctx rootPtn rootLab level st) : PathOk ctx rootPtn rootLab level { lab := (Nauty.refine ctx level st.lab st.ptn active numcells).lab, ptn := (Nauty.refine ctx level st.lab st.ptn active numcells).ptn, active := (Nauty.refine ctx level st.lab st.ptn active numcells).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 }

Node-entry refinement preserves both path facts.

theorem Hex.GraphIso.Nauty.PathOk.breakout {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rootPtn rootLab rsLab rsPtn : Array Nat} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {currentOffset : Nat} {codes bs fs : List Nat} {cursor : Option Nat} {base st : 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) (hcurrent : currentOffset < len) (h : PathOk ctx rootPtn rootLab level st) : PathOk ctx rootPtn rootLab (level + 1) { lab := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst, ptn := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.fst, active := (Nauty.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 }

A loop child extends both path facts by its selected fresh vertex.

theorem Hex.GraphIso.Nauty.PathOk.ofSearchOut {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level numcells : Nat} {st out : SearchSt n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (h : PathOk ctx rootPtn rootLab level st) (hfixed : out.fixedpts = st.fixedpts) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (heffect : SearchOut G level level st out) : PathOk ctx rootPtn rootLab level out

Recovered parent state preserves both path facts once child cleanup restores the parent's fixed-point set.

theorem Hex.GraphIso.Nauty.PathOk.autos {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells tcLevel : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st) (hrun : RunInv G ctx tcLevel level cs bs fs numcells st best trail) : LocalAutos ctx level st

The path facts and root ledger supply the exact local ledger needed by a pruning filter.

theorem Hex.GraphIso.Nauty.PathOk.pair {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {fix mcr : VSet n} (hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st) (hroot : PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 fix mcr) (hcovers : ∀ (v : Nat), v < n → st.fixedpts.mem v = true → fix.mem v = true) : PairOk ctx.g st.ptn st.lab level fix mcr

A root-valid pair whose fix contains the individualized path is valid at the current search frame, even when that pair was admitted by a deeper result state rather than being present on entry.

structure Hex.GraphIso.Nauty.Live {n : Nat} (ctx : Ctx n) (level : Nat) (st : SearchSt n) (trail : FrameTrail) : Prop

Reference history, ordered live guides, and stabilization of every ancestor frame to which the current node may return.

• history : RefTrail ctx level st trail
• order : st.gcaFirst ≤ st.gcaCanon
• stable : ReturnStab trail (Int.ofNat st.gcaFirst) st

theorem Hex.GraphIso.Nauty.Live.stateEq {n : Nat} {ctx : Ctx n} {level : Nat} {st st' : SearchSt n} {trail : FrameTrail} (h : Live ctx level st trail) (hfirstGca : st'.gcaFirst = st.gcaFirst) (hfirst : st'.firstlab = st.firstlab) (hcanonGca : st'.gcaCanon = st.gcaCanon) (hcanon : st'.canonlab = st.canonlab) (hgen : st'.genTrace = st.genTrace) : Live ctx level st' trail

Live depends only on the two reference controls and labellings and on the recorded-generator store.

theorem Hex.GraphIso.Nauty.Live.setTctotal {n : Nat} {ctx : Ctx n} {level value : Nat} {st : SearchSt n} {trail : FrameTrail} (h : Live ctx level st trail) : Live ctx 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, 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 } trail

Target-cell accounting changes no live field.

theorem Hex.GraphIso.Nauty.Live.park {n : Nat} {ctx : Ctx n} {level boundary : Nat} {st : SearchSt n} {trail : FrameTrail} (h : Live ctx level st trail) : Live ctx 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 := 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 } trail

Parking the cheap-automorphism boundary changes no live field.

theorem Hex.GraphIso.Nauty.Live.setFixed {n : Nat} {ctx : Ctx n} {level : Nat} {fixedpts : VSet n} {st : SearchSt n} {trail : FrameTrail} (h : Live ctx level st trail) : Live ctx level { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := 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 } trail

Fixed-point cleanup changes no live field.

theorem Hex.GraphIso.Nauty.Live.clearShort {n : Nat} {ctx : Ctx n} {level : Nat} {st : SearchSt n} {trail : FrameTrail} (h : Live ctx level st trail) : Live ctx 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 } trail

Clearing the one-shot short-prune flag changes no live field.

theorem Hex.GraphIso.Nauty.Live.otherLeaf {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} {trail : FrameTrail} (h : Live ctx level st trail) : Live ctx level (otherLeafSt ctx level numcells st) trail

Refinement and the off-path comparison step preserve the complete live package.

theorem Hex.GraphIso.Nauty.Live.processnode {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} {trail : FrameTrail} (h : Live ctx level st trail) (htrail : TrailOk ctx level st trail) (hfirst : st.gcaFirst ≤ level) : RefTrail ctx level (Nauty.processnode ctx level numcells st).snd trail ∧ (Nauty.processnode ctx level numcells st).snd.gcaFirst ≤ (Nauty.processnode ctx level numcells st).snd.gcaCanon

A leaf event preserves reference history and live GCA ordering. Its return-indexed generator stabilization is supplied separately by the admission classifier.

theorem Hex.GraphIso.Nauty.Live.rowTiePair {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} {entry : TrailEntry} (hn0 : 0 < n) (hprep : RunPrep G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) (hbelow : st.gcaCanon < level) (htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) (hentry : trail st.gcaCanon = some entry) : PairOk ctx.g entry.frame.rsPtn entry.frame.rsLab st.gcaCanon (fmperm (canonScatter n st.canonlab st.lab) n).fst (fmperm (canonScatter n st.canonlab st.lab) n).snd

The explicit pair admitted by a code-two row tie is valid at its canonical return frame, not merely at the root ledger. This is the local fact consumed when the one-shot short-prune flag reaches that frame.

theorem Hex.GraphIso.Nauty.RunPrep.rowTieBack {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 : RunPrep G ctx tcLevel level codes bs fs numcells st best trail) (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.back? = some (fmperm (canonScatter n st.canonlab st.lab) n)

Workspace capacity makes the code-two pair the exact final entry read by shortprune, including the full-workspace overwrite case.

structure Hex.GraphIso.Nauty.OtherLive {n : Nat} (ctx : Ctx n) (level : Nat) (st : SearchSt n) (trail : FrameTrail) extends Hex.GraphIso.Nauty.Live ctx level st trail : Prop

The live state of an off-path sweep. gcaFirst stays strictly above the divergence ancestor, so a child push requires no new stabilization at the current frame.

• history : RefTrail ctx level st trail
• order : st.gcaFirst ≤ st.gcaCanon
• stable : ReturnStab trail (Int.ofNat st.gcaFirst) st
• firstBelow : st.gcaFirst < level

structure Hex.GraphIso.Nauty.FirstLive {n : Nat} (ctx : Ctx n) (level : Nat) (st : SearchSt n) (trail : FrameTrail) (rsLab rsPtn : Array Nat) extends Hex.GraphIso.Nauty.Live ctx level st trail : Prop

The live state of a first-path sweep. Once generators exist, the guiding child has already been absorbed, and every recorded generator stabilizes this frozen frame. Before that point the store is empty and the same clause holds vacuously.

• history : RefTrail ctx level st trail
• order : st.gcaFirst ≤ st.gcaCanon
• stable : ReturnStab trail (Int.ofNat st.gcaFirst) st
• frameStab (γ : Array Nat) : γ ∈ st.genTrace.toList → CellStab rsPtn level rsLab γ

theorem Hex.GraphIso.Nauty.OtherOutcome.recover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel childNumcells numcells level inf : Nat} {fixedpts : VSet n} {codes fs : List Nat} {child out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Int} (h : OtherOutcome G ctx tcLevel specFuel runFuel (level + 1) codes fs child out childNumcells best outBest receiptTrail eventTrail r) (hreturn : r = Int.ofNat level) (hpath : codes.length = level) (hlevel : 1 ≤ level) (hinf : level < inf) (hfirst : child.gcaFirst < level) (hok : SearchOk G level numcells (Nauty.recover n inf level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := fixedpts, 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 })) : ∃ (bs : List Nat), RunInv G ctx tcLevel level codes bs fs numcells (Nauty.recover n inf level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := fixedpts, 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 }) outBest eventTrail ∧ OtherLive ctx level (Nauty.recover n inf level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := fixedpts, 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 }) eventTrail

Cleaning and recovering a completed off-path child reconstructs both the parent's stable run invariant and its off-path live package.

theorem Hex.GraphIso.Nauty.OtherOutcome.cover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tc len : Nat} {tcell : VSet n} {tv offset : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st child out : SearchSt n} {best outBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (h : OtherOutcome G ctx tcLevel specFuel runFuel (level + 1) codes fs child out (numcells + 1) best outBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (hfuel : runFuel ≠ 0) (hstay : ¬r < Int.ofNat level) (hnext : tcell.nextElem cursor = some tv) (hoffset : offset < len) (htv : rsLab[tc + offset]! = tv) (hfirst : child.gcaFirst < level) (heq : ∀ (o : Nat), o < len → rsLab[tc + o]! = tv → sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells o = nodeKey ctx tcLevel specFuel (level + 1) codes child (numcells + 1)) : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) outBest

Resolving a returning off-path child advances the evolving sweep. The impossible orbit-return arm is discharged by the strict first-guide bound, so no current-child cosetindex equation is needed.

theorem Hex.GraphIso.Nauty.OtherOutcome.refs {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tc len tv offset currentOffset inf : Nat} {tcell fixedpts : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st out : SearchSt n} {best outBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hlive : OtherLive ctx level st trail) (h : OtherOutcome G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 (numcells + 1) best outBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (hcover : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) outBest) (hfuel : runFuel ≠ 0) (hnext : tcell.nextElem cursor = some tv) (hoffset : offset < len) (hcurrent : currentOffset < len) (htv : rsLab[tc + offset]! = tv) (hat : st.lab[tc + currentOffset]! = tv) : FrameRefs ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells (Nauty.recover n inf level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := fixedpts, 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 }) outBest

After recovery, the first guide remains strictly older and the canonical guide names either an earlier covered child or the child just absorbed. Both current-frame reference conditions therefore hold again.

theorem Hex.GraphIso.Nauty.OtherOutcome.next {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tc len tv offset currentOffset inf : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st out : SearchSt n} {best outBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hlive : OtherLive ctx level st trail) (h : OtherOutcome G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 (numcells + 1) best outBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (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) (hinf : inf = n + 2) (hpath : codes.length = level) (hfuel : runFuel ≠ 0) (hstay : ¬r < Int.ofNat level) (hnext : tcell.nextElem cursor = some tv) (hoffset : offset < len) (hcurrent : currentOffset < len) (htv : rsLab[tc + offset]! = tv) (hat : st.lab[tc + currentOffset]! = tv) (heq : ∀ (o : Nat), o < len → rsLab[tc + o]! = tv → sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells o = nodeKey ctx tcLevel specFuel (level + 1) codes { 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 } (numcells + 1)) (hshort : out.needshortprune = false) : have cleaned := { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, 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 := Nauty.recover n inf level cleaned; ∃ (bs' : List Nat), LoopInv G ctx tcLevel specFuel level codes bs' fs numcells rsLab rsPtn tc len tcell (some tv) base recovered outBest eventTrail ∧ OtherLive ctx level recovered eventTrail

An ordinary off-path child return with no requested pruning rebuilds the complete invariant for the recursive tail of the same sweep.

theorem Hex.GraphIso.Nauty.NodeInv.otherLive {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells len : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : have pre := otherLeafSt ctx level numcells st; 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 }; OtherLive ctx level start trail

The bookkeeping between an off-path node's refinement and its fresh child sweep preserves the live package and the strict first-reference bound.

theorem Hex.GraphIso.Nauty.LoopInv.childLive {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {coset : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : 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) (hlive : Live ctx level st trail) (offset currentOffset : Nat) (hframe : st.gcaFirst = level → ∀ (γ : Array Nat), γ ∈ st.genTrace.toList → CellStab rsPtn level rsLab γ) : Live ctx (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 := 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 } (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })

A loop child inherits reference history and stabilization through its live first-reference GCA. The current frozen frame is required only when that GCA is exactly the loop level.

theorem Hex.GraphIso.Nauty.LoopInv.otherChildLive {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} (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hlive : OtherLive ctx level st trail) (offset currentOffset : Nat) : Live ctx (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 } (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })

An off-path loop's strict first-reference bound discharges the only new-frame premise of childLive.

theorem Hex.GraphIso.Nauty.LoopInv.firstChildLive {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {coset : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : 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) (hlive : FirstLive ctx level st trail rsLab rsPtn) (offset currentOffset : Nat) : Live ctx (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 := 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 } (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })

A first-path loop carries stabilization of its frozen frame directly, including the initial empty-store phase.

theorem Hex.GraphIso.Nauty.RunPrep.leafEvent {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {stem codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hbound : st.noncheaplevel ≤ level) (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hreturn : (processnode ctx level numcells st).fst ≤ Int.ofNat level - 1) (hgen : (processnode ctx level numcells st).snd.genTrace = st.genTrace) (hprep : RunPrep G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : ∃ (bs' : List Nat), EventOut G ctx tcLevel stem fs (processnode ctx level numcells st).snd (some (incKey ctx bs' (processnode ctx level numcells st).snd.canonlab)) trail (processnode ctx level numcells st).fst ∧ incKey ctx bs' (processnode ctx level numcells st).snd.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx codes st.lab)

A non-first leaf event whose branch does not append a generator produces the complete result-side package. The caller supplies the strict return bound because processnode itself also has a non-unwinding result at the current level.

theorem Hex.GraphIso.Nauty.RunPrep.firstEvent {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {stem codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hbelow : st.gcaFirst < level) (hnp : st.compCanon ≤ 0) (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) (hprep : RunPrep G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : EventOut G ctx tcLevel stem fs (processnode ctx level numcells st).snd best trail (processnode ctx level numcells st).fst

A code-one admission with a nonpositive incumbent comparison is a fully verified generator event. The semantic loop proof supplies the nonpositivity premise from coverage of the guiding child.

theorem Hex.GraphIso.Nauty.RunPrep.tiedEvent {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {stem codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hbound : st.noncheaplevel ≤ level) (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) (hcanonBelow : st.gcaCanon < level) (hprep : RunPrep G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : ∃ (bs' : List Nat), EventOut G ctx tcLevel stem fs (processnode ctx level numcells st).snd (some (incKey ctx bs' (processnode ctx level numcells st).snd.canonlab)) trail (processnode ctx level numcells st).fst ∧ incKey ctx bs' (processnode ctx level numcells st).snd.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx codes st.lab) ∧ some (incKey ctx bs' (processnode ctx level numcells st).snd.canonlab) = best

A code-two row tie produces a verified event for either its canonical return or its special first-ancestor orbit return.

theorem Hex.GraphIso.Nauty.NodeInv.firstLeaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hnp : (otherLeafSt ctx level numcells st).compCanon ≤ 0) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hsent : (otherLeafSt ctx level numcells st).firstcode[level + 1]! = codeSentinel) (hpass : isautom ctx (firstScatter n (otherLeafSt ctx level numcells st).firstlab (otherLeafSt ctx level numcells st).lab) = true) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : NodeOutcome G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best best trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ ∃ (target : Nat), (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst = Int.ofNat target ∧ target < level ∧ (target = (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd.gcaFirst ∨ target = (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd.gcaCanon) ∧ ∃ (payload : Unwind ctx tcLevel target (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd best), Unwind.Located trail payload

A discrete code-one branch closes the complete node outcome. Its guide supplies the located unwind receipt, while firstEvent supplies the result-state invariants.

theorem Hex.GraphIso.Nauty.NodeInv.tiedLeaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (hcheap : st.noncheaplevel ≤ level) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hef : ¬((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hcc : (otherLeafSt ctx level numcells st).compCanon = 0) (hge : ¬level < (otherLeafSt ctx level numcells st).canonlevel) (htie : (testcanlab ctx (updatecan ctx (otherLeafSt ctx level numcells st).canong (otherLeafSt ctx level numcells st).canonlab (otherLeafSt ctx level numcells st).samerows) (otherLeafSt ctx level numcells st).lab).fst = 0) (hcoset : (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.cosetindex < n) (horbit : OrbSound (OrbConn (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.genTrace.toList n) (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.orbits n) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : NodeOutcome G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best best trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ ∃ (target : Nat), (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst = Int.ofNat target ∧ target < level ∧ (target = (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd.gcaFirst ∨ target = (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd.gcaCanon) ∧ ∃ (payload : Unwind ctx tcLevel target (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd best), Unwind.Located trail payload

A discrete code-two row tie closes the complete node outcome for both the canonical-guide and first-ancestor orbit return arms.

theorem Hex.GraphIso.Nauty.NodeInv.plainLeaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (hcheap : st.noncheaplevel ≤ level) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) (hef : ¬((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hgen : (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.genTrace = (otherLeafSt ctx level numcells st).genTrace) (hearly : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : ∃ (outBest : Option (Key n)), NodeOutcome G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ outBest = some (incMax best (nodeKey ctx tcLevel (specFuel + 1) level codes st numcells))

An early non-generator leaf absorbs its singleton subtree and returns the explicit local-prune outcome.

theorem Hex.GraphIso.Nauty.NodeInv.plainLeafDone {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (hcheap : st.noncheaplevel ≤ level) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) (hef : ¬((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hgen : (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.genTrace = (otherLeafSt ctx level numcells st).genTrace) (hdone : ¬(processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : ∃ (outBest : Option (Key n)), NodeOutcome G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ outBest = some (incMax best (nodeKey ctx tcLevel (specFuel + 1) level codes st numcells))

A non-generator leaf that does not unwind completes after the empty child sweep and returns the exact singleton-subtree maximum.

theorem Hex.GraphIso.Nauty.LoopInv.firstDone {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 index : Nat} {tcell : VSet n} {stem codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hnext : tcell.nextElem cursor = none) (hnp : st.compCanon ≤ 0) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hlive : Live ctx level st trail) : LoopOutcome G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell index st).snd.snd best best trail trail (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell index st).fst

An empty positive-fuel first-path sweep closes the coupled loop outcome. The comparison sign is explicit: a freshly prepared node may enter its first child with sign one, whereas every state that reaches the end of a real sweep has already absorbed a child and restored a nonpositive sign.

theorem Hex.GraphIso.Nauty.LoopInv.otherDone {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 : Nat} {tcell : VSet n} {stem codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hnext : tcell.nextElem cursor = none) (hnp : st.compCanon ≤ 0) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hlive : Live ctx level st trail) : LoopOutcome G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell st).snd best best trail trail (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell st).fst

An empty positive-fuel off-path sweep closes the coupled loop outcome with the same frozen-frame coverage and result event.