def Hex.GraphIso.Nauty.clearShortIf {n : Nat} (clear : Bool) (st : SearchSt n) : SearchSt n

Consume the one-shot short-prune request when it is raised.

Equations

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

theorem Hex.GraphIso.Nauty.clearShortIf_fields {n : Nat} (clear : Bool) (st : SearchSt n) : (clearShortIf clear st).fixedpts = st.fixedpts ∧ (clearShortIf clear st).cosetindex = st.cosetindex ∧ (clearShortIf clear st).compCanon = st.compCanon ∧ (clearShortIf clear st).genTrace = st.genTrace ∧ (clearShortIf clear st).orbits = st.orbits ∧ (clearShortIf clear st).firstlab = st.firstlab ∧ (clearShortIf clear st).noncheaplevel = st.noncheaplevel ∧ (clearShortIf clear st).gcaFirst = st.gcaFirst ∧ (clearShortIf clear st).gcaCanon = st.gcaCanon ∧ (clearShortIf clear st).canonlab = st.canonlab ∧ (clearShortIf clear st).autos = st.autos

theorem Hex.GraphIso.Nauty.recover_clearShortIf (n inf level : Nat) (clear : Bool) (st : SearchSt n) : recover n inf level (clearShortIf clear st) = clearShortIf clear (recover n inf level st)

Recovering a cleared state is the cleared recovery.

theorem Hex.GraphIso.Nauty.PathOk.clearShortIf {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {st : SearchSt n} (clear : Bool) (h : PathOk ctx rootPtn rootLab level st) : PathOk ctx rootPtn rootLab level (Nauty.clearShortIf clear st)

Path facts ignore the one-shot short-prune request.

theorem Hex.GraphIso.Nauty.otherChildLoop_early {n : Nat} (ctx : Ctx n) (inf tcLevel runFuel loopFuel level numcells tc tv1 tv : Nat) (tcell : VSet n) (st : SearchSt n) (value : Int) (out : SearchSt n) (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 } = (value, out)) (hearly : value < Int.ofNat level) : otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st = (some value, { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace })

An early child return leaves the loop after cleaning the temporary fixed vertex.

theorem Hex.GraphIso.Nauty.otherChildLoop_stay {n : Nat} (ctx : Ctx n) (inf tcLevel runFuel loopFuel level numcells tc tv1 tv : Nat) (tcell : VSet n) (st : SearchSt n) (value : Int) (out : SearchSt n) (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 } = (value, out)) (hstay : ¬value < Int.ofNat level) : have cleaned := { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }; have cleared := clearShortIf cleaned.needshortprune cleaned; have tcell' := if cleaned.needshortprune = true then shortprune tcell cleared else tcell; have tcell'' := if (tv == tv1) = true then longprune tcell' cleared.fixedpts cleared.autos else tcell'; otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st = otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell''.nextElem (some tv)) tcell'' (recover n inf level cleared)

A child that stays at the loop level continues with the recursive tail on the recovered, possibly filtered, state.

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

A loop exit depends on its receipt trail only below the loop level.

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

An off-path sweep result can be rebased onto any entry trail agreeing below the loop level.

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

What an off-path sibling sweep knows at every cursor position: the established loop invariant, the live package, path facts, guide and orbit facts, and the cheap-cell boundary discipline relative to the node entry boundary e.

• inv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail
• live : OtherLive ctx level st trail
• path : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st
• cursorLt (v : Nat) : cursor = some v → v < n
• sign : st.compCanon ≤ 0 ∨ cursor = none
• start : cursor = none → tcell = windowSet n rsLab tc len
• guide : GuideRel level base st
• baseCanon : base.gcaCanon ≤ level
• orbits : OrbSound (OrbConn st.genTrace.toList n) st.orbits n
• coset : st.cosetindex < n
• firstDom (b : Key n) : best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b
• desc : CheapDesc ctx level st.noncheaplevel (LoopInv.frame rsLab rsPtn numcells)
• bnd : st.noncheaplevel ≤ level + 1
• park : cheapautom rsPtn level n = false → st.noncheaplevel = level + 1
• keep : st.noncheaplevel < level → st.noncheaplevel = e

structure Hex.GraphIso.Nauty.OtherLoopKeep {n : Nat} (ctx : Ctx n) (level e : Nat) (st out : SearchSt n) : Prop

What a finished off-path sweep preserves for its enclosing node.

• firstlab : out.firstlab = st.firstlab
• orbits : OrbSound (OrbConn out.genTrace.toList n) out.orbits n
• boundary : out.noncheaplevel < level → out.noncheaplevel = e

theorem Hex.GraphIso.Nauty.OtherLoopHyp.cheapOk {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {e : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (h : OtherLoopHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e base st best trail) : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) (level + 1) st

The cheap-cell ledger is ready for the next child.

inductive Hex.GraphIso.Nauty.OtherSweep {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat) (codes fs : List Nat) (rsLab rsPtn : Array Nat) (base : SearchSt n) : Nat → Option Nat → VSet n → SearchSt n → Option (Key n) → FrameTrail → Prop

A proof of the visits made by an off-path sweep, retaining each child's packaged return and the invariant at its receiving frame. This is proof-only: it adds no trace to the executable search state.

• done {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat} {codes fs : List Nat} {rsLab rsPtn : Array Nat} {base : SearchSt n} {loopFuel : Nat} {cursor : Option Nat} {tcell : VSet n} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {bs : List Nat} (hyp : OtherLoopHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e base st best trail) (next : tcell.nextElem cursor = none) : OtherSweep G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base (loopFuel + 1) cursor tcell st best trail
• visit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 e : Nat} {codes fs : List Nat} {rsLab rsPtn : Array Nat} {base : SearchSt n} {loopFuel : Nat} {cursor : Option Nat} {tcell : VSet n} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {bs : List Nat} {tv offset : Nat} {child out : SearchSt n} {r : Int} {childBest : Option (Key n)} {eventTrail : FrameTrail} (hyp : OtherLoopHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e base st best trail) (next : tcell.nextElem cursor = some tv) (offsetLt : offset < len) (atOffset : rsLab[tc + offset]! = tv) (childEq : child = { 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 }) (call : otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) child = (r, out)) (run : OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs child out (numcells + 1) best childBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (keep : OtherKeep ctx (level + 1) child out) (continuation : ¬r < Int.ofNat level → let cleaned := { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace }; let cleared := clearShortIf cleaned.needshortprune cleaned; let cell := if cleaned.needshortprune = true then shortprune tcell cleared else tcell; let cell' := if (tv == tv1) = true then longprune cell cleared.fixedpts cleared.autos else cell; OtherSweep G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel (some tv) cell' (recover n inf level cleared) childBest eventTrail) : OtherSweep G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base (loopFuel + 1) cursor tcell st best trail

theorem Hex.GraphIso.Nauty.otherLoopTotal {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 tail e : Nat} {stem codes fs : List Nat} {rsLab rsPtn : Array Nat} {base : SearchSt n} {bound : Key n} (hg : ctx.g = rowsOf G) (hinf : inf = n + 2) (hn0 : 0 < n) (ih : OtherTotal G ctx inf tcLevel runFuel) (hrun : n + 2 < level + 1 + runFuel) (hspec : level + 1 + specFuel = n + 1) (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells (o + 1)) (List.range tail))) (hlen : len = tail + 1) (loopFuel : Nat) (cursor : Option Nat) (tcell : VSet n) (st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) (bs : List Nat) : OtherLoopHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e base st best trail → n < cursorRank cursor + loopFuel → ∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), OtherLoopRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell st).snd best outBest trail eventTrail (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell st).fst ∧ GuideRel level base (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell st).snd ∧ OtherLoopKeep ctx level e st (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell st).snd ∧ OtherSweep G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel cursor tcell st best trail

Totality of an off-path sibling sweep at every cursor fuel exceeding the remaining cursor range, given totality of its children.

theorem Hex.GraphIso.Nauty.processnode_plain_genTrace {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hnt : ¬(st.compCanon = 0 ∧ ¬level < st.canonlevel ∧ (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0)) : (processnode ctx level numcells st).snd.genTrace = st.genTrace

A comparison leaf that is not a row tie records no generator.

theorem Hex.GraphIso.Nauty.processnode_plain_orbits {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hnt : ¬(st.compCanon = 0 ∧ ¬level < st.canonlevel ∧ (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0)) : (processnode ctx level numcells st).snd.orbits = st.orbits

A comparison leaf that is not a row tie leaves the orbits alone.

theorem Hex.GraphIso.Nauty.processnode_plain_short_ne {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hnt : ¬(st.compCanon = 0 ∧ ¬level < st.canonlevel ∧ (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0)) (hclear : st.needshortprune = false) (hshort : (processnode ctx level numcells st).snd.needshortprune = true) : level ≠ st.noncheaplevel

A fresh short-prune request at such a leaf proves that the implicit pair was admitted below the saved boundary.

theorem Hex.GraphIso.Nauty.pruneReturn_at_level {noncheaplevel allsamelevel level : Nat} (hle : noncheaplevel ≤ level) : pruneReturn noncheaplevel allsamelevel (Int.ofNat level) = Int.ofNat noncheaplevel - 1

The shared prune tail returns the level just below the saved boundary whenever the comparison depth is the current level.

theorem Hex.GraphIso.Nauty.processnode_plain_return {n nn : Nat} {ctx : Ctx n} {level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hcinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hlen : cs.length = level) (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hnn : 0 ≤ st.compCanon) (hnt : ¬(st.compCanon = 0 ∧ ¬level < st.canonlevel ∧ (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0)) (hle : st.noncheaplevel ≤ level) : (processnode ctx level numcells st).fst = Int.ofNat st.noncheaplevel - 1 ∧ (processnode ctx level numcells st).snd.autos = pruneAutos level st

A comparison leaf that is not a row tie returns just below the saved cheap-cell boundary.

theorem Hex.GraphIso.Nauty.CodeCmpInv.nonpos_of_dom {n nn : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {canoncode firstcode : Array Nat} {canonlevel : Nat} {eqlevCanon compCanon : Int} {canonlab firstlab : Array Nat} (hcinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon compCanon) (hfinv : FirstCodeInv nn cs fs firstcode cs.length) (hdom : keyLe (pathLeafKey ctx fs firstlab) (incKey ctx bs canonlab)) : compCanon ≤ 0

A first-path-agreeing leaf cannot compare above the incumbent when the first leaf is dominated by that incumbent.

theorem Hex.GraphIso.Nauty.NodeInv.cheapLeaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (hcheap : st.noncheaplevel ≤ level) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hef : ¬((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hnn : 0 ≤ (otherLeafSt ctx level numcells st).compCanon) (hnt : ¬((otherLeafSt ctx level numcells st).compCanon = 0 ∧ ¬level < (otherLeafSt ctx level numcells st).canonlevel ∧ (testcanlab ctx (updatecan ctx (otherLeafSt ctx level numcells st).canong (otherLeafSt ctx level numcells st).canonlab (otherLeafSt ctx level numcells st).samerows) (otherLeafSt ctx level numcells st).lab).fst = 0)) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : ∃ (outBest : Option (Key n)), OtherRun G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A comparison leaf that neither ties the incumbent nor sits in the frozen-downward arm installs or rejects itself and returns to the saved cheap-cell boundary.

theorem Hex.GraphIso.Nauty.OtherRun.leafKeep {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel fuel level numcells : Nat} {codes fs : 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) (hearly : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) (hsound : OrbSound (OrbConn st.genTrace.toList n) st.orbits n) (h : OtherRun G ctx tcLevel specFuel runFuel level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst) : OtherKeep ctx level st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd

An early off-path leaf keeps the first labelling, orbit soundness, and the saved cheap-cell boundary of its node.

theorem Hex.GraphIso.Nauty.NodeInv.leafOther {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (hcheap : st.noncheaplevel ≤ level) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hef : ¬((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) (hsound : OrbSound (OrbConn st.genTrace.toList n) st.orbits n) (hcoset : st.cosetindex < n) : ∃ (outBest : Option (Key n)), OtherRun G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ OtherKeep ctx level st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd

Every off-path leaf outside the first-path admission test is a packaged run that keeps its node's carried facts.

theorem Hex.GraphIso.Nauty.NodeInv.leafFirstOther {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hsent : (otherLeafSt ctx level numcells st).firstcode[level + 1]! = codeSentinel) (hpass : isautom ctx (firstScatter n (otherLeafSt ctx level numcells st).firstlab (otherLeafSt ctx level numcells st).lab) = true) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) (hsound : OrbSound (OrbConn st.genTrace.toList n) st.orbits n) (hdom : ∀ (b : Key n), best = some b → keyLe (pathLeafKey ctx fs st.firstlab) b) : OtherRun G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best best trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ OtherKeep ctx level st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd

The admitted first-path-agreeing leaf is a packaged run that keeps its node's carried facts. Domination of the first leaf rules out a comparison above the incumbent.

def Hex.GraphIso.Nauty.SearchSt.setEqlev {n : Nat} (e : Nat) (st : SearchSt n) : SearchSt n

Overwrite the first-path agreement depth.

Equations

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

theorem Hex.GraphIso.Nauty.processnode_gateFail_state {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hcanonSize : st.canonlab.size = n) (hcanonOk : LabOk st.canonlab n) (hcanonInj : LabInj st.canonlab n) (hlevel : 1 ≤ level) (heq : (st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hfail : st.firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n st.firstlab st.lab) = false) : processnode ctx level numcells st = Prod.map id (SearchSt.setEqlev st.eqlevFirst) (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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 })

Failing the admission test runs exactly the comparison arm of the twin state with agreement depth zero. Only the recorded depth differs.

theorem Hex.GraphIso.Nauty.processnode_gateFail_pair {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hcanonSize : st.canonlab.size = n) (hcanonOk : LabOk st.canonlab n) (hcanonInj : LabInj st.canonlab n) (hlevel : 1 ≤ level) (heq : (st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hfail : st.firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n st.firstlab st.lab) = false) : processnode ctx level numcells st = ((processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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, have __src := (processnode ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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 := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := st.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 })

The paired form of processnode_gateFail_state.

theorem Hex.GraphIso.Nauty.otherLeafSt_setEqlev {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) (hlevel : 2 ≤ level) : otherLeafSt ctx level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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 } = have __src := otherLeafSt ctx level numcells st; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, 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 }

Below the root, node preparation never raises a zero agreement depth, so the twin leaf state is the leaf state with its depth overwritten.

theorem Hex.GraphIso.Nauty.leafFinish_setEqlev {n : Nat} (level e : Nat) (st : SearchSt n) : leafFinish level { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := e, 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 } = have __src := leafFinish level st; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := __src.fixedpts, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := e, 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 }

Leaf cleanup commutes with overwriting the agreement depth.

theorem Hex.GraphIso.Nauty.otherNode_gateFail_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hlevel : 2 ≤ level) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hcanonSize : (otherLeafSt ctx level numcells st).canonlab.size = n) (hcanonOk : LabOk (otherLeafSt ctx level numcells st).canonlab n) (hcanonInj : LabInj (otherLeafSt ctx level numcells st).canonlab n) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hfail : (otherLeafSt ctx level numcells st).firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n (otherLeafSt ctx level numcells st).firstlab (otherLeafSt ctx level numcells st).lab) = false) : otherNode ctx inf tcLevel (fuel + 1) level numcells st = Prod.map id (SearchSt.setEqlev (otherLeafSt ctx level numcells st).eqlevFirst) (otherNode ctx inf tcLevel (fuel + 1) level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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 })

An off-path leaf that fails admission runs as its twin with the recorded agreement depth restored.

theorem Hex.GraphIso.Nauty.RunInv.setEqlevFirst {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells e : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : RunInv G ctx tcLevel level codes bs fs numcells st best trail) (he : e ≤ st.eqlevFirst) : RunInv G ctx tcLevel level codes bs fs numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := e, 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 } best trail

Lowering the first-path agreement depth preserves the stable invariant.

theorem Hex.GraphIso.Nauty.NodeInv.setEqlevFirst {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells e : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (he : e ≤ st.eqlevFirst) : NodeInv G ctx tcLevel level codes bs fs numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := e, 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 } best trail

Lowering the first-path agreement depth preserves the node invariant.

def Hex.GraphIso.Nauty.Unwind.setEqlev {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (e : Nat) : Unwind ctx tcLevel target out best → 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 := e, 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

Overwriting the agreement depth does not touch an unwind payload.

Equations

• Hex.GraphIso.Nauty.Unwind.setEqlev e (Hex.GraphIso.Nauty.Unwind.first anchor carrier atFirst) = Hex.GraphIso.Nauty.Unwind.first anchor carrier atFirst
• Hex.GraphIso.Nauty.Unwind.setEqlev e (Hex.GraphIso.Nauty.Unwind.canon anchor carrier atCanon) = Hex.GraphIso.Nauty.Unwind.canon anchor carrier atCanon
• Hex.GraphIso.Nauty.Unwind.setEqlev e (Hex.GraphIso.Nauty.Unwind.orbit payload) = Hex.GraphIso.Nauty.Unwind.orbit ⋯

theorem Hex.GraphIso.Nauty.Unwind.Located.setEqlev {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {payload : Unwind ctx tcLevel target out best} (e : Nat) (h : Located trail payload) : Located trail (Unwind.setEqlev e payload)

Location evidence survives the transport.

theorem Hex.GraphIso.Nauty.FrozenOut.setEqlev {n : Nat} {ctx : Ctx n} {stem : List Nat} {out : SearchSt n} {best : Option (Key n)} {r : Int} (h : FrozenOut ctx stem out best r) (e : Nat) : FrozenOut ctx stem { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := e, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } best r

A frozen comparison does not read the agreement depth.

theorem Hex.GraphIso.Nauty.ShortSource.setEqlev {n k : Nat} {G : Colored n k} {ctx : Ctx n} {out : SearchSt n} {trail : FrameTrail} {r : Int} (h : ShortSource G ctx out trail r) (e : Nat) : ShortSource G ctx { 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 := e, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, genTrace := out.genTrace } trail r

A short-prune source does not read the agreement depth.

theorem Hex.GraphIso.Nauty.NodeSound.setEqlev {n : Nat} {ctx : Ctx n} {tcLevel specFuel level numcells : Nat} {codes : List Nat} {st : SearchSt n} {best out : Option (Key n)} (h : NodeSound ctx tcLevel specFuel level codes { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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 best out) : NodeSound ctx tcLevel specFuel level codes st numcells best out

Semantic soundness only reads the frame of the entry state.

theorem Hex.GraphIso.Nauty.NodeExit.setEqlev {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells e : Nat} {codes : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} {r : Int} (hfuel : runFuel ≠ 0) (h : NodeExit ctx tcLevel specFuel runFuel level codes { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } out numcells best outBest trail r) : NodeExit ctx tcLevel specFuel runFuel level codes st { 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 := e, 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 } numcells best outBest trail r

The exit classification transports from the twin.

theorem Hex.GraphIso.Nauty.OtherRun.ofGateFail {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hn0 : 0 < n) (hlevel : 2 ≤ level) (hpath : level = codes.length + 1) (hcheap : st.noncheaplevel ≤ level) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hfail : (otherLeafSt ctx level numcells st).firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n (otherLeafSt ctx level numcells st).firstlab (otherLeafSt ctx level numcells st).lab) = false) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) (h : OtherRun G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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 } (otherNode ctx inf tcLevel (fuel + 1) level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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 numcells best outBest trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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) (hkeep : OtherKeep ctx level { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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 } (otherNode ctx inf tcLevel (fuel + 1) level numcells { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, 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) : OtherRun G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest trail trail (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ OtherKeep ctx level st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd

The off-path result of a leaf that fails admission follows from the result of its twin. The event package is rebuilt directly from the leaf comparison, because the twin's event only records agreement depth zero.