def Hex.GraphIso.Nauty.BoundaryOk {n k : Nat} (G : Colored n k) (ctx : Ctx n) (level : Nat) (st : SearchSt n) : Prop

At a loop boundary, an implicit small-cell pair is available even when noncheaplevel is exactly the loop level. CheapOk omits this equality case at general node entries. The loop guards restore it before beginning a sibling sweep.

Equations

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

theorem Hex.GraphIso.Nauty.BoundaryOk.parked {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st : SearchSt n} : BoundaryOk G 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 := 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 }

Parking strictly past a loop makes its equality case vacuous.

theorem Hex.GraphIso.Nauty.BoundaryOk.ofCheap {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} (hg : ctx.g = rowsOf G) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hcheap : cheapautom st.ptn level n = true) : BoundaryOk G ctx level st

A successful cheap-cell test supplies the implicit pair required at the loop boundary.

theorem Hex.GraphIso.Nauty.BoundaryOk.nextCheap {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 : BoundaryOk G ctx level st) (hrun : RunInv G ctx tcLevel level codes bs fs numcells st best trail) : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) (level + 1) st

The boundary pair advances the strict CheapOk ledger through the next child level.

theorem Hex.GraphIso.Nauty.EventOut.recoverBoundary {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level inf : Nat} {fixedpts : VSet n} {stem fs : List Nat} {out : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {r : Int} (h : EventOut G ctx tcLevel stem fs out best trail r) (hstem : stem.length = level) (hlevel : 1 ≤ level) (hinf : level < inf) : BoundaryOk G ctx level (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 })

Recovering a child event to its parent supplies the equality-boundary pair needed by the next sibling, even though ordinary CheapOk makes that equality case dormant.

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

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

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

theorem Hex.GraphIso.Nauty.erase_insert_of_miss {n : Nat} {s : VSet n} {v : Nat} (h : s.mem v = false) : (s.insert v).erase v = s

Clearing a freshly inserted bit restores the original set.

theorem Hex.GraphIso.Nauty.firstPath_discrete_fixedpts {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) : (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).snd.fixedpts = st.fixedpts

The discrete first-path arm restores its entry fixed-point set.

theorem Hex.GraphIso.Nauty.otherNode_leaf_early_fixedpts {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) (hearly : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) : (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd.fixedpts = st.fixedpts

Every early off-path leaf return restores its entry fixed-point set.

theorem Hex.GraphIso.Nauty.otherNode_leaf_done_fixedpts {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) (hdone : ¬(processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) : (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd.fixedpts = st.fixedpts

Every completed off-path leaf restores its entry fixed-point set.

structure Hex.GraphIso.Nauty.NodeProof {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel specFuel runFuel level : Nat) (cs fs : List Nat) (st out : SearchSt n) (numcells : Nat) (best outBest : Option (Key n)) (receiptTrail eventTrail : FrameTrail) (r : Int) : Prop

A semantic node outcome together with restoration of its entry fixed-point set.

• outcome : NodeOutcome G ctx tcLevel specFuel runFuel level cs fs st out numcells best outBest receiptTrail eventTrail r
• fixed : out.fixedpts = st.fixedpts

structure Hex.GraphIso.Nauty.OtherProof {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel specFuel runFuel level : Nat) (cs fs : List Nat) (st out : SearchSt n) (numcells : Nat) (best outBest : Option (Key n)) (receiptTrail eventTrail : FrameTrail) (r : Int) : Prop

The stronger off-path result retains the guide facts required by an ordinary sibling loop.

• outcome : OtherOutcome G ctx tcLevel specFuel runFuel level cs fs st out numcells best outBest receiptTrail eventTrail r
• fixed : out.fixedpts = st.fixedpts
• coset : out.cosetindex = st.cosetindex

structure Hex.GraphIso.Nauty.LoopProof {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel specFuel runFuel loopFuel level : Nat) (stem codes fs : List Nat) (rsLab rsPtn : Array Nat) (tc len numcells : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st out : SearchSt n) (best outBest : Option (Key n)) (receiptTrail eventTrail : FrameTrail) (r : Option Int) : Prop

A semantic loop outcome together with restoration of the loop entry's fixed-point set.

• outcome : LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r
• fixed : out.fixedpts = st.fixedpts

structure Hex.GraphIso.Nauty.OtherLoopProof {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel specFuel runFuel loopFuel level : Nat) (stem codes fs : List Nat) (rsLab rsPtn : Array Nat) (tc len numcells : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st out : SearchSt n) (best outBest : Option (Key n)) (receiptTrail eventTrail : FrameTrail) (r : Option Int) : Prop

An off-path loop additionally preserves the first-path coset cursor. The analogous claim is false for firstChildLoop, which installs the currently selected sibling before entering an off-path subtree.

• loop : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r
• coset : out.cosetindex = st.cosetindex

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

The first leaf remembers every child selected on the unique initial descent. Unlike RefTrail.first, this history is independent of the mutable gcaFirst return control: outer first-path loops reset that control while the leaf remains a descendant of all their frozen frames.

• reach (target : Nat) (entry : TrailEntry) : target < current → trail target = some entry → cellsPerm entry.frame.rsPtn target entry.frame.rsLab st.firstlab
• picked (target : Nat) (entry : TrailEntry) : target < current → trail target = some entry → ∃ (len : Nat), IsCell entry.frame.rsPtn target entry.frame.tc len ∧ entry.offset < len ∧ st.firstlab[entry.frame.tc]! = entry.frame.rsLab[entry.frame.tc + entry.offset]!

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

Before the enclosing first-path node returns, its canonical reference also remains inside every strictly older guiding child. The current loop frame is excluded because later siblings may replace the canonical child there. FrameRefs states what holds at that changing boundary.

• reach (target : Nat) (entry : TrailEntry) : target < current → trail target = some entry → cellsPerm entry.frame.rsPtn target entry.frame.rsLab st.canonlab
• picked (target : Nat) (entry : TrailEntry) : target < current → trail target = some entry → ∃ (len : Nat), IsCell entry.frame.rsPtn target entry.frame.tc len ∧ entry.offset < len ∧ st.canonlab[entry.frame.tc]! = entry.frame.rsLab[entry.frame.tc + entry.offset]!

inductive Hex.GraphIso.Nauty.FrozenOut {n : Nat} (ctx : Ctx n) (stem : List Nat) (out : SearchSt n) (best : Option (Key n)) (r : Int) : Prop

A comparison-frozen return retains the full deep code path while exposing any ancestor prefix through stem. The floor clause says the return does not jump above the recorded downward divergence; the boundary clause retains the cheap-cell or all-same floor of the actual prune tail.

• mk {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (current : Nat) (codes bestCodes : List Nat) (codeInv : CodeCmpInv n codes bestCodes out.canoncode out.canonlevel out.eqlevCanon (-1)) (depth : current = codes.length) (stemEq : List.take stem.length codes = stem) (installed : bestCodes ≠ []) (incumbent : best = some (incKey ctx bestCodes out.canonlab)) (floor : Int.ofNat out.eqlevCanon.toNat ≤ r) (boundary : Int.ofNat out.noncheaplevel - 1 ≤ r ∨ Int.ofNat out.allsamelevel - 1 ≤ r) : FrozenOut ctx stem out best r

theorem Hex.GraphIso.Nauty.FrozenOut.keyLe {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (h : FrozenOut ctx stem out best r) {level : Nat} (hlevel : level = stem.length) (hbelow : r < Int.ofNat level) (K : Key n) : ∃ (b : Key n), best = some b ∧ Nauty.keyLe (prefixKey stem K) b

Every subtree below an exposed ancestor prefix is below the installed incumbent once that ancestor lies strictly above the frozen return.

theorem Hex.GraphIso.Nauty.FrozenOut.liveKeyLe {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (h : FrozenOut ctx stem out best r) {tcLevel specFuel level tail tc numcells : Nat} {tcell : VSet n} {rsLab rsPtn : Array Nat} {cursor : Option Nat} (hlevel : level = stem.length) (hbelow : r < Int.ofNat level) (o : Nat) : ChildLive rsLab tc (tail + 1) tcell cursor o → ∃ (b : Key n), best = some b ∧ Nauty.keyLe (sweepKey ctx tcLevel specFuel level stem rsLab rsPtn tc numcells o) b

The frozen verdict bounds every still-live child of an abandoned ancestor sweep.

theorem Hex.GraphIso.Nauty.FrozenOut.present {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (h : FrozenOut ctx stem out best r) : ∃ (b : Key n), best = some b

A frozen verdict always names the installed incumbent that caused the comparison to stop.

theorem Hex.GraphIso.Nauty.FrozenOut.read {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (h : FrozenOut ctx stem out best r) : stInc ctx out = best

The concrete state read agrees with the incumbent carried by a frozen comparison.

theorem Hex.GraphIso.Nauty.FrozenOut.exactLoop {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {outBest best : Option (Key n)} {r : Int} {tcLevel specFuel level tail tc numcells : Nat} {tcell : VSet n} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} (h : FrozenOut ctx stem out outBest r) (hlevel : level = stem.length) (hbelow : r < Int.ofNat level) (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level stem rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level stem rsLab rsPtn tc numcells (o + 1)) (List.range tail))) (hcover : SweepCover ctx tcLevel specFuel level stem rsLab rsPtn tc (tail + 1) numcells tcell cursor outBest) (hsound : LoopSound ctx bound best outBest) : outBest = some (incMax best bound)

Coverage of the explored prefix and a frozen comparison of the live suffix recover the exact maximum of an abandoned parent sweep.

inductive Hex.GraphIso.Nauty.NodeEscape {n : Nat} (ctx : Ctx n) (tcLevel specFuel level : Nat) (cs : List Nat) (st out : SearchSt n) (numcells : Nat) (best outBest : Option (Key n)) (trail : FrameTrail) (r : Int) : Prop

What a first-path node may export. A locally absorbed or pruned node exports its exact maximum, and a genuine generator unwind directly names the first or canonical reference child. The orbit-pointer arm is resolved by firstChildLoop and does not appear here.

• full {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (eq : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level cs st numcells))) : NodeEscape ctx tcLevel specFuel level cs st out numcells best outBest trail r
• first {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (target : Nat) (returned : r = Int.ofNat target) (below : target < level) (anchor : Anchor ctx tcLevel target outBest) (carrier : LabelCarrier ctx out.firstlab out.lab out.genTrace) (located : Anchor.Located trail anchor) : NodeEscape ctx tcLevel specFuel level cs st out numcells best outBest trail r
• canon {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (target : Nat) (returned : r = Int.ofNat target) (below : target < level) (anchor : Anchor ctx tcLevel target outBest) (carrier : LabelCarrier ctx out.canonlab out.lab out.genTrace) (located : Anchor.Located trail anchor) : NodeEscape ctx tcLevel specFuel level cs st out numcells best outBest trail r

inductive Hex.GraphIso.Nauty.LoopEscape {n : Nat} (ctx : Ctx n) (tcLevel level : Nat) (bound : Key n) (out : SearchSt n) (best outBest : Option (Key n)) (trail : FrameTrail) (r : Option Int) : Prop

The corresponding first-path loop exit. Fuel-exhausted intermediate tails may still return none, and sufficient outer cursor fuel rules that arm out.

• full {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {bound : Key n} {out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Option Int} (eq : outBest = some (incMax best bound)) : LoopEscape ctx tcLevel level bound out best outBest trail r
• first {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {bound : Key n} {out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Option Int} (target : Nat) (returned : r = some (Int.ofNat target)) (below : target < level) (anchor : Anchor ctx tcLevel target outBest) (carrier : LabelCarrier ctx out.firstlab out.lab out.genTrace) (located : Anchor.Located trail anchor) : LoopEscape ctx tcLevel level bound out best outBest trail r
• canon {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {bound : Key n} {out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Option Int} (target : Nat) (returned : r = some (Int.ofNat target)) (below : target < level) (anchor : Anchor ctx tcLevel target outBest) (carrier : LabelCarrier ctx out.canonlab out.lab out.genTrace) (located : Anchor.Located trail anchor) : LoopEscape ctx tcLevel level bound out best outBest trail r
• pending {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {bound : Key n} {out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Option Int} (returned : r = none) : LoopEscape ctx tcLevel level bound out best outBest trail r

theorem Hex.GraphIso.Nauty.NodeEscape.firstFinish {n : Nat} {ctx : Ctx n} {tcLevel specFuel level numcells size index : Nat} {cs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (h : NodeEscape ctx tcLevel specFuel level cs st out numcells best outBest trail r) : NodeEscape ctx tcLevel specFuel level cs st (Nauty.firstFinish level size index out) numcells best outBest trail r

First-path sweep cleanup changes no data named by an escape witness.

theorem Hex.GraphIso.Nauty.LoopEscape.retrail {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {bound : Key n} {out : SearchSt n} {best outBest : Option (Key n)} {source dest : FrameTrail} {r : Option Int} (htrail : TrailExt level dest source) (h : LoopEscape ctx tcLevel level bound out best outBest source r) : LoopEscape ctx tcLevel level bound out best outBest dest r

Rebase direct escape locations onto a trail agreeing below the loop.

theorem Hex.GraphIso.Nauty.LoopEscape.prepend {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {bound : Key n} {out : SearchSt n} {best mid outBest : Option (Key n)} {trail : FrameTrail} {r : Option Int} (hpre : LoopSound ctx bound best mid) (h : LoopEscape ctx tcLevel level bound out mid outBest trail r) : LoopEscape ctx tcLevel level bound out best outBest trail r

Prepending a sound loop fragment adjusts only the incoming incumbent.

structure Hex.GraphIso.Nauty.FirstProof {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel specFuel runFuel level : Nat) (cs fs : List Nat) (st out : SearchSt n) (numcells : Nat) (outBest : Option (Key n)) (receiptTrail eventTrail : FrameTrail) (r : Int) : Prop

A first-path node proof additionally retains the unconditional history of the first leaf through every active ancestor frame.

• node : NodeProof G ctx tcLevel specFuel runFuel level cs fs st out numcells none outBest receiptTrail eventTrail r
• escape : NodeEscape ctx tcLevel specFuel level cs st out numcells none outBest receiptTrail r
• trail : FirstTrail ctx level out eventTrail
• canonTrail : CanonTrail ctx level out eventTrail
• resumable : Int.ofNat level - 1 ≤ r → level - 1 ≤ out.gcaFirst
• order : out.gcaFirst ≤ out.gcaCanon

structure Hex.GraphIso.Nauty.FirstLoopProof {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel specFuel runFuel loopFuel level : Nat) (stem codes fs : List Nat) (rsLab rsPtn : Array Nat) (tc len numcells : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st out : SearchSt n) (best outBest : Option (Key n)) (receiptTrail eventTrail : FrameTrail) (r : Option Int) : Prop

A first-path loop keeps the current frozen frame in the first leaf's history until the loop is converted back to its parent node result.

• loop : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r
• escape : LoopEscape ctx tcLevel level bound out best outBest receiptTrail r
• trail : FirstTrail ctx (level + 1) out eventTrail
• canonTrail : CanonTrail ctx level out eventTrail
• guideLevel : level ≤ out.gcaFirst
• order : out.gcaFirst ≤ out.gcaCanon

theorem Hex.GraphIso.Nauty.FirstTrail.retrail {n : Nat} {ctx : Ctx n} {current : Nat} {st out : SearchSt n} {source dest : FrameTrail} (h : FirstTrail ctx current st source) (hfirst : out.firstlab = st.firstlab) (hext : TrailExt current source dest) : FirstTrail ctx current out dest

Reindex first-leaf history along an output trail extension and a state update that leaves the stored first leaf unchanged.

theorem Hex.GraphIso.Nauty.FirstTrail.lower {n : Nat} {ctx : Ctx n} {current : Nat} {st : SearchSt n} {trail : FrameTrail} (h : FirstTrail ctx (current + 1) st trail) : FirstTrail ctx current st trail

Forgetting the newest active frame gives the history expected by its parent node.

theorem Hex.GraphIso.Nauty.CanonTrail.retrail {n : Nat} {ctx : Ctx n} {current : Nat} {st out : SearchSt n} {source dest : FrameTrail} (h : CanonTrail ctx current st source) (hcanon : out.canonlab = st.canonlab) (hext : TrailExt current source dest) : CanonTrail ctx current out dest

theorem Hex.GraphIso.Nauty.CanonTrail.lower {n : Nat} {ctx : Ctx n} {current : Nat} {st : SearchSt n} {trail : FrameTrail} (h : CanonTrail ctx (current + 1) st trail) : CanonTrail ctx current st trail

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

First-path sweep cleanup changes only allsamelevel.

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

theorem Hex.GraphIso.Nauty.EventOut.recoverFirst {n k specFuel : Nat} {codes : List Nat} {tc frameNumcells offset : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level inf numcells : Nat} {fixedpts : VSet n} {tv1 : Nat} {stem fs : List Nat} {out : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {r : Int} {rsLab rsPtn : Array Nat} (h : EventOut G ctx tcLevel stem fs { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.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 := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, 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 } best trail r) (hreturn : r = Int.ofNat level) (hstem : stem.length = level) (hlevel : 1 ≤ level) (hinf : level < inf) (hok : SearchOk G level numcells (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 := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, 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 })) (horder : level ≤ out.gcaCanon) (hframe : trail level = some { frame := { specFuel := specFuel, codes := codes, rsLab := rsLab, rsPtn := rsPtn, tc := tc, numcells := frameNumcells }, offset := offset }) : ∃ (bs : List Nat), RunInv G ctx tcLevel level stem bs fs numcells (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 := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, 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 }) best trail ∧ FirstLive ctx level (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 := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, 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 }) trail rsLab rsPtn

Recovering a guiding-child event whose first control has been reset to the parent produces the live first-path loop package. Return stabilization at that exact control is precisely the store-wide stabilization required for the frozen parent frame.

theorem Hex.GraphIso.Nauty.LoopInv.recoverPath {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 inf : Nat} {codes bs fs : List 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) (hpath : PathOk ctx rootPtn rootLab level st) (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) (hfixed : out.fixedpts = st.fixedpts.insert st.lab[tc + currentOffset]!) (hinf : inf = n + 2) (hcurrent : currentOffset < len) : 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; PathOk ctx rootPtn rootLab level recovered ∧ recovered.fixedpts = st.fixedpts

A completed child, cleanup, and recovery restore both parent path facts. The selected vertex is fresh because it lies in a non-singleton target cell while all older fixed vertices occupy singleton cells.

theorem Hex.GraphIso.Nauty.NodeProof.firstFinish {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells size index : Nat} {cs fs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Int} (hfuel : runFuel ≠ 0) (h : NodeProof G ctx tcLevel specFuel runFuel level cs fs st out numcells best outBest receiptTrail eventTrail r) : NodeProof G ctx tcLevel specFuel runFuel level cs fs st (Nauty.firstFinish level size index out) numcells best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.PathOk.stateEq {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {st out : SearchSt n} (h : PathOk ctx rootPtn rootLab level st) (hlab : out.lab = st.lab) (hptn : out.ptn = st.ptn) (hfixed : out.fixedpts = st.fixedpts) : PathOk ctx rootPtn rootLab level out

Reindex path facts across a state update that changes none of the fields they mention.

theorem Hex.GraphIso.Nauty.PathOk.individualize {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level tc len o : Nat} {st : SearchSt n} (h : PathOk ctx rootPtn rootLab level st) (hinj : LabInj st.lab n) (hlab : LabOk st.lab n) (hsize : st.lab.size = n) (hpsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hvals : ∀ (q : Nat), st.ptn[q]! ≠ level + 1) : PathOk 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 facts from any well-formed equitable parent frame. This is the pre-incumbent analogue of PathOk.breakout, which obtains the same premises from a LoopInv.

theorem Hex.GraphIso.Nauty.FirstInv.terminalProof {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; NodeProof G ctx tcLevel (specFuel + 1) (fuel + 1) level cs full st out.snd numcells none (some (pathLeafKey ctx full rs.lab)) trail trail out.fst

A discrete first-path leaf supplies the coupled node result and restores the fixed-point frame with which the node was entered.

theorem Hex.GraphIso.Nauty.FirstInv.terminalFirstProof {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; FirstProof G ctx tcLevel (specFuel + 1) (fuel + 1) level cs full st out.snd numcells (some (pathLeafKey ctx full rs.lab)) trail trail out.fst

The first leaf also turns the accumulated active descent into an unconditional history of the selected child at every ancestor frame.

theorem Hex.GraphIso.Nauty.FirstInv.childPath {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {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) (h : FirstInv G ctx level cs numcells st trail) (hp : PathOk ctx rootPtn rootLab level st) (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 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 }; PathOk ctx rootPtn rootLab (level + 1) child

The executable first-child prefix preserves and extends the root path facts before the first incumbent exists.

theorem Hex.GraphIso.Nauty.OtherProof.otherLeafSt_coset {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (otherLeafSt ctx level numcells st).cosetindex = st.cosetindex

theorem Hex.GraphIso.Nauty.OtherProof.firstCover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tc len tv offset currentOffset : 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} (hg : ctx.g = rowsOf G) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (h : OtherProof 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 := tv, 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) (hfuel : runFuel ≠ 0) (hstay : ¬r < Int.ofNat level) (hnext : tcell.nextElem cursor = some tv) (hoffset : offset < len) (htv : rsLab[tc + offset]! = 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 := tv, 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)) : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) outBest

A completed off-path child of the first-path loop consumes its current sibling. Here cosetindex is sound: the child record installs tv, and the whole otherNode result preserves it.

theorem Hex.GraphIso.Nauty.OtherProof.ofLeafEarly {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes fs : List Nat} {st : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hearly : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) (hout : OtherOutcome G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest receiptTrail eventTrail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst) : OtherProof G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest receiptTrail eventTrail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

Package any early off-path leaf outcome with its fixed-frame equation.

theorem Hex.GraphIso.Nauty.OtherProof.ofLeafDone {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes fs : List Nat} {st : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdone : ¬(processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) (hout : OtherOutcome G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest receiptTrail eventTrail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst) : OtherProof G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest receiptTrail eventTrail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

Package any completed off-path leaf outcome with its fixed-frame equation.

theorem Hex.GraphIso.Nauty.OtherProof.node {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells : Nat} {cs fs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {r : Int} {receiptTrail eventTrail : FrameTrail} (h : OtherProof G ctx tcLevel specFuel runFuel level cs fs st out numcells best outBest receiptTrail eventTrail r) : NodeProof G ctx tcLevel specFuel runFuel level cs fs st out numcells best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.LoopProof.reindexSet {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (h : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r) : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell' cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.LoopProof.step {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level tv : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (ha : After cursor tv) (h : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv) bound st out best outBest receiptTrail eventTrail r) : LoopProof G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.LoopProof.retrail {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {source dest eventTrail : FrameTrail} {r : Option Int} (htrail : TrailExt level dest source) (h : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest source eventTrail r) : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest dest eventTrail r

theorem Hex.GraphIso.Nauty.LoopProof.prepend {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st recSt out : SearchSt n} {best mid outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (hfixed : recSt.fixedpts = st.fixedpts) (hpre : LoopSound ctx bound best mid) (h : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound recSt out mid outBest receiptTrail eventTrail r) : LoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.OtherLoopProof.reindexSet {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (h : OtherLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r) : OtherLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell' cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.OtherLoopProof.step {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level tv : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (ha : After cursor tv) (h : OtherLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv) bound st out best outBest receiptTrail eventTrail r) : OtherLoopProof G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.OtherLoopProof.retrail {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {source dest eventTrail : FrameTrail} {r : Option Int} (htrail : TrailExt level dest source) (h : OtherLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest source eventTrail r) : OtherLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest dest eventTrail r

theorem Hex.GraphIso.Nauty.OtherLoopProof.prepend {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st recSt out : SearchSt n} {best mid outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (hfixed : recSt.fixedpts = st.fixedpts) (hcoset : recSt.cosetindex = st.cosetindex) (hpre : LoopSound ctx bound best mid) (h : OtherLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound recSt out mid outBest receiptTrail eventTrail r) : OtherLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.FirstLoopProof.toNodeSome {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat} {nodeCs loopCs fs : List Nat} {rsLab rsPtn : Array Nat} {tc len nodeNumcells loopNumcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {nodeSt loopSt out : SearchSt n} {outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Int} (hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCs nodeSt nodeNumcells) (hfixed : loopSt.fixedpts = nodeSt.fixedpts) (h : FirstLoopProof G ctx tcLevel loopSpecFuel runFuel loopFuel level nodeCs loopCs fs rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt out none outBest receiptTrail eventTrail (some r)) : FirstProof G ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCs fs nodeSt out nodeNumcells outBest receiptTrail eventTrail r

An early-returning first-path loop supplies its enclosing first-path node while dropping the loop's own frozen frame from the active history.

theorem Hex.GraphIso.Nauty.FirstLoopProof.toNodeNone {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel nodeRunFuel runFuel loopFuel level tail : Nat} {nodeCs loopCs fs : List Nat} {rsLab rsPtn : Array Nat} {tc len nodeNumcells loopNumcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {nodeSt loopSt out : SearchSt n} {outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} (hbound : bound = nodeKey ctx tcLevel (specFuel + 1) level nodeCs nodeSt nodeNumcells) (hchildren : nodeKey ctx tcLevel (specFuel + 1) level nodeCs nodeSt nodeNumcells = keysMax (sweepKey ctx tcLevel specFuel level loopCs rsLab rsPtn tc loopNumcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level loopCs rsLab rsPtn tc loopNumcells (o + 1)) (List.range tail))) (hlen : len = tail + 1) (hfuel : n < cursorRank cursor + loopFuel) (hfixed : loopSt.fixedpts = nodeSt.fixedpts) (h : FirstLoopProof G ctx tcLevel specFuel runFuel loopFuel level nodeCs loopCs fs rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt out none outBest receiptTrail eventTrail none) : FirstProof G ctx tcLevel (specFuel + 1) nodeRunFuel level nodeCs fs nodeSt out nodeNumcells outBest receiptTrail eventTrail (Int.ofNat level - 1)

A fully exhausted first-path loop supplies its enclosing node once cursor fuel proves that exhaustion means complete child coverage.

theorem Hex.GraphIso.Nauty.FirstLoopProof.reindexSet {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (h : FirstLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r) : FirstLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell' cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.FirstLoopProof.step {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level tv : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (ha : After cursor tv) (h : FirstLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv) bound st out best outBest receiptTrail eventTrail r) : FirstLoopProof G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.FirstLoopProof.retrail {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {source dest eventTrail : FrameTrail} {r : Option Int} (htrail : TrailExt level dest source) (h : FirstLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest source eventTrail r) : FirstLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest dest eventTrail r

theorem Hex.GraphIso.Nauty.FirstLoopProof.prepend {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st recSt out : SearchSt n} {best mid outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Option Int} (hfixed : recSt.fixedpts = st.fixedpts) (hpre : LoopSound ctx bound best mid) (h : FirstLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound recSt out mid outBest receiptTrail eventTrail r) : FirstLoopProof G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail eventTrail r

theorem Hex.GraphIso.Nauty.FirstProof.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} {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 none trail) (h : FirstProof G ctx tcLevel specFuel runFuel (level + 1) codes fs child out (numcells + 1) 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) (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

A first-path child that stays at its parent boundary consumes the selected child. NodeEscape rules out the orbit-pointer arm here: a deeper first-path loop resolves that arm before returning.

theorem Hex.GraphIso.Nauty.FirstProof.recoverRefs {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tc len offset tv1 inf : Nat} {fixedpts : VSet n} {cs fs : List Nat} {rsLab rsPtn : Array Nat} {child out : SearchSt n} {outBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} (h : FirstProof G ctx tcLevel specFuel runFuel (level + 1) cs fs child out (numcells + 1) outBest (trail.push level { frame := sweepFrame specFuel cs rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (hdone : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells outBest offset) (hoff : offset < len) : FrameRefs ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells (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 := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, 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 first-child cleanup and recovery, both reference leaves still lie below the selected guiding child. Thus the one absorbed child backs both current-frame reference controls, whichever controls recover to the parent level.

theorem Hex.GraphIso.Nauty.FirstProof.recoverTrails {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tv1 inf : Nat} {fixedpts : VSet n} {cs fs : List Nat} {child out : SearchSt n} {outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Int} (h : FirstProof G ctx tcLevel specFuel runFuel (level + 1) cs fs child out (numcells + 1) outBest receiptTrail eventTrail r) : FirstTrail ctx (level + 1) (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 := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, 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 ∧ CanonTrail ctx level (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 := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, 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

Cleanup, first-control installation, and recovery change neither leaf reference. The first trail therefore keeps the current frozen frame, while the canonical trail can be lowered to the shallower frames of the enclosing first-path node.

theorem Hex.GraphIso.Nauty.FirstProof.setFirstEvent {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tc len offset tv1 : Nat} {cs fs : List Nat} {rsLab rsPtn : Array Nat} {child out : SearchSt n} {outBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} (hpath : cs.length = level) (hreturn : r = Int.ofNat level) (h : FirstProof G ctx tcLevel specFuel runFuel (level + 1) cs fs child out (numcells + 1) outBest (trail.push level { frame := sweepFrame specFuel cs rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (hdone : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells outBest offset) (hlevel : 1 ≤ level) (hls : rsLab.size = n) (hlab : LabOk rsLab n) (hps : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hcell : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hoff : offset < len) (hfuel : level + 1 + specFuel ≤ n + 1) : EventOut G ctx tcLevel cs fs { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.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 := level, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := tv1, 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 r

A completed guiding child installs a located first-reference guide at its parent frame. The unconditional first trail supplies both the exact selected vertex and the cell-permutation reachability that the mutable GCA control alone cannot recover.

theorem Hex.GraphIso.Nauty.FirstProof.firstFinish {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells size index : Nat} {cs fs : List Nat} {st out : SearchSt n} {outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Int} (hfuel : runFuel ≠ 0) (h : FirstProof G ctx tcLevel specFuel runFuel level cs fs st out numcells outBest receiptTrail eventTrail r) : FirstProof G ctx tcLevel specFuel runFuel level cs fs st (Nauty.firstFinish level size index out) numcells outBest receiptTrail eventTrail r

The final first-path allsamelevel adjustment preserves both the semantic result and the stored first-leaf history.

theorem Hex.GraphIso.Nauty.LoopInv.firstZero {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len : Nat} {tcell : VSet n} {tv1 index : Nat} {stem codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {tv? 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) (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) (hcursor : ∀ (v : Nat), cursor = some v → v < n) : LoopProof G ctx tcLevel specFuel runFuel 0 level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).snd.snd best best trail trail (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).fst

Exhausting first-path loop fuel retains both the semantic event and the unchanged fixed-point frame. The outer node later rules this case out from the cursor-progress bound.

theorem Hex.GraphIso.Nauty.LoopInv.otherZero {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len : Nat} {tcell : VSet n} {tv1 : Nat} {stem codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {tv? 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) (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) (hcursor : ∀ (v : Nat), cursor = some v → v < n) : LoopProof G ctx tcLevel specFuel runFuel 0 level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).snd best best trail trail (otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).fst

Exhausting off-path loop fuel retains both the semantic event and the unchanged fixed-point frame.

theorem Hex.GraphIso.Nauty.LoopInv.firstDoneProof {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) : LoopProof 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

Completing a positive-fuel first-path sweep leaves its fixed-point frame unchanged.

theorem Hex.GraphIso.Nauty.LoopInv.otherDoneProof {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) : LoopProof 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

Completing a positive-fuel off-path sweep leaves its fixed-point frame unchanged.

theorem Hex.GraphIso.Nauty.OtherLoopProof.zero {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len : Nat} {tcell : VSet n} {tv1 : Nat} {stem codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {tv? 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) (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) (hcursor : ∀ (v : Nat), cursor = some v → v < n) : OtherLoopProof G ctx tcLevel specFuel runFuel 0 level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).snd best best trail trail (otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).fst

The zero-fuel off-path loop preserves the coset cursor literally.

theorem Hex.GraphIso.Nauty.OtherLoopProof.done {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) : OtherLoopProof 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

A positive-fuel loop with no next child likewise returns its state unchanged.

theorem Hex.GraphIso.Nauty.FirstLoopProof.zero {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len : Nat} {tcell : VSet n} {tv1 index : Nat} {stem codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {tv? 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) (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) (hcursor : ∀ (v : Nat), cursor = some v → v < n) (hfirst : FirstTrail ctx (level + 1) st trail) (hcanon : CanonTrail ctx level st trail) (hguide : level ≤ st.gcaFirst) (horder : st.gcaFirst ≤ st.gcaCanon) : FirstLoopProof G ctx tcLevel specFuel runFuel 0 level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).snd.snd best best trail trail (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).fst

A zero-fuel first-path loop is a pending tail and preserves all first-descent history literally.

theorem Hex.GraphIso.Nauty.FirstLoopProof.done {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel loopFuel level numcells tc len tv1 index tail : 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) (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells (o + 1)) (List.range tail))) (hlen : len = tail + 1) (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) (hfirst : FirstTrail ctx (level + 1) st trail) (hcanon : CanonTrail ctx level st trail) (hguide : level ≤ st.gcaFirst) (horder : st.gcaFirst ≤ st.gcaCanon) : FirstLoopProof 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

A positive-fuel first-path loop with no next child has covered its fixed specification bound.