def Hex.GraphIso.Nauty.CheapDesc {n : Nat} (ctx : Ctx n) (level boundary : Nat) (st : RefineSt n) : Prop

Below a saved cheap-cell boundary, the current refined node remains in the small-cell subtree generated at that boundary. At the boundary itself the implication is dormant until the executable guard either validates the shape or parks the boundary at the child.

Equations

• Hex.GraphIso.Nauty.CheapDesc ctx level boundary st = (boundary < level → Hex.GraphIso.Nauty.SubtreeOk ctx level st)

theorem Hex.GraphIso.Nauty.CheapDesc.same {n : Nat} (ctx : Ctx n) (level : Nat) (st : RefineSt n) : CheapDesc ctx level level st

A boundary created at the current node imposes no condition on its strict descendants yet.

theorem Hex.GraphIso.Nauty.CheapDesc.atLevel {n : Nat} {ctx : Ctx n} {level boundary : Nat} {st : RefineSt n} (h : CheapDesc ctx level boundary st) (hit : IterOk ctx level st) (heq : Equitable ctx level st.lab st.ptn) (hcount : bcount st.ptn level n = st.numcells) (hle : boundary ≤ level) (hguard : boundary = level → cheapautom st.ptn level n = true) : SubtreeOk ctx level st

At an entered sibling sweep, a saved boundary at or above the current node supplies the small-cell subtree fact. A strictly shallower boundary uses the inherited descent invariant. Equality is exactly the case in which the current cheap-cell guard must have succeeded.

theorem Hex.GraphIso.Nauty.CheapDesc.child {n : Nat} {ctx : Ctx n} {level boundary tc len o : Nat} {st : RefineSt n} (h : CheapDesc ctx level boundary st) (hit : IterOk ctx level st) (heq : Equitable ctx level st.lab st.ptn) (hcount : bcount st.ptn level n = st.numcells) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hlvl : level < n) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) : have boundary' := if boundary ≥ level ∧ ¬cheapautom st.ptn level n = true then level + 1 else boundary; CheapDesc ctx (level + 1) boundary' (childSt ctx level st tc st.lab[tc + o]!)

The executable cheap-cell boundary update carries the small-cell subtree invariant into every individualized child.

theorem Hex.GraphIso.Nauty.FrozenOut.shrink {n : Nat} {ctx : Ctx n} {stem ancestor : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (h : FrozenOut ctx stem out best r) (hprefix : List.take ancestor.length stem = ancestor) : FrozenOut ctx ancestor out best r

Expose a shorter ancestor prefix while retaining the same frozen comparison. This is the transport used as an early return crosses nested node and loop frames.

theorem Hex.GraphIso.Nauty.FrozenOut.setFixed {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (h : FrozenOut ctx stem out best r) (fixedpts : VSet n) : FrozenOut ctx stem { 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 } best r

Fixed-point cleanup changes none of a frozen comparison's fields.

theorem Hex.GraphIso.Nauty.FrozenOut.setFirst {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (h : FrozenOut ctx stem out best r) (gcaFirst stabvertex : Nat) : FrozenOut ctx stem { 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 := gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := 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 } best r

Resetting first-path return controls changes none of a frozen comparison's fields.

theorem Hex.GraphIso.Nauty.RunPrep.frozen {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel current numcells : Nat} {stem codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunPrep G ctx tcLevel current codes bs fs numcells st best trail) (hpath : current = codes.length) (hstem : List.take stem.length codes = stem) (hfirst : st.eqlevFirst ≠ current) (hneg : st.compCanon < 0) (hfloor : Int.ofNat st.eqlevCanon.toNat ≤ pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon) : FrozenOut ctx stem (processnode ctx current numcells st).snd best (processnode ctx current numcells st).fst

A negative comparison branch whose prune tail stays below the recorded divergence produces a frozen-code witness without changing the incumbent.

theorem Hex.GraphIso.Nauty.RunPrep.pruneMode {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel current numcells : Nat} {stem codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunPrep G ctx tcLevel current codes bs fs numcells st best trail) (hpath : current = codes.length) (hstem : List.take stem.length codes = stem) (hfirst : st.eqlevFirst ≠ current) (hneg : st.compCanon < 0) : FrozenOut ctx stem (processnode ctx current numcells st).snd best (processnode ctx current numcells st).fst ∨ (processnode ctx current numcells st).fst = Int.ofNat st.noncheaplevel - 1

Every negative off-path leaf prune is either comparison-frozen or a jump to the saved cheap-cell boundary.

structure Hex.GraphIso.Nauty.FrameRel {n : Nat} (level : Nat) (st out : SearchSt n) : Prop

Two states describe the same recovered search frame at level when their partitions agree and their current labellings differ only within that partition's cells.

• ptn : out.ptn = st.ptn
• lab : cellsPerm st.ptn level st.lab out.lab

theorem Hex.GraphIso.Nauty.FrameRel.refl {n : Nat} (level : Nat) (st : SearchSt n) : FrameRel level st st

theorem Hex.GraphIso.Nauty.FrameRel.symm {n level : Nat} {st out : SearchSt n} (h : FrameRel level st out) : FrameRel level out st

theorem Hex.GraphIso.Nauty.FrameRel.trans {n level : Nat} {a b c : SearchSt n} (hab : FrameRel level a b) (hbc : FrameRel level b c) : FrameRel level a c

theorem Hex.GraphIso.Nauty.FrameRel.ofSearchOut {n k : Nat} {G : Colored n k} {level numcells : Nat} {st out : SearchSt n} (h : SearchOut G level level st out) (hst : SearchOk G level numcells st) (hout : SearchOk G level numcells out) : FrameRel level st out

A recovered SearchOut between valid endpoints is exactly a frame relation.

structure Hex.GraphIso.Nauty.GuideRel {n : Nat} (level : Nat) (st out : SearchSt n) : Prop

The guide-control facts preserved by every off-path search fragment. The second canonical alternative records a newly installed descendant of the fragment's entry frame.

• first : out.gcaFirst = st.gcaFirst
• order : out.gcaFirst ≤ out.gcaCanon
• canon : out.gcaCanon = st.gcaCanon ∧ out.canonlab = st.canonlab ∨ level ≤ out.gcaCanon ∧ cellsPerm st.ptn level st.lab out.canonlab

theorem Hex.GraphIso.Nauty.GuideRel.refl {n level : Nat} {st : SearchSt n} (horder : st.gcaFirst ≤ st.gcaCanon) : GuideRel level st st

theorem Hex.GraphIso.Nauty.GuideRel.trans {n level : Nat} {a b c : SearchSt n} (hab : GuideRel level a b) (hbc : GuideRel level b c) (hframe : FrameRel level a b) : GuideRel level a c

Guide relations compose across an equivalent recovered frame.

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

Result of one node call. done is the ordinary one-level return. frozen and cheap retain the distinct witnesses needed when the return crosses more than one loop, and unwind carries a stored generator.

• done {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {codes : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (returned : r = Int.ofNat level - 1) (exact : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level codes st numcells))) : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest trail r
• unwind {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {codes : 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) (sound : NodeSound ctx tcLevel specFuel level codes st numcells best outBest) (payload : Unwind ctx tcLevel target out outBest) (located : Unwind.Located trail payload) (control : target = out.gcaFirst ∨ target = out.gcaCanon) : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest trail r
• frozen {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {codes : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (below : r < Int.ofNat level) (exact : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level codes st numcells))) (freeze : FrozenOut ctx codes out outBest r) : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest trail r
• cheap {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {codes : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (boundary : Nat) (returned : r = Int.ofNat boundary - 1) (positive : 1 ≤ boundary) (atOrAbove : boundary ≤ level) (saved : out.noncheaplevel = boundary) (exact : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level codes st numcells))) : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest trail r
• exhausted {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {codes : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (returned : r = 0) (state : out = st) (incumbent : outBest = best) (emptyFuel : runFuel = 0) : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest trail r

inductive Hex.GraphIso.Nauty.ShortSource {n k : Nat} (G : Colored n k) (ctx : Ctx n) (out : SearchSt n) (trail : FrameTrail) (r : Int) : Prop

Provenance of the newest workspace pair while the one-shot needshortprune request is live. Explicit code-two pairs are already valid at their returned frame. Implicit cheap-cell pairs retain root validity and the deeper boundary needed to localize them when the return reaches its receiving loop.

• explicit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {out : SearchSt n} {trail : FrameTrail} {r : Int} (target : Nat) (fix mcr : VSet n) (returned : r = Int.ofNat target) (back : out.autos.back? = some (fix, mcr)) (valid : ∀ (entry : TrailEntry), trail target = some entry → PairOk ctx.g entry.frame.rsPtn entry.frame.rsLab target fix mcr) (source : ∃ (γ : Array Nat), γ ∈ out.genTrace ∧ fmperm γ n = (fix, mcr)) : ShortSource G ctx out trail r
• implicit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {out : SearchSt n} {trail : FrameTrail} {r : Int} (target : Nat) (returned : r = Int.ofNat target) (below : target < out.noncheaplevel) (back : out.autos.back? = some (fmptn out.lab out.ptn out.noncheaplevel n)) (root : PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn out.lab out.ptn out.noncheaplevel n).fst (fmptn out.lab out.ptn out.noncheaplevel n).snd) : ShortSource G ctx out trail r

theorem Hex.GraphIso.Nauty.ShortSource.setFixed {n k : Nat} {G : Colored n k} {ctx : Ctx n} {out : SearchSt n} {trail : FrameTrail} {r : Int} (h : ShortSource G ctx out trail r) (fixedpts : VSet n) : ShortSource G ctx { 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 } trail r

Fixed-point cleanup after a child return does not affect the stored pair or its source evidence.

theorem Hex.GraphIso.Nauty.ShortSource.firstFinish {n k : Nat} {G : Colored n k} {ctx : Ctx n} {out : SearchSt n} {trail : FrameTrail} {r : Int} {level size index : Nat} (h : ShortSource G ctx out trail r) : ShortSource G ctx (Nauty.firstFinish level size index out) trail r

The final first-path counter adjustment changes none of the fields used by a live short-prune source.

theorem Hex.GraphIso.Nauty.NodeExit.below {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells : Nat} {codes : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (h : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest trail r) (hlevel : 0 < level) : r < Int.ofNat level

Every result of a positive-level node lies strictly below that node's level. This is the one-step bound that lets a receiving loop identify an explicit or implicit short-prune source with its own level.

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

The final first-path counter adjustment preserves every node exit, including the payload of a located unwind.

inductive Hex.GraphIso.Nauty.LoopExit {n : Nat} (ctx : Ctx n) (tcLevel specFuel runFuel loopFuel level : Nat) (codes : 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)) (trail : FrameTrail) (r : Option Int) : Prop

Result of a sibling loop. Early comparison and cheap-cell exits carry both the exact loop maximum and the payload required to cross an older frame. Cursor-fuel exhaustion remains explicit and cannot be confused with completion.

• done {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {codes : 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)} {trail : FrameTrail} {r : Option Int} (returned : r = none) (exact : outBest = some (incMax best bound)) : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest trail r
• unwind {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {codes : 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)} {trail : FrameTrail} {r : Option Int} (target : Nat) (returned : r = some (Int.ofNat target)) (below : target < level) (sound : LoopSound ctx bound best outBest) (payload : Unwind ctx tcLevel target out outBest) (located : Unwind.Located trail payload) (control : target = out.gcaFirst ∨ target = out.gcaCanon) : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest trail r
• frozen {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {codes : 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)} {trail : FrameTrail} {r : Option Int} (value : Int) (returned : r = some value) (below : value < Int.ofNat level) (exact : outBest = some (incMax best bound)) (freeze : FrozenOut ctx codes out outBest value) : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest trail r
• cheap {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {codes : 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)} {trail : FrameTrail} {r : Option Int} (boundary : Nat) (returned : r = some (Int.ofNat boundary - 1)) (positive : 1 ≤ boundary) (below : boundary ≤ level) (saved : out.noncheaplevel = boundary) (exact : outBest = some (incMax best bound)) : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest trail r
• exhausted {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {codes : 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)} {trail : FrameTrail} {r : Option Int} (returned : r = none) (finalCursor : Option Nat) (progress : cursorRank cursor + loopFuel ≤ cursorRank finalCursor) (bounded : ∀ (v : Nat), finalCursor = some v → v < n) : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest trail r

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

Concrete node result paired with its return classification. The event and trail clauses are independent of the semantic maximum and remain reusable from the established leaf machinery.

• exit : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest receiptTrail r
• event : EventOut G ctx tcLevel codes fs out outBest eventTrail r
• preserved : TrailExt level receiptTrail eventTrail
• fixed : out.fixedpts = st.fixedpts
• short : out.needshortprune = true → ShortSource G ctx out eventTrail r

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

Off-path nodes additionally preserve the first-path control and coset cursor needed by their enclosing sibling loop.

• node : NodeRun G ctx tcLevel specFuel runFuel level codes fs st out numcells best outBest receiptTrail eventTrail r
• firstGuide : out.gcaFirst = st.gcaFirst
• order : out.gcaFirst ≤ out.gcaCanon
• canonGuide : out.gcaCanon = st.gcaCanon ∧ out.canonlab = st.canonlab ∨ level ≤ out.gcaCanon ∧ cellsPerm st.ptn level st.lab out.canonlab
• coset : out.cosetindex = st.cosetindex

structure Hex.GraphIso.Nauty.LoopRun {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 sibling-loop proof paired with its exit reason. The established proof retains coverage, event, and recovery facts. exit separately records why an unfinished suffix is nevertheless absorbed.

• proof : 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
• exit : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail r
• short : out.needshortprune = true → ∃ (value : Int), r = some value ∧ ShortSource G ctx out eventTrail value

structure Hex.GraphIso.Nauty.OtherLoopRun {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 sibling sweep additionally retains its coset cursor.

• proof : 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
• exit : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail r
• short : out.needshortprune = true → ∃ (value : Int), r = some value ∧ ShortSource G ctx out eventTrail value

structure Hex.GraphIso.Nauty.FirstLoopRun {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

The first-path sibling sweep retains both reference histories in its established proof, together with the reason for abandoning any suffix.

• proof : 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
• exit : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest receiptTrail r
• short : out.needshortprune = true → ∃ (value : Int), r = some value ∧ ShortSource G ctx out eventTrail value

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

A node run can be viewed through the local outcome interface. The conversion holds at a single node, where both early exit variants already carry exactness. It says nothing about the enclosing loop: an early exit is not coverage of the later siblings.

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

Restore the established result interface used by the invariant transport lemmas after the exit has been classified.

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

Forget the semantic receipt and expose the off-path guide relation.

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

Restore the established off-path interface for ordinary parent-level consumption and recovery.

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

Changing only the mutable live set leaves an already classified loop exit unchanged.

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

One processed cursor step increases both the loop fuel and its starting-rank budget.

theorem Hex.GraphIso.Nauty.LoopExit.prepend {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level tc len numcells : Nat} {tcell : VSet n} {codes : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {st recSt out : SearchSt n} {best mid outBest : Option (Key n)} {trail : FrameTrail} {r : Option Int} (hpre : LoopSound ctx bound best mid) (h : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound recSt out mid outBest trail r) : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest trail r

A sound processed child changes only the incoming incumbent of the classified recursive tail.

theorem Hex.GraphIso.Nauty.LoopExit.ofCheap {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level boundary tc len numcells : Nat} {tcell fixedpts : VSet n} {codes : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound childKey : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} (hboundary : 1 ≤ boundary) (hbelow : boundary ≤ level) (hsaved : out.noncheaplevel = boundary) (hbound : bound = childKey) (hexact : outBest = some (incMax best childKey)) : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st { 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 } best outBest trail (some (Int.ofNat boundary - 1))

At a small-cell node, exactness of the selected child is exactness of the whole sibling sweep, so the saved-boundary return remains a cheap exit after fixed-point cleanup.

theorem Hex.GraphIso.Nauty.LoopExit.ofFrozen {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level tail tc len numcells : Nat} {tcell fixedpts : VSet n} {codes : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {st out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {value : Int} (hfreeze : FrozenOut ctx codes out outBest value) (hlevel : level = codes.length) (hbelow : value < Int.ofNat level) (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) (hcover : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell cursor outBest) (hsound : LoopSound ctx bound best outBest) : LoopExit ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st { 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 } best outBest trail (some value)

An early frozen child absorbs both the explored prefix and every live suffix child, yielding the exact loop maximum while retaining the frozen payload for the next enclosing frame.

theorem Hex.GraphIso.Nauty.LoopExit.toNodeSome {n : Nat} {ctx : Ctx n} {tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level tc len nodeNumcells loopNumcells : Nat} {tcell : VSet n} {nodeCodes loopCodes : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {nodeSt loopSt out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {value : Int} (hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells) (hprefix : List.take nodeCodes.length loopCodes = nodeCodes) (h : LoopExit ctx tcLevel loopSpecFuel runFuel loopFuel level loopCodes rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt out best outBest trail (some value)) : NodeExit ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCodes nodeSt out nodeNumcells best outBest trail value

Convert an integer-valued loop exit to the enclosing node, shortening the frozen comparison prefix at the node boundary.

theorem Hex.GraphIso.Nauty.LoopExit.toNodeNone {n : Nat} {ctx : Ctx n} {tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level tc len nodeNumcells loopNumcells : Nat} {tcell : VSet n} {nodeCodes loopCodes : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {bound : Key n} {nodeSt loopSt out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} (hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells) (hfuel : n < cursorRank cursor + loopFuel) (h : LoopExit ctx tcLevel loopSpecFuel runFuel loopFuel level loopCodes rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt out best outBest trail none) : NodeExit ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCodes nodeSt out nodeNumcells best outBest trail (Int.ofNat level - 1)

With nonzero cursor fuel, a none loop result is genuine completion and supplies the enclosing node's ordinary one-level return.

theorem Hex.GraphIso.Nauty.RunPrep.fastSource {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) (hbound : st.noncheaplevel ≤ level) (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) (hclear : st.needshortprune = false) (hshort : (processnode ctx level numcells st).snd.needshortprune = true) : ShortSource G ctx (processnode ctx level numcells st).snd trail (processnode ctx level numcells st).fst

A fresh request from the frozen-downward processnode arm records the implicit pair admitted at the saved cheap-cell boundary.

theorem Hex.GraphIso.Nauty.NodeInv.negativeLeaf {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) (hneg : (otherLeafSt ctx level numcells st).compCanon < 0) (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)), NodeRun 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

A negative, non-generator discrete leaf produces its exit classification: ordinary comparison pruning retains its frozen prefix, and the other return is the explicit cheap-cell jump.

theorem Hex.GraphIso.Nauty.NodeInv.earlyOther {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 outBest : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (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) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) (hrun : NodeRun 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) : OtherRun 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

An early off-path leaf also preserves the guide and coset fields used when its unwind stops at the immediately enclosing sibling loop.

theorem Hex.GraphIso.Nauty.NodeInv.firstOther {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) : OtherRun 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

A code-one automorphism leaf returns the stored first-path unwind, with all off-path control fields retained for the enclosing sibling loop.

theorem Hex.GraphIso.Nauty.NodeInv.tiedOther {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) : OtherRun 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

A code-two row tie returns either its canonical guide or its first-ancestor orbit guide, retaining the chosen unwind explicitly.

theorem Hex.GraphIso.Nauty.NodeInv.negativeOther {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) (hneg : (otherLeafSt ctx level numcells st).compCanon < 0) (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)), OtherRun 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

The negative non-generator leaf, with the off-path fields needed by its parent loop retained.

theorem Hex.GraphIso.Nauty.NodeInv.doneLeaf {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)), OtherRun 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

A non-generator leaf whose return remains at the current boundary is an ordinary exact off-path node run.