theorem Hex.GraphIso.Nauty.SearchOut.ofCoset {n k : Nat} {G : Colored n k} {B lev coset : Nat} {st out : SearchSt n} (h : SearchOut G B lev { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := coset, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace } out) : SearchOut G B lev st out

The coset cursor plays no role in the reach relation.

theorem Hex.GraphIso.Nauty.EventOut.checkGen {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {stem fs : List Nat} {out : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {r : Int} (h : EventOut G ctx tcLevel stem fs out best trail r) (γ : Array Nat) : γ ∈ out.genTrace.toList → checkAutom ctx.g γ = true

Every generator recorded by an event is a checked automorphism.

theorem Hex.GraphIso.Nauty.CanonTrail.ofPerm {n : Nat} {ctx : Ctx n} {level : Nat} {st out : SearchSt n} {trail : FrameTrail} (htrail : TrailOk ctx level st trail) (hlab : st.lab.size = n) (hptn : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hperm : cellsPerm st.ptn level st.lab out.canonlab) (hcsz : out.canonlab.size = n) : CanonTrail ctx level out trail

A canonical reference that is a cell permutation of the current labelling at the current level reaches every active ancestor frame and picks the same child there.

structure Hex.GraphIso.Nauty.FirstSweepHyp {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 tv1 : Nat) (base st : SearchSt n) (best : Option (Key n)) (trail : FrameTrail) : Prop

What the first-path sweep knows at every cursor position after its guiding child: the loop invariant, the live package with frame stabilization, path facts, both reference histories below the loop, the first-path controls, orbit and coset facts, first-leaf domination, 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 : FirstLive ctx level st trail rsLab rsPtn
• path : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st
• after : ∃ (v : Nat), cursor = some v ∧ tv1 ≤ v
• cursorLt (v : Nat) : cursor = some v → v < n
• sign : st.compCanon ≤ 0
• guide : st.gcaFirst = level
• firstTrail : FirstTrail ctx level st trail
• canonTrail : CanonTrail ctx level st trail
• 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
• keep : st.noncheaplevel < level → st.noncheaplevel = e

structure Hex.GraphIso.Nauty.FirstSweepKeep {n : Nat} (ctx : Ctx n) (level e : Nat) (fs : List Nat) (st out : SearchSt n) (outBest : Option (Key n)) : Prop

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

• dom (b : Key n) : outBest = some b → keyLe (pathLeafKey ctx fs out.firstlab) b
• firstlab : out.firstlab = st.firstlab
• orbits : OrbSound (OrbConn out.genTrace.toList n) out.orbits n
• coset : out.cosetindex < n
• boundary : out.noncheaplevel < level → out.noncheaplevel = e

theorem Hex.GraphIso.Nauty.LoopInv.childDescWeak {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {tv currentOffset : 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 : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hdesc : CheapDesc ctx level st.noncheaplevel (frame rsLab rsPtn numcells)) (hbnd : st.noncheaplevel ≤ level + 1) (hpark : cheapautom rsPtn level n = false → st.noncheaplevel ≠ level) (hcurrent : currentOffset < len) (hat : st.lab[tc + currentOffset]! = tv) : CheapDesc ctx (level + 1) st.noncheaplevel (refine ctx (level + 1) (breakout n st.lab st.ptn (level + 1) tc tv).fst (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd (numcells + 1))

The small-cell descent invariant of a child, when the loop boundary is merely known to avoid the loop level.

theorem Hex.GraphIso.Nauty.LoopInv.subtreeAtWeak {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hdesc : CheapDesc ctx level st.noncheaplevel (frame rsLab rsPtn numcells)) (hpark : cheapautom rsPtn level n = false → st.noncheaplevel ≠ level) (hle : st.noncheaplevel ≤ level) : SubtreeOk ctx level { lab := rsLab, ptn := rsPtn, active := base.active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }

The small-cell subtree fact at the frozen frame, when the boundary is merely known to avoid the loop level.

theorem Hex.GraphIso.Nauty.FirstSweepHyp.cheapOk {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {e tv1 : 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 : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 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.

theorem Hex.GraphIso.Nauty.FirstSweepHyp.filter {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell tcell' : VSet n} {e tv1 : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best trail) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell' cursor base st best trail) : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell' cursor e tv1 base st best trail

Filtering the live set leaves every other hypothesis unchanged.

theorem Hex.GraphIso.Nauty.SearchOut.inputEq {n k : Nat} {G : Colored n k} {B lev : Nat} {st st' out : SearchSt n} (h : SearchOut G B lev st out) (hlab : st'.lab = st.lab) (hptn : st'.ptn = st.ptn) (hfirst : st'.firstlab = st.firstlab) (hcanon : st'.canonlab = st.canonlab) : SearchOut G B lev st' out

The reach relation depends on its input state only through the labelling and partition.

theorem Hex.GraphIso.Nauty.LoopInv.childCanonPerm {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {tv currentOffset : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {canonlab : Array Nat} (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hcurrent : currentOffset < len) (hat : st.lab[tc + currentOffset]! = tv) (hcsz : canonlab.size = n) (hnew : cellsPerm (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst (level + 1) (breakout n st.lab st.ptn (level + 1) tc tv).fst canonlab) : cellsPerm st.ptn level st.lab canonlab

A new canonical reference installed below a child is a cell permutation of the loop labelling at the loop level.

theorem Hex.GraphIso.Nauty.FirstSweepHyp.next {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv offset currentOffset e tv1 : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st out : SearchSt n} {best childBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} (hg : ctx.g = rowsOf G) (hinf : inf = n + 2) (hh : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best trail) (hcodesLen : codes.length = level) (hfuel : runFuel ≠ 0) (hnext : tcell.nextElem cursor = some tv) (hoffset : offset < len) (hcurrent : currentOffset < len) (hatFrozen : rsLab[tc + offset]! = tv) (hat : st.lab[tc + currentOffset]! = tv) (hchild : OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 } out (numcells + 1) best childBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (hkeep : OtherKeep ctx (level + 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 } out) (hstay : ¬r < Int.ofNat level) (hout : SearchOut G level (level + 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 } out) (clear : Bool) (hshort : (clearShortIf clear { 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 }).needshortprune = false) : ∃ (bs' : List Nat), FirstSweepHyp G ctx tcLevel specFuel level codes bs' fs numcells rsLab rsPtn tc len tcell (some tv) e tv1 base (recover n inf level (clearShortIf clear { 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 })) childBest eventTrail

An off-path child that stays at the loop level rebuilds every sweep hypothesis for the recursive tail on the recovered state.

theorem Hex.GraphIso.Nauty.clearShortIf_lab {n : Nat} (clear : Bool) (st : SearchSt n) : (clearShortIf clear st).lab = st.lab

Clearing the request keeps the labelling and partition.

theorem Hex.GraphIso.Nauty.clearShortIf_ptn {n : Nat} (clear : Bool) (st : SearchSt n) : (clearShortIf clear st).ptn = st.ptn

theorem Hex.GraphIso.Nauty.shortPairAtReceiver {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {offset : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st out : SearchSt n} {best outBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} {fix mcr : VSet n} (hpathCodes : level = codes.length) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st) (hrBelow : r < Int.ofNat (level + 1)) (hevent : EventOut G ctx tcLevel codes fs out outBest eventTrail r) (hpreserved : TrailExt (level + 1) (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail) (hsource : ShortSource G ctx out eventTrail r) (hstay : ¬r < Int.ofNat level) (hback : out.autos.back? = some (fix, mcr)) : PairOk ctx.g rsPtn rsLab level fix mcr

The receiving-loop validity of a child's live short-prune pair, from the child's return bound alone.

theorem Hex.GraphIso.Nauty.clearShortIf_self {n : Nat} (st : SearchSt n) : (clearShortIf st.needshortprune st).needshortprune = false

Clearing the request exactly when it is raised leaves none.

theorem Hex.GraphIso.Nauty.FirstSweepHyp.childTrails {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells tc len tv offset currentOffset e tv1 : Nat} {tcell : VSet n} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {base st out : SearchSt n} {best childBest : Option (Key n)} {trail eventTrail : FrameTrail} {r : Int} (hh : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best trail) (hcurrent : currentOffset < len) (hat : st.lab[tc + currentOffset]! = tv) (hchild : OtherRun G ctx tcLevel specFuel runFuel (level + 1) codes fs { 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 } out (numcells + 1) best childBest (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail r) (hfirstlab : out.firstlab = st.firstlab) : FirstTrail ctx level { 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 } eventTrail ∧ CanonTrail ctx level { 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 } eventTrail

Both reference histories below the loop after an off-path child, whatever its return.