structure Hex.GraphIso.Nauty.GuideStore {n : Nat} (ctx : Ctx n) (tcLevel level : Nat) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) : Prop

Live first-path and canonical guides, each tied to its active ancestor frame.

• first : 0 < st.gcaFirst → st.gcaFirst < level → ∃ (g : Guide ctx tcLevel st.gcaFirst best), g.ref = st.firstlab ∧ Guide.Located trail g
• canon : 0 < st.gcaCanon → st.gcaCanon < level → ∃ (g : Guide ctx tcLevel st.gcaCanon best), g.ref = st.canonlab ∧ Guide.Located trail g

theorem Hex.GraphIso.Nauty.GuideStore.toGuides {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : GuideStore ctx tcLevel level st best trail) : Guides ctx tcLevel level st best

Forgetting frame locations recovers the guide invariant used by the leaf-event lemmas.

theorem Hex.GraphIso.Nauty.Guide.Located.mono {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {before best : Option (Key n)} {trail : FrameTrail} (g : Guide ctx tcLevel level before) (hloc : Located trail g) (hinc : IncGrows before best) : Located trail (g.mono hinc)

Growing a guide's incumbent changes neither its frame nor its location in the active trail.

theorem Hex.GraphIso.Nauty.GuideStore.grow {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st : SearchSt n} {before best : Option (Key n)} {trail : FrameTrail} (h : GuideStore ctx tcLevel level st before trail) (hinc : IncGrows before best) : GuideStore ctx tcLevel level st best trail

Both located guide ledgers survive an incumbent increase.

theorem Hex.GraphIso.Nauty.GuideStore.root {n : Nat} (g : Array (VSet n)) (lab : Array Nat) (cellEnds : List Nat) (tcLevel : Nat) (best : Option (Key n)) (trail : FrameTrail) : GuideStore { g := g } tcLevel 1 (rootSt n lab cellEnds) best trail

The root has no live guide, independently of the empty trail.

theorem Hex.GraphIso.Nauty.GuideStore.push {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : GuideStore ctx tcLevel level st best trail) (entry : TrailEntry) (hfirst : st.gcaFirst = level → 0 < st.gcaFirst → ∃ (g : Guide ctx tcLevel st.gcaFirst best), g.ref = st.firstlab ∧ Guide.Located (trail.push level entry) g) (hcanon : st.gcaCanon = level → 0 < st.gcaCanon → ∃ (g : Guide ctx tcLevel st.gcaCanon best), g.ref = st.canonlab ∧ Guide.Located (trail.push level entry) g) : GuideStore ctx tcLevel (level + 1) st best (trail.push level entry)

Descending through a newly recorded parent child preserves every older guide and installs any guide whose control points at the parent.

The two last premises state the only new requirement: a control equal to level must be backed by a guide in the newly extended trail.

theorem Hex.GraphIso.Nauty.GuideStore.stateEq {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st st' : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : GuideStore ctx tcLevel level st best trail) (hfirst : st'.gcaFirst = st.gcaFirst) (hfirstlab : st'.firstlab = st.firstlab) (hcanon : st'.gcaCanon = st.gcaCanon) (hcanonlab : st'.canonlab = st.canonlab) : GuideStore ctx tcLevel level st' best trail

Reindex a located guide invariant across state fields that do not change either guide control or reference labelling.

theorem Hex.GraphIso.Nauty.nodeKey_perm {n : Nat} {ctx : Ctx n} (tcLevel fuel level : Nat) (cs : List Nat) (st st' : SearchSt n) (numcells : Nat) (hcp : cellsPerm st.ptn level st.lab st'.lab) (hls : st'.lab.size = st.lab.size) (hsl : st.lab.size = n) (hlab : LabOk st.lab n) (hlab' : LabOk st'.lab n) (hptn : st'.ptn = st.ptn) (hactive : st'.active = st.active) (hsp : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hstarts : ∀ (v : Nat), st.active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level) (hvals : ∀ (q : Nat), st.ptn[q]! ≤ level ∨ st.ptn[q]! = n + 2) (hlf : level + fuel ≤ n + 1) : nodeKey ctx tcLevel fuel level cs st numcells = nodeKey ctx tcLevel fuel level cs st' numcells

Cell-equivalent node labellings with the same partition and active set have the same specification key.

theorem Hex.GraphIso.Nauty.ChildDone.ofKeyEq {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells o : Nat} {child : SearchSt n} {best out : Option (Key n)} (hfull : out = some (incMax best (nodeKey ctx tcLevel specFuel (level + 1) cs child (numcells + 1)))) (heq : sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o = nodeKey ctx tcLevel specFuel (level + 1) cs child (numcells + 1)) : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells out o

Exact completion of a key-equivalent executable child covers the corresponding frozen specification child.

theorem Hex.GraphIso.Nauty.SweepCover.advanceKey {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells tv : Nat} {tcell : VSet n} {cursor : Option Nat} {child : SearchSt n} {best out : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = some tv) (hfull : out = some (incMax best (nodeKey ctx tcLevel specFuel (level + 1) cs child (numcells + 1)))) (heq : ∀ (o : Nat), o < len → rsLab[tc + o]! = tv → sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o = nodeKey ctx tcLevel specFuel (level + 1) cs child (numcells + 1)) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell (some tv) out

A key-equivalent completed child advances the mutable sweep.

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

A node outcome whose generator unwind, when present, is tied to the active frame trail. The constructors match those of NodeResult. Keeping the location in the unwind constructor prevents a caller from forgetting the only evidence that lets the receiving loop consume that return.

• complete {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {r : Int} (sound : NodeSound ctx tcLevel specFuel level cs st numcells best outBest) (returned : r = Int.ofNat level - 1) (installed : out.canonlevel ≠ 0) (read : stInc ctx out = outBest) (full : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level cs st numcells))) : NodeReceipt trail ctx tcLevel specFuel runFuel level cs st out numcells best outBest r
• unwind {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {r : Int} (sound : NodeSound ctx tcLevel specFuel level cs st numcells best outBest) (target : Nat) (returned : r = Int.ofNat target) (below : target < level) (payload : Unwind ctx tcLevel target out outBest) (located : Unwind.Located trail payload) : NodeReceipt trail ctx tcLevel specFuel runFuel level cs st out numcells best outBest r
• pruned {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {r : Int} (sound : NodeSound ctx tcLevel specFuel level cs st numcells best outBest) (target : Int) (returned : r = target) (below : target < Int.ofNat level) (installed : out.canonlevel ≠ 0) (read : stInc ctx out = outBest) (full : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level cs st numcells))) : NodeReceipt trail ctx tcLevel specFuel runFuel level cs st out numcells best outBest r
• exhausted {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {r : Int} (empty : runFuel = 0) (returned : r = 0) (unchanged : out = st) (bestUnchanged : outBest = best) : NodeReceipt trail ctx tcLevel specFuel runFuel level cs st out numcells best outBest r

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

Forgetting a node receipt's frame location recovers its ordinary semantic result.

theorem Hex.GraphIso.Nauty.NodeReceipt.sound {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells : Nat} {cs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {r : Int} (h : NodeReceipt trail ctx tcLevel specFuel runFuel level cs st out numcells best outBest r) (hfuel : runFuel ≠ 0) : NodeSound ctx tcLevel specFuel level cs st numcells best outBest

A positive-fuel receipt always carries the node soundness shared by its non-exhausted outcomes.

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

A loop outcome with every transported generator unwind located in the active frame trail.

• complete {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {cs : 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)} {r : Option Int} (returned : r = none) (sound : LoopSound ctx bound best outBest) (installed : out.canonlevel ≠ 0) (read : stInc ctx out = outBest) (finalSet : VSet n) (finalCursor : Option Nat) (cover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells finalSet finalCursor outBest) (empty : ∀ (o : Nat), ¬ChildLive rsLab tc len finalSet finalCursor o) : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r
• unwind {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {cs : 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)} {r : Option Int} (sound : LoopSound ctx bound best outBest) (target : Nat) (returned : r = some (Int.ofNat target)) (below : target < level) (payload : Unwind ctx tcLevel target out outBest) (located : Unwind.Located trail payload) : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r
• pruned {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {cs : 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)} {r : Option Int} (target : Int) (returned : r = some target) (below : target < Int.ofNat level) (sound : LoopSound ctx bound best outBest) (installed : out.canonlevel ≠ 0) (read : stInc ctx out = outBest) (full : outBest = some (incMax best bound)) : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r
• exhausted {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {cs : 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)} {r : Option Int} (returned : r = none) (sound : LoopSound ctx bound best outBest) (finalSet : VSet n) (finalCursor : Option Nat) (cover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells finalSet finalCursor outBest) (progress : cursorRank cursor + loopFuel ≤ cursorRank finalCursor) (bounded : ∀ (v : Nat), finalCursor = some v → v < n) : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r

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

Forgetting a loop receipt's frame location recovers its ordinary semantic result.

theorem Hex.GraphIso.Nauty.NodeReceipt.parentReturn {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells : Nat} {cs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {r : Int} (h : NodeReceipt trail ctx tcLevel specFuel runFuel (level + 1) cs st out numcells best outBest r) (hfuel : runFuel ≠ 0) (hstay : ¬r < Int.ofNat level) : outBest = some (incMax best (nodeKey ctx tcLevel specFuel (level + 1) cs st numcells)) ∨ ∃ (payload : Unwind ctx tcLevel level out outBest), Unwind.Located trail payload

At a parent boundary, a located child receipt either supplies the exact child maximum or a located unwind addressed to that parent.

theorem Hex.GraphIso.Nauty.SweepCover.receipt {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level tc len numcells : Nat} {tcell : VSet n} {tv offset : Nat} {codes : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {before best : Option (Key n)} {child out : SearchSt n} {r : Int} {trail : FrameTrail} (h : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell cursor before) (hnext : tcell.nextElem cursor = some tv) (hchild : NodeReceipt (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) ctx tcLevel specFuel runFuel (level + 1) codes child out (numcells + 1) before best r) (hfuel : runFuel ≠ 0) (hreturn : best = some (incMax before (nodeKey ctx tcLevel specFuel (level + 1) codes child (numcells + 1))) ∨ ∃ (payload : Unwind ctx tcLevel level out best), Unwind.Located (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) payload ∧ Unwind.FrameStable rsPtn level rsLab payload) (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)) (ho : offset < len) (htv : rsLab[tc + offset]! = tv) (hcoset : out.cosetindex = tv) (hgsz : ctx.g.size = n) (hv : ∀ (γ : Array Nat), γ ∈ out.genTrace.toList → checkAutom ctx.g γ = true) (hs : rsLab.size = n) (hinj : LabInj rsLab rsLab.size) (hok : LabOk rsLab n) (hsp : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hic : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hlf : level + 1 + specFuel ≤ n + 1) : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) best

A resolved child receipt advances its parent's coverage. Exact children may use cell-permutation key equivalence. Generator children use their location in the just-pushed parent frame, and only an orbit-pointer unwind requires stabilization.

theorem Hex.GraphIso.Nauty.SweepCover.offPathUnwind {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tc len numcells : Nat} {tcell : VSet n} {tv offset : Nat} {codes : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {before best : Option (Key n)} {out : SearchSt n} {trail : FrameTrail} {payload : Unwind ctx tcLevel level out best} (h : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell cursor before) (hinc : IncGrows before best) (hnext : tcell.nextElem cursor = some tv) (hloc : Unwind.Located trail payload) (hframe : trail level = some { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) (hoffset : offset < len) (htv : rsLab[tc + offset]! = tv) (hfirst : out.gcaFirst < level) (hs : rsLab.size = n) (hinj : LabInj rsLab rsLab.size) (hrange : tc + len ≤ n) : SweepCover ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells tcell (some tv) best

A located unwind from an off-path child cannot use the orbit arm at its parent: that arm returns to gcaFirst, which is strictly below this loop. The two direct carrier arms therefore advance coverage without a cosetindex premise.

theorem Hex.GraphIso.Nauty.Unwind.Located.setFirst {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} {payload : Unwind ctx tcLevel target out best} (h : Located trail payload) (gcaFirst stabvertex : Nat) (hbound : target ≤ gcaFirst) : ∃ (payload' : Unwind ctx tcLevel target { 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), Located trail payload'

Updating the first-path return controls preserves the source location of a generator unwind.

theorem Hex.GraphIso.Nauty.Unwind.Located.setFixed {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} {payload : Unwind ctx tcLevel target out best} (h : Located trail payload) (fixedpts : VSet n) : ∃ (payload' : Unwind ctx tcLevel target { 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), Located trail payload'

Removing a loop's temporary fixed vertex preserves the source location of a generator unwind.

theorem Hex.GraphIso.Nauty.LoopReceipt.ofChildUnwind {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel childFuel childRunFuel parentFuel loopFuel level : Nat} {childCs loopCs : List Nat} {childNumcells loopNumcells : Nat} {childSt loopSt out : SearchSt n} {best outBest : Option (Key n)} {target : Nat} {fixedpts : VSet n} {rsLab rsPtn : Array Nat} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} (hsound : NodeSound ctx tcLevel childFuel (level + 1) childCs childSt childNumcells best outBest) (hkey : keyLe (nodeKey ctx tcLevel childFuel (level + 1) childCs childSt childNumcells) bound) (hbelow : target < level) (payload : Unwind ctx tcLevel target out outBest) (hloc : Unwind.Located trail payload) : LoopReceipt trail ctx tcLevel parentFuel childRunFuel loopFuel level loopCs rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt { 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 (some (Int.ofNat target))

A located child unwind strictly past its parent lifts through the parent loop's fixed-vertex cleanup.

theorem Hex.GraphIso.Nauty.NodeReceipt.ofLoopSome {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat} {nodeCs loopCs : 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} {best outBest : Option (Key n)} {r : Int} (hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCs nodeSt nodeNumcells) (h : LoopReceipt trail ctx tcLevel loopSpecFuel runFuel loopFuel level loopCs rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt out best outBest (some r)) : NodeReceipt trail ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCs nodeSt out nodeNumcells best outBest r

A located loop return carrying an integer lifts directly through its parent node.

theorem Hex.GraphIso.Nauty.NodeReceipt.ofLoopNone {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel nodeRunFuel runFuel loopFuel level tail : Nat} {nodeCs loopCs : 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} {best outBest : Option (Key n)} (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) (h : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level loopCs rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt out best outBest none) : NodeReceipt trail ctx tcLevel (specFuel + 1) nodeRunFuel level nodeCs nodeSt out nodeNumcells best outBest (Int.ofNat level - 1)

A located completed loop with enough cursor fuel lifts to node completion.

theorem Hex.GraphIso.Nauty.LoopReceipt.prefix {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {cs : 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)} {r : Option Int} (hpre : LoopSound ctx bound best mid) (h : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound recSt out mid outBest r) : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r

Prepending a sound child fragment preserves the location carried by every recursive loop outcome.

theorem Hex.GraphIso.Nauty.LoopReceipt.reindexSet {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {cs : 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)} {r : Option Int} (h : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r) : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell' cursor bound st out best outBest r

Reindex the entry set of a located loop result.

theorem Hex.GraphIso.Nauty.LoopReceipt.step {n : Nat} {trail : FrameTrail} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level tv : Nat} {cs : 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)} {r : Option Int} (ha : After cursor tv) (h : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell (some tv) bound st out best outBest r) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r

One successful cursor step preserves located recursive outcomes.

theorem Hex.GraphIso.Nauty.SearchOut.ptnEq {n k : Nat} {G : Colored n k} {level numcells : Nat} {st out : SearchSt n} (h : SearchOut G level level st out) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) : out.ptn = st.ptn

Once both ends of a loop frame are recovered at the same level, the SearchOut low-boundary contract identifies their partitions exactly. The labelling may still differ by a within-cell permutation.

theorem Hex.GraphIso.Nauty.SearchOut.breakoutPerm {n k : Nat} {G : Colored n k} {level numcells tc len o : Nat} {st out : SearchSt n} (h : SearchOut G level level st out) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) : ∃ (oCur : Nat), oCur < len ∧ out.lab[tc + oCur]! = st.lab[tc + o]! ∧ cellsPerm (st.ptn.set! tc (level + 1)) (level + 1) (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst (breakout n out.lab out.ptn (level + 1) tc st.lab[tc + o]!).fst

A recovered loop state individualizes the same vertex as its frozen entry frame, possibly at a different offset within the target cell. The two resulting child labellings remain cell-equivalent.

theorem Hex.GraphIso.Nauty.split_end {ptn : Array Nat} {level tc : Nat} (hend : ptn[ptn.size - 1]! ≤ level) (htc : tc < ptn.size) : (ptn.set! tc (level + 1))[(ptn.set! tc (level + 1)).size - 1]! ≤ level + 1

Splitting a nonempty cell start keeps the final partition position closed one level later.

theorem Hex.GraphIso.Nauty.split_starts {n : Nat} {ptn : Array Nat} {level tc len : Nat} (hcell : IsCell ptn level tc len) (hrange : tc + len ≤ n) (v : Nat) : (VSet.empty.insert tc).mem v = true → v = 0 ∨ (ptn.set! tc (level + 1))[v - 1]! ≤ level + 1

The active singleton created by individualization marks a cell start of the split partition.

theorem Hex.GraphIso.Nauty.SearchOut.breakoutKey {n k : Nat} {codes : List Nat} {G : Colored n k} {ctx : Ctx n} {level numcells tc len o specFuel tcLevel : Nat} {st out child : SearchSt n} (h : SearchOut G level level st out) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hclab : child.lab = (breakout n out.lab out.ptn (level + 1) tc st.lab[tc + o]!).fst) (hcptn : child.ptn = (breakout n out.lab out.ptn (level + 1) tc st.lab[tc + o]!).snd.fst) (hcactive : child.active = (breakout n out.lab out.ptn (level + 1) tc st.lab[tc + o]!).snd.snd) (hcanon : child.canonlab = out.canonlab) (hfuel : level + 1 + specFuel ≤ n + 1) : sweepKey ctx tcLevel specFuel level codes st.lab st.ptn tc numcells o = nodeKey ctx tcLevel specFuel (level + 1) codes child (numcells + 1)

Individualizing the same frozen vertex after a recovered within-cell permutation produces the same specification child key. This carries SearchOut.breakoutPerm to the exact key premise consumed by SweepCover.receipt.

theorem Hex.GraphIso.Nauty.Unwind.Located.firstFinish {n : Nat} {ctx : Ctx n} {tcLevel target level size index : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {payload : Unwind ctx tcLevel target st best} (h : Located trail payload) : Located trail payload.firstFinish

First-path exit bookkeeping preserves the location of a transported generator unwind.

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

Every located node receipt crosses the first-path exit-counter update.

theorem Hex.GraphIso.Nauty.firstPath_internal_receipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel fuel level numcells tail : Nat) (cs : List Nat) (st : SearchSt n) (best outBest : Option (Key n)) (trail : FrameTrail) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells ≠ n) (hchildren : nodeKey ctx tcLevel (specFuel + 1) level cs st numcells = have rs := refine ctx level st.lab st.ptn st.active numcells; have mt := maketargetcell ctx rs.lab rs.ptn level tcLevel (-1); keysMax (sweepKey ctx tcLevel specFuel level (cs ++ [rs.longcode]) rs.lab rs.ptn mt.fst rs.numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level (cs ++ [rs.longcode]) rs.lab rs.ptn mt.fst rs.numcells (o + 1)) (List.range tail))) (hlen : (maketargetcell ctx (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn level tcLevel (-1)).snd.snd = tail + 1) : have rs := refine ctx level st.lab st.ptn st.active numcells; have mt := maketargetcell ctx rs.lab rs.ptn level tcLevel (-1); have pre0 := { lab := rs.lab, ptn := rs.ptn, active := rs.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode.set! level rs.longcode, canoncode := st.canoncode, firsttc := st.firsttc.set! level (Int.ofNat mt.fst), 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 + mt.snd.snd, 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 L := firstChildLoop ctx inf tcLevel fuel (n + 1) level rs.numcells mt.fst ((mt.snd.fst.nextElem none).getD 0) (mt.snd.fst.nextElem none) mt.snd.fst 0 pre; LoopReceipt trail ctx tcLevel specFuel fuel (n + 1) level (cs ++ [rs.longcode]) rs.lab rs.ptn mt.fst mt.snd.snd rs.numcells mt.snd.fst none (nodeKey ctx tcLevel (specFuel + 1) level cs st numcells) pre L.snd.snd best outBest L.fst → NodeReceipt trail ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A located child-loop receipt supplies the complete outcome of a non-discrete first-path node.

theorem Hex.GraphIso.Nauty.otherNode_receipt {n : Nat} {ctx : Ctx n} {inf tcLevel specFuel fuel level nodeNumcells loopNumcells tail : Nat} {nodeCs loopCs : List Nat} {nodeSt loopSt : SearchSt n} {rsLab rsPtn : Array Nat} {tc len : Nat} {tcell : VSet n} {best outBest : Option (Key n)} {trail : FrameTrail} {L : Option Int × SearchSt n} (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) (hstate : otherNode ctx inf tcLevel (fuel + 1) level nodeNumcells nodeSt = match L.fst with | some r => (r, L.snd) | none => (Int.ofNat level - 1, L.snd)) (hloop : LoopReceipt trail ctx tcLevel specFuel fuel (n + 1) level loopCs rsLab rsPtn tc len loopNumcells tcell none (nodeKey ctx tcLevel (specFuel + 1) level nodeCs nodeSt nodeNumcells) loopSt L.snd best outBest L.fst) : NodeReceipt trail ctx tcLevel (specFuel + 1) (fuel + 1) level nodeCs nodeSt (otherNode ctx inf tcLevel (fuel + 1) level nodeNumcells nodeSt).snd nodeNumcells best outBest (otherNode ctx inf tcLevel (fuel + 1) level nodeNumcells nodeSt).fst

Once the imperative prefix exposes an off-path child loop, its located receipt constructs the corresponding located node receipt.

theorem Hex.GraphIso.Nauty.otherLoop_childReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best outBest : Option (Key n)) (target : Nat) (trail : FrameTrail) (hsound : NodeSound ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } (numcells + 1) best outBest) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } (numcells + 1)) bound) (hreturn : (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).fst = Int.ofNat target) (hbelow : target < level) (payload : Unwind ctx tcLevel target (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd outBest) (hloc : Unwind.Located trail payload) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best outBest (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst

An off-path child generator unwind strictly past this loop returns with its frame location intact after fixed-vertex cleanup.

theorem Hex.GraphIso.Nauty.firstLoop_zeroReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel level numcells tc tv1 : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tv? cursor : Option Nat) (tcell : VSet n) (index : Nat) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hcursor : ∀ (v : Nat), cursor = some v → v < n) : LoopReceipt trail ctx tcLevel specFuel runFuel 0 level cs 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 (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).fst

First-path loop fuel exhaustion is retained as a distinct located receipt.

theorem Hex.GraphIso.Nauty.otherLoop_zeroReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel level numcells tc tv1 : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tv? cursor : Option Nat) (tcell : VSet n) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hcursor : ∀ (v : Nat), cursor = some v → v < n) : LoopReceipt trail ctx tcLevel specFuel runFuel 0 level cs 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 (otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).fst

Off-path loop fuel exhaustion is retained as a distinct located receipt.

theorem Hex.GraphIso.Nauty.firstLoop_doneReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index : Nat) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) (hinstalled : st.canonlevel ≠ 0) (hread : stInc ctx st = best) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = none) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs 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 (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell index st).fst

An absent next child completes a positive-fuel first-path loop.

theorem Hex.GraphIso.Nauty.otherLoop_doneReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) (hinstalled : st.canonlevel ≠ 0) (hread : stInc ctx st = best) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = none) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs 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 (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell st).fst

An absent next child completes a positive-fuel off-path loop.

theorem Hex.GraphIso.Nauty.firstLoop_orbitReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index o : Nat) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) (gens : List (Array Nat)) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = some tv) (ho : o < len) (htv : rsLab[tc + o]! = tv) (hgsz : ctx.g.size = n) (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom ctx.g γ = true) (hstab : ∀ (γ : Array Nat), γ ∈ gens → CellStab rsPtn level rsLab γ) (hs : rsLab.size = n) (hinj : LabInj rsLab rsLab.size) (hok : LabOk rsLab n) (hsp : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hic : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hlf : level + 1 + specFuel ≤ n + 1) (hsound : OrbSound (OrbConn gens n) st.orbits n) (horbit : (st.orbits[tv]! == tv) = false) (hrec : ∀ (index' : Nat), SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell (some tv) best → LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell (some tv) bound st (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index' st).snd.snd best best (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index' st).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best best (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A non-root orbit pointer skips the current first-path child while retaining located outcomes from the recursive tail.

theorem Hex.GraphIso.Nauty.firstLoop_otherReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index : Nat) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best outBest : Option (Key n)) (target : Nat) (trail : FrameTrail) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hsound : NodeSound ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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) best outBest) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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)) bound) (hreturn : (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).fst = Int.ofNat target) (hbelow : target < level) (payload : Unwind ctx tcLevel target (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd outBest) (hloc : Unwind.Located trail payload) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

An off-path child of the first-path loop transports a located unwind strictly past the loop.

theorem Hex.GraphIso.Nauty.firstLoop_guideReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index : Nat) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best outBest : Option (Key n)) (target : Nat) (trail : FrameTrail) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hsound : NodeSound ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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) best outBest) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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)) bound) (hreturn : (firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).fst = Int.ofNat target) (hbelow : target < level) (payload : Unwind ctx tcLevel target (firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd outBest) (hloc : Unwind.Located trail payload) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

The guiding child transports a located unwind strictly past the loop after installing its first-path return controls.

theorem Hex.GraphIso.Nauty.otherLoop_nextReceipt {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (trail : FrameTrail) (hnext : tcell.nextElem cursor = some tv) (hsound : NodeSound ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } (numcells + 1) best mid) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } (numcells + 1)) bound) (hreturn : (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).fst = r) (hstay : ¬r < Int.ofNat level) (hshort : (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd.needshortprune = false) (hother : (tv == tv1) = false) (hrec : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell (some tv) bound (recover n inf level (have __src := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace })) (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell (recover n inf level (have __src := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace }))).snd mid outBest (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell (recover n inf level (have __src := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace }))).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best outBest (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst

After an ordinary child completes without either filter, an off-path loop continues while retaining every located recursive outcome.

theorem Hex.GraphIso.Nauty.firstLoop_otherNext {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index : Nat) (cursor : Option Nat) (bound : Key n) (st child recSt : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (trail : FrameTrail) (hnext : tcell.nextElem cursor = some tv) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } = (r, child)) (hstay : ¬r < Int.ofNat level) (hshort : child.needshortprune = false) (hrecover : recSt = recover n inf level { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex, needshortprune := child.needshortprune, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hpre : LoopSound ctx bound best mid) (hrec : ∀ (index' : Nat), LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell (some tv) bound recSt (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index' recSt).snd.snd mid outBest (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index' recSt).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

After an ordinary non-guiding child completes without requesting a short prune, the first-path loop recovers its parent frame and continues. The child call is exposed as one equation so the mutual induction need not duplicate its output expression in every premise.

theorem Hex.GraphIso.Nauty.firstLoop_guideNext {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index : Nat) (cursor : Option Nat) (bound : Key n) (st child recSt : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (trail : FrameTrail) (hnext : tcell.nextElem cursor = some tv) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hcall : firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } = (r, child)) (hstay : ¬r < Int.ofNat level) (hshort : child.needshortprune = false) (hrecover : recSt = recover n inf level { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := level, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := tv1, needshortprune := child.needshortprune, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hpre : LoopSound ctx bound best mid) (hrec : ∀ (index' : Nat), LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell (some tv) bound recSt (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index' recSt).snd.snd mid outBest (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index' recSt).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

After the guiding child completes without requesting a short prune, the first-path loop installs its return controls, recovers the parent frame, and continues with every recursive location intact.

theorem Hex.GraphIso.Nauty.otherLoop_longNext {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (filtered tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st child recSt : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (trail : FrameTrail) (hnext : tcell.nextElem cursor = some tv) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } = (r, child)) (hstay : ¬r < Int.ofNat level) (hshort : child.needshortprune = false) (hfirst : (tv == tv1) = true) (hfiltered : filtered = longprune tcell (child.fixedpts.erase tv) child.autos) (hrecover : recSt = recover n inf level { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex, needshortprune := child.needshortprune, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hpre : LoopSound ctx bound best mid) (hrec : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells filtered (some tv) bound recSt (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt).snd mid outBest (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best outBest (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst

When the guiding child of an off-path loop completes without a short prune, the long-pruned recursive sweep reindexes to the loop's original entry set while retaining located outcomes.

theorem Hex.GraphIso.Nauty.otherLoop_shortNext {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (filtered tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st child recSt : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (trail : FrameTrail) (hnext : tcell.nextElem cursor = some tv) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } = (r, child)) (hstay : ¬r < Int.ofNat level) (hshort : child.needshortprune = true) (hother : (tv == tv1) = false) (hfiltered : filtered = shortprune tcell { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hrecover : recSt = recover n inf level { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hpre : LoopSound ctx bound best mid) (hrec : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells filtered (some tv) bound recSt (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt).snd mid outBest (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best outBest (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst

A short-pruned off-path sweep whose current child is not the guiding vertex reindexes its recursive receipt to the original entry set.

theorem Hex.GraphIso.Nauty.otherLoop_bothNext {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (shortSet filtered tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st child recSt : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (trail : FrameTrail) (hnext : tcell.nextElem cursor = some tv) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } = (r, child)) (hstay : ¬r < Int.ofNat level) (hshort : child.needshortprune = true) (hfirst : (tv == tv1) = true) (hshortSet : shortSet = shortprune tcell { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hfiltered : filtered = longprune shortSet (child.fixedpts.erase tv) child.autos) (hrecover : recSt = recover n inf level { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hpre : LoopSound ctx bound best mid) (hrec : LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells filtered (some tv) bound recSt (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt).snd mid outBest (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered recSt).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best outBest (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst

When both executable filters fire, their composed target set still reindexes to the original off-path loop entry while locations are retained.

theorem Hex.GraphIso.Nauty.firstLoop_otherShort {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len index : Nat) (filtered tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st child recSt : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (trail : FrameTrail) (hnext : tcell.nextElem cursor = some tv) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hcall : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } = (r, child)) (hstay : ¬r < Int.ofNat level) (hshort : child.needshortprune = true) (hfiltered : filtered = shortprune tcell { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hrecover : recSt = recover n inf level { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := child.gcaFirst, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := child.stabvertex, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hpre : LoopSound ctx bound best mid) (hrec : ∀ (index' : Nat), LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells filtered (some tv) bound recSt (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered index' recSt).snd.snd mid outBest (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered index' recSt).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A short-pruned non-guiding first-path child reindexes the recursive sweep to the original loop entry while retaining located outcomes.

theorem Hex.GraphIso.Nauty.firstLoop_guideShort {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len index : Nat) (filtered tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st child recSt : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (trail : FrameTrail) (hnext : tcell.nextElem cursor = some tv) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hcall : firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } = (r, child)) (hstay : ¬r < Int.ofNat level) (hshort : child.needshortprune = true) (hfiltered : filtered = shortprune tcell { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := level, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := tv1, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hrecover : recSt = recover n inf level { lab := child.lab, ptn := child.ptn, active := child.active, orbits := child.orbits, fixedpts := child.fixedpts.erase tv, autos := child.autos, wsCap := child.wsCap, firstcode := child.firstcode, canoncode := child.canoncode, firsttc := child.firsttc, firstlab := child.firstlab, canonlab := child.canonlab, canong := child.canong, samerows := child.samerows, compCanon := child.compCanon, eqlevFirst := child.eqlevFirst, eqlevCanon := child.eqlevCanon, gcaFirst := level, gcaCanon := child.gcaCanon, canonlevel := child.canonlevel, noncheaplevel := child.noncheaplevel, allsamelevel := child.allsamelevel, cosetindex := child.cosetindex, stabvertex := tv1, numnodes := child.numnodes, tctotal := child.tctotal, canupdates := child.canupdates, numorbits := child.numorbits, numgenerators := child.numgenerators, numbadleaves := child.numbadleaves, maxlevel := child.maxlevel, genTrace := child.genTrace }) (hpre : LoopSound ctx bound best mid) (hrec : ∀ (index' : Nat), LoopReceipt trail ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells filtered (some tv) bound recSt (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered index' recSt).snd.snd mid outBest (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (filtered.nextElem (some tv)) filtered index' recSt).fst) : LoopReceipt trail ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A short-pruned guiding first-path child installs the guide controls before reindexing the recursive sweep to its original entry set.