theorem Hex.GraphIso.Nauty.firstTail {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) (index : Nat) : FirstSweepHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e tv1 base st best trail → n < cursorRank cursor + loopFuel → ∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), FirstSweepRun G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell index st).snd.snd best outBest trail eventTrail (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell index st).fst ∧ FirstSweepKeep ctx level e fs st (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell index st).snd.snd outBest

Totality of the first-path sweep after its guiding child, at every cursor fuel exceeding the remaining cursor range, given totality of every off-path child.

theorem Hex.GraphIso.Nauty.NodeExit.retrail {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells : Nat} {codes : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {source dest : FrameTrail} {r : Int} (htrail : ∀ (target : Nat), target < level → source target = dest target) (h : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest source r) : NodeExit ctx tcLevel specFuel runFuel level codes st out numcells best outBest dest r

A node exit depends on its receipt trail only at its unwind target.

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

What the whole first-path sweep establishes for its enclosing node, relative to the node entry boundary e.

• dom (b : Key n) : outBest = some b → keyLe (pathLeafKey ctx fs out.firstlab) b
• 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.boundEq_of_subtree {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tc len numcells tail offset : Nat} {active : VSet n} {codes : List Nat} {rsLab rsPtn : Array Nat} {bound : Key n} (hsmall : SubtreeOk ctx level { lab := rsLab, ptn := rsPtn, active := active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hcell : IsCell rsPtn level tc len) (hlen2 : 2 ≤ len) (hrange : tc + len ≤ n) (hfuel : level + 1 + specFuel ≤ n + 1) (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) (hoffset : offset < len) : bound = sweepKey ctx tcLevel specFuel level codes rsLab rsPtn tc numcells offset

The sweep bound is every child's key once the frozen frame is a verified small-cell subtree.

theorem Hex.GraphIso.Nauty.firstLoopTotal {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tail : Nat} {cs : List Nat} {st : SearchSt n} {trail : FrameTrail} {bound : Key n} (hg : ctx.g = rowsOf G) (hinf : inf = n + 2) (hn0 : 0 < n) (ih : OtherTotal G ctx inf tcLevel runFuel) (ihFirst : FirstTotal G ctx inf tcLevel runFuel) (hrun : n + 2 < level + 1 + runFuel) (hspec : level + 1 + specFuel = n + 1) (hlevel : 1 ≤ level) (hpath : level = cs.length + 1) (hlt : level < n) (hfirst : FirstInv G ctx level cs numcells st trail) (hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st) (hcheap : st.noncheaplevel ≤ level) (hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells)) (horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n) (hcell : IsCell (refine ctx level st.lab st.ptn st.active numcells).ptn level tc len) (hlen2 : 2 ≤ len) (hrange : tc + len ≤ n) (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn tc (refine ctx level st.lab st.ptn st.active numcells).numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn tc (refine ctx level st.lab st.ptn st.active numcells).numcells (o + 1)) (List.range tail))) (hlen : len = tail + 1) : have r := refine ctx level st.lab st.ptn st.active numcells; have full := cs ++ [r.longcode]; have pre0 := { lab := r.lab, ptn := r.ptn, active := r.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode.set! level r.longcode, canoncode := st.canoncode, firsttc := st.firsttc.set! level (Int.ofNat tc), firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes + 1, tctotal := st.tctotal + len, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; have pre := if pre0.noncheaplevel ≥ level ∧ ¬cheapautom pre0.ptn level n = true then { lab := pre0.lab, ptn := pre0.ptn, active := pre0.active, orbits := pre0.orbits, fixedpts := pre0.fixedpts, autos := pre0.autos, wsCap := pre0.wsCap, firstcode := pre0.firstcode, canoncode := pre0.canoncode, firsttc := pre0.firsttc, firstlab := pre0.firstlab, canonlab := pre0.canonlab, canong := pre0.canong, samerows := pre0.samerows, compCanon := pre0.compCanon, eqlevFirst := pre0.eqlevFirst, eqlevCanon := pre0.eqlevCanon, gcaFirst := pre0.gcaFirst, gcaCanon := pre0.gcaCanon, canonlevel := pre0.canonlevel, noncheaplevel := level + 1, allsamelevel := pre0.allsamelevel, cosetindex := pre0.cosetindex, stabvertex := pre0.stabvertex, needshortprune := pre0.needshortprune, numnodes := pre0.numnodes, tctotal := pre0.tctotal, canupdates := pre0.canupdates, numorbits := pre0.numorbits, numgenerators := pre0.numgenerators, numbadleaves := pre0.numbadleaves, maxlevel := pre0.maxlevel, genTrace := pre0.genTrace } else pre0; have tcell := windowSet n r.lab tc len; have tv1 := (tcell.nextElem none).getD 0; ∃ (fs : List Nat), ∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), FirstSweepRun G ctx tcLevel specFuel runFuel (n + 1) level cs full fs r.lab r.ptn tc len r.numcells tcell none bound pre (firstChildLoop ctx inf tcLevel runFuel (n + 1) level r.numcells tc tv1 (tcell.nextElem none) tcell 0 pre).snd.snd none outBest trail eventTrail (firstChildLoop ctx inf tcLevel runFuel (n + 1) level r.numcells tc tv1 (tcell.nextElem none) tcell 0 pre).fst ∧ FirstSweepOut ctx level st.noncheaplevel fs (firstChildLoop ctx inf tcLevel runFuel (n + 1) level r.numcells tc tv1 (tcell.nextElem none) tcell 0 pre).snd.snd outBest ∧ Generation.FirstHead G ctx inf tcLevel specFuel runFuel level r.numcells tc len tv1 st.noncheaplevel full r.lab r.ptn tcell pre trail ∧ ∃ (last : Option Nat), Generation.Counted (segN r.lab tc len) (fun (v : Nat) => ∃ (γ : Array Nat), checkAutom ctx.g γ = true ∧ CellStab r.ptn level r.lab γ ∧ γ[v]! = tv1) last (firstChildLoop ctx inf tcLevel runFuel (n + 1) level r.numcells tc tv1 (tcell.nextElem none) tcell 0 pre).snd.fst

Totality of the whole first-path sibling sweep of an internal node on the first descent, from the parked refined state at cursor none, given totality of the guiding child through FirstTotal and of every later sibling through OtherTotal.

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

The escape classification of a sweep result. Below-loop unwinds are direct, since the first-path controls keep every orbit pointer at or above the loop level.

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

An early integer-valued sweep becomes its enclosing first-path node.

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

A sufficiently fuelled none sweep is genuine completion and becomes the enclosing first-path node's ordinary return.

theorem Hex.GraphIso.Nauty.firstterminal_ledger {n : Nat} (level : Nat) (st : SearchSt n) : (firstterminal level st).orbits = st.orbits ∧ (firstterminal level st).cosetindex = st.cosetindex ∧ (firstterminal level st).noncheaplevel = st.noncheaplevel

Installing the first leaf leaves the orbit ledger, the coset cursor and the cheap-cell boundary alone.

theorem Hex.GraphIso.Nauty.FirstInv.leafTotal {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes : List Nat} {st : SearchSt n} {trail : FrameTrail} (hn0 : 0 < n) (hpath : level = codes.length + 1) (h : FirstInv G ctx level codes numcells st trail) (hsound : OrbSound (OrbConn st.genTrace.toList n) st.orbits n) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) : ∃ (fs : List Nat), ∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), FirstRun G ctx tcLevel (specFuel + 1) (fuel + 1) level codes fs st (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells outBest trail eventTrail (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).fst ∧ FirstKeep ctx level st (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).snd fs outBest

The discrete first-path arm is total and carries the sweep facts.

theorem Hex.GraphIso.Nauty.firstFinish_ledger {n : Nat} (level size index : Nat) (st : SearchSt n) : (firstFinish level size index st).orbits = st.orbits ∧ (firstFinish level size index st).genTrace = st.genTrace ∧ (firstFinish level size index st).cosetindex = st.cosetindex ∧ (firstFinish level size index st).noncheaplevel = st.noncheaplevel ∧ (firstFinish level size index st).gcaFirst = st.gcaFirst

The final first-path counter adjustment leaves the sweep facts alone.

theorem Hex.GraphIso.Nauty.FirstInv.internalTotal {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells : Nat} {codes : List Nat} {st : SearchSt n} {trail : FrameTrail} (hg : ctx.g = rowsOf G) (hinf : inf = n + 2) (hn0 : 0 < n) (ih : OtherTotal G ctx inf tcLevel runFuel) (ihFirst : FirstTotal G ctx inf tcLevel runFuel) (hlevel : 1 ≤ level) (hpath : level = codes.length + 1) (hspec : level + (specFuel + 1) = n + 1) (hfuel : n + 2 < level + (runFuel + 1)) (hcheap : st.noncheaplevel ≤ level) (hdesc : CheapDesc ctx level st.noncheaplevel (refine ctx level st.lab st.ptn st.active numcells)) (horb : OrbSound (OrbConn st.genTrace.toList n) st.orbits n) (hfirst : FirstInv G ctx level codes numcells st trail) (hpathOk : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells ≠ n) : ∃ (fs : List Nat), ∃ (outBest : Option (Key n)), ∃ (eventTrail : FrameTrail), FirstRun G ctx tcLevel (specFuel + 1) (runFuel + 1) level codes fs st (firstPathNode ctx inf tcLevel (runFuel + 1) level numcells st).snd numcells outBest trail eventTrail (firstPathNode ctx inf tcLevel (runFuel + 1) level numcells st).fst ∧ FirstKeep ctx level st (firstPathNode ctx inf tcLevel (runFuel + 1) level numcells st).snd fs outBest

The internal first-path arm is total once every node at the current fuel is.

theorem Hex.GraphIso.Nauty.FirstTotal.succ {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel runFuel : Nat) (ih : OtherTotal G ctx inf tcLevel runFuel) (ihFirst : FirstTotal G ctx inf tcLevel runFuel) : FirstTotal G ctx inf tcLevel (runFuel + 1)

Every first-path node at the next executable fuel is total once every node at the current fuel is.