theorem Hex.GraphIso.Nauty.processnode_fast_genTrace {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) : (processnode ctx level numcells st).snd.genTrace = st.genTrace

The frozen-downward arm records no generator.

theorem Hex.GraphIso.Nauty.processnode_fast_orbits {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) : (processnode ctx level numcells st).snd.orbits = st.orbits

The frozen-downward arm leaves the orbit array alone.

theorem Hex.GraphIso.Nauty.processnode_fast_gcaCanon {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) : (processnode ctx level numcells st).snd.gcaCanon = st.gcaCanon

The frozen-downward arm leaves the canonical guide alone.

theorem Hex.GraphIso.Nauty.otherLeafSt_eq {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : otherLeafSt ctx level numcells st = otherNodePrep level (refine ctx level st.lab st.ptn st.active numcells).longcode { lab := (refine ctx level st.lab st.ptn st.active numcells).lab, ptn := (refine ctx level st.lab st.ptn st.active numcells).ptn, active := (refine ctx level st.lab st.ptn st.active numcells).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 := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }

The prepared state of an off-path node: refinement followed by the comparison step, before any target selection.

theorem Hex.GraphIso.Nauty.otherNode_gate_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n) (hgate : (otherLeafSt ctx level numcells st).eqlevFirst ≠ level ∧ (otherLeafSt ctx level numcells st).compCanon < 0) (hearly : (processnode ctx level (refine ctx level st.lab st.ptn st.active numcells).numcells (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) : otherNode ctx inf tcLevel (fuel + 1) level numcells st = processnode ctx level (refine ctx level st.lab st.ptn st.active numcells).numcells (otherLeafSt ctx level numcells st)

With the first-path agreement broken under a negative comparison, an internal node prunes at once and returns the leaf event's result.

theorem Hex.GraphIso.Nauty.otherNode_hintFail_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hneg : (otherLeafSt ctx level numcells st).compCanon < 0) (hmis : Int.ofNat (maketargetcell ctx (otherLeafSt ctx level numcells st).lab (otherLeafSt ctx level numcells st).ptn level tcLevel (otherLeafSt ctx level numcells st).firsttc[level]!).fst ≠ (otherLeafSt ctx level numcells st).firsttc[level]!) (hearly : (processnode ctx level (refine ctx level st.lab st.ptn st.active numcells).numcells (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, eqlevFirst := level - 1, 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 := (otherLeafSt ctx level numcells st).tctotal + (maketargetcell ctx (otherLeafSt ctx level numcells st).lab (otherLeafSt ctx level numcells st).ptn level tcLevel (otherLeafSt ctx level numcells st).firsttc[level]!).snd.snd, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace })).fst < Int.ofNat level) : otherNode ctx inf tcLevel (fuel + 1) level numcells st = processnode ctx level (refine ctx level st.lab st.ptn st.active numcells).numcells (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, eqlevFirst := level - 1, 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 := (otherLeafSt ctx level numcells st).tctotal + (maketargetcell ctx (otherLeafSt ctx level numcells st).lab (otherLeafSt ctx level numcells st).ptn level tcLevel (otherLeafSt ctx level numcells st).firsttc[level]!).snd.snd, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace })

A negative comparison whose hinted target disagrees with the first path demotes the agreement depth and prunes at once.

theorem Hex.GraphIso.Nauty.otherNode_hint_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hneg : (otherLeafSt ctx level numcells st).compCanon < 0) (hmatch : Int.ofNat (maketargetcell ctx (otherLeafSt ctx level numcells st).lab (otherLeafSt ctx level numcells st).ptn level tcLevel (otherLeafSt ctx level numcells st).firsttc[level]!).fst = (otherLeafSt ctx level numcells st).firsttc[level]!) (hshort : (processnode ctx level (refine ctx level st.lab st.ptn st.active numcells).numcells (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, 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 := (otherLeafSt ctx level numcells st).tctotal + (maketargetcell ctx (otherLeafSt ctx level numcells st).lab (otherLeafSt ctx level numcells st).ptn level tcLevel (otherLeafSt ctx level numcells st).firsttc[level]!).snd.snd, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace })).snd.needshortprune = false) : have pre := otherLeafSt ctx level numcells st; have mt := maketargetcell ctx pre.lab pre.ptn level tcLevel pre.firsttc[level]!; have base := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + mt.snd.snd, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; have pr := processnode ctx level (refine ctx level st.lab st.ptn st.active numcells).numcells base; have start := if ¬cheapautom pr.snd.ptn level n = true then have __src := pr.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 := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := level + 1, 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 } else pr.snd; have L := otherChildLoop ctx inf tcLevel fuel (n + 1) level (refine ctx level st.lab st.ptn st.active numcells).numcells mt.fst ((mt.snd.fst.nextElem none).getD 0) (mt.snd.fst.nextElem none) mt.snd.fst start; otherNode ctx inf tcLevel (fuel + 1) level numcells st = if pr.fst < Int.ofNat level then pr else match L.fst with | some rtn => (rtn, L.snd) | none => (Int.ofNat level - 1, L.snd)

A negative comparison whose hinted target agrees with the first path enters its child loop over that target cell with the comparison still frozen.

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

Off-path bookkeeping never rewrites the first leaf, keeps the orbit array sound, and lowers the saved cheap-cell boundary only to a value it already had on entry.

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

theorem Hex.GraphIso.Nauty.RunPrep.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 : RunPrep G ctx tcLevel level codes bs fs numcells st best trail) (he : e ≤ st.eqlevFirst) : RunPrep 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 prepared state.

theorem Hex.GraphIso.Nauty.RunPrep.fastEvent {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {stem 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) (hpath : level = codes.length) (hstem : List.take stem.length codes = stem) (hpast : stem.length < level) (hbound : st.noncheaplevel ≤ level) (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) (hprep : RunPrep G ctx tcLevel level codes bs fs numcells st best trail) (hlive : Live ctx level st trail) : EventOut G ctx tcLevel stem fs (processnode ctx level numcells st).snd best trail (processnode ctx level numcells st).fst

The frozen-downward arm of processnode, at any cell count, yields the packaged event with the incumbent unchanged.

theorem Hex.GraphIso.Nauty.processnode_fast_below {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hg : st.eqlevFirst ≠ level ∧ st.compCanon < 0) (hbound : st.noncheaplevel ≤ level) : (processnode ctx level numcells st).fst < Int.ofNat level

The return of the frozen-downward arm lies strictly below the node whenever the saved boundary does not exceed it.

theorem Hex.GraphIso.Nauty.nodeKey_le_of_frozen {n : Nat} {ctx : Ctx n} {tcLevel specFuel level numcells tail : Nat} {codes bs : List Nat} {st : SearchSt n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon compCanon : Int} {canonlab : Array Nat} (hinv : CodeCmpInv n (codes ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) bs canoncode canonlevel eqlevCanon compCanon) (hneg : compCanon < 0) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = false) (hlen : (specMaketargetcell 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).snd.snd = tail + 1) : keyLe (nodeKey ctx tcLevel (specFuel + 1) level codes st numcells) (incKey ctx bs canonlab)

With the comparison frozen downward at the refined code, every key of the node's specification subtree is dominated by the incumbent.

theorem Hex.GraphIso.Nauty.NodeInv.fastRun {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {codes bs fs : List Nat} {st pre : 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) (hstate : otherNode ctx inf tcLevel (fuel + 1) level numcells st = processnode ctx level (refine ctx level st.lab st.ptn st.active numcells).numcells pre) (hprep : RunPrep G ctx tcLevel level (codes ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) bs fs (refine ctx level st.lab st.ptn st.active numcells).numcells pre best trail) (hlive : Live ctx level pre trail) (hgate : pre.eqlevFirst ≠ level ∧ pre.compCanon < 0) (hbound : pre.noncheaplevel ≤ level) (hclear : pre.needshortprune = false) (hfirst : pre.gcaFirst = st.gcaFirst) (hcanon : pre.gcaCanon = st.gcaCanon) (hcanonlab : pre.canonlab = st.canonlab) (hcoset : pre.cosetindex = st.cosetindex) (hfixed : pre.fixedpts = st.fixedpts) (hfirstlab : pre.firstlab = st.firstlab) (hgen : pre.genTrace = st.genTrace) (horb : pre.orbits = st.orbits) (hncl : pre.noncheaplevel = st.noncheaplevel) (hnode : NodeInv G ctx tcLevel level codes bs fs numcells st best trail) (hsound : OrbSound (OrbConn st.genTrace.toList n) st.orbits 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 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

An internal off-path node whose prepared state prunes at once through the frozen-downward arm: its exact maximum is the unchanged incumbent, and its return is either a frozen comparison or a cheap-cell jump.

theorem Hex.GraphIso.Nauty.otherLeafSt_frames {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (otherLeafSt ctx level numcells st).gcaFirst = st.gcaFirst ∧ (otherLeafSt ctx level numcells st).gcaCanon = st.gcaCanon ∧ (otherLeafSt ctx level numcells st).canonlab = st.canonlab ∧ (otherLeafSt ctx level numcells st).cosetindex = st.cosetindex ∧ (otherLeafSt ctx level numcells st).fixedpts = st.fixedpts ∧ (otherLeafSt ctx level numcells st).firstlab = st.firstlab ∧ (otherLeafSt ctx level numcells st).genTrace = st.genTrace ∧ (otherLeafSt ctx level numcells st).orbits = st.orbits ∧ (otherLeafSt ctx level numcells st).noncheaplevel = st.noncheaplevel ∧ (otherLeafSt ctx level numcells st).needshortprune = st.needshortprune

The prepared state of an off-path node keeps every field the immediate-prune packaging reads.

theorem Hex.GraphIso.Nauty.NodeInv.gateRun {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) (hgate : (otherLeafSt ctx level numcells st).eqlevFirst ≠ level ∧ (otherLeafSt ctx level numcells st).compCanon < 0) (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) : 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 broken-agreement negative branch of an internal node.

theorem Hex.GraphIso.Nauty.NodeInv.hintFailRun {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) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hneg : (otherLeafSt ctx level numcells st).compCanon < 0) (hmis : Int.ofNat (maketargetcell ctx (otherLeafSt ctx level numcells st).lab (otherLeafSt ctx level numcells st).ptn level tcLevel (otherLeafSt ctx level numcells st).firsttc[level]!).fst ≠ (otherLeafSt ctx level numcells st).firsttc[level]!) (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) : 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 mismatched-hint negative branch of an internal node.

theorem Hex.GraphIso.Nauty.nodeKey_congr {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells : Nat} {cs : List Nat} {st st' : SearchSt n} (hlab : st'.lab = st.lab) (hptn : st'.ptn = st.ptn) (hactive : st'.active = st.active) : nodeKey ctx tcLevel fuel level cs st' numcells = nodeKey ctx tcLevel fuel level cs st numcells

The node key reads only the labelling, partition, and active set.

theorem Hex.GraphIso.Nauty.LoopInv.childKeyAll {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel level numcells tc len : Nat} {tcell : VSet n} {tv offset currentOffset : Nat} {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) (hoffset : offset < len) (hfrozen : rsLab[tc + offset]! = tv) (hcurrentAt : st.lab[tc + currentOffset]! = tv) (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 { 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)

Every frozen offset carrying the selected vertex has the key of the executable child built from it.

theorem Hex.GraphIso.Nauty.nextElem_windowSet_some {n : Nat} {lab : Array Nat} {tc len : Nat} (hlen : 1 ≤ len) (hlt : lab[tc]! < n) : ∃ (v : Nat), (windowSet n lab tc len).nextElem none = some v

The start of a sweep always has a first vertex.

theorem Hex.GraphIso.Nauty.GuideRel.stateEq {n level : Nat} {base st st' : SearchSt n} (h : GuideRel level base st) (hfirst : st'.gcaFirst = st.gcaFirst) (hcanon : st'.gcaCanon = st.gcaCanon) (hcanonlab : st'.canonlab = st.canonlab) : GuideRel level base st'

The guide relation depends only on the guide controls and the two reference labellings.

theorem Hex.GraphIso.Nauty.GuideRel.ofChild {n k : Nat} {trail : FrameTrail} {G : Colored n k} {ctx : Ctx n} {tcLevel specFuel runFuel 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 out : SearchSt n} {best outBest : Option (Key n)} {receiptTrail eventTrail : FrameTrail} {r : Int} (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail) (hguide : GuideRel level base st) (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 := 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 + 1) best outBest receiptTrail eventTrail r) : GuideRel level base out

A completed or early-returning off-path child of a sweep keeps the guide relation to the sweep's frozen entry.

theorem Hex.GraphIso.Nauty.GuideRel.recover {n level inf : Nat} {base out : SearchSt n} (h : GuideRel level base out) (hbase : base.gcaCanon ≤ level) (horder : (Nauty.recover n inf level out).gcaFirst ≤ (Nauty.recover n inf level out).gcaCanon) : GuideRel level base (Nauty.recover n inf level out)

Recovery to the sweep level keeps the guide relation once the sweep entry's canonical control is at most the sweep level.

theorem Hex.GraphIso.Nauty.SubtreeOk.setActive {n : Nat} {ctx : Ctx n} {level : Nat} {r : RefineSt n} {a : VSet n} (h : SubtreeOk ctx level r) : SubtreeOk ctx level { lab := r.lab, ptn := r.ptn, active := a, numcells := r.numcells, hint := r.hint, maxpos := r.maxpos, longcode := r.longcode }

The subtree facts survive a change of the recorded active set.

def Hex.GraphIso.Nauty.LoopInv.frame {n : Nat} (rsLab rsPtn : Array Nat) (numcells : Nat) : RefineSt n

The frozen frame of a sweep, as a refinement state.

Equations

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

theorem Hex.GraphIso.Nauty.LoopInv.levelLt {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) : level < n

A sweep frame with a live target cell has an open position.

theorem Hex.GraphIso.Nauty.LoopInv.childDesc {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)) (hpark : cheapautom rsPtn level n = false → st.noncheaplevel = level + 1) (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 at the frozen frame transports to the individualized child of the current recovered state.

theorem Hex.GraphIso.Nauty.LoopInv.subtreeAt {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 + 1) (hle : st.noncheaplevel ≤ level) : SubtreeOk ctx level { lab := rsLab, ptn := rsPtn, active := base.active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }

A small-cell subtree fact at the frozen frame, in the form the sibling-sweep bound identification consumes.

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

Facts a first-path node preserves or establishes beyond its packaged run.

• 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 : st.cosetindex < n → out.cosetindex < n
• boundary : out.noncheaplevel < level → out.noncheaplevel = st.noncheaplevel
• guide : level ≤ out.gcaFirst

def Hex.GraphIso.Nauty.OtherTotal {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel runFuel : Nat) : Prop

Totality of one off-path node at a fixed executable recursion fuel. Off-path nodes are never the root, so the level is at least two.

Equations

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

def Hex.GraphIso.Nauty.FirstTotal {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel runFuel : Nat) : Prop

Totality of one node on the unique descent preceding the first leaf.

Equations

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

theorem Hex.GraphIso.Nauty.SearchOk.levelLe {n k : Nat} {G : Colored n k} {level numcells : Nat} {st : SearchSt n} (h : SearchOk G level numcells st) : level ≤ n

A well-formed search node cannot occur deeper than the graph.

theorem Hex.GraphIso.Nauty.OtherTotal.zero {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel : Nat) : OtherTotal G ctx inf tcLevel 0

The strict node-fuel invariant rules out the zero-fuel off-path branch before any operational case analysis is needed.

theorem Hex.GraphIso.Nauty.FirstTotal.zero {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel : Nat) : FirstTotal G ctx inf tcLevel 0

The same strict bound rules out zero executable fuel on the initial descent.