theorem
Hex.GraphIso.Nauty.LoopInv.tree
{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)
:
Generation.TreeOk ctx level (frame rsLab rsPtn numcells)
A valid sweep freezes a valid refined tree, including its depth bound.
theorem
Hex.GraphIso.Nauty.LoopInv.childPath
{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)
{boundary o current : Nat}
{targets : List Nat}
{key : Key n}
(hgsz : ctx.g.size = n)
(ho : o < len)
(hc : current < len)
(hat : st.lab[tc + current]! = rsLab[tc + o]!)
(hp :
Generation.RefPath ctx tcLevel boundary (level + 1) (childSt ctx level (frame rsLab rsPtn numcells) tc rsLab[tc + o]!)
targets key)
:
A frozen child reference follows the same vertex through any cell reordering performed by the preceding sibling visits.
theorem
Hex.GraphIso.Nauty.LoopInv.picked
{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)
{current tv : Nat}
{child : SearchSt n}
(hc : current < len)
(hat : st.lab[tc + current]! = tv)
(he :
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 })
:
The selected vertex occupies a singleton cell at child entry.
theorem
Hex.GraphIso.Nauty.LoopInv.returned
{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)
{current tv : Nat}
{child out : SearchSt n}
(hc : current < len)
(hat : st.lab[tc + current]! = tv)
(he :
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 })
(hout : SearchOut G level (level + 1) child out)
:
A child's reached labelling remains in the frozen parent cell frame, with its individualized vertex still at the target position.
theorem
Hex.GraphIso.Nauty.LoopInv.localPairs
{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)
(hp : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(p : VSet n × VSet n)
:
Every retained ledger pair accepted by this frame's fixed points stabilizes its frozen cells, independently of the mutable target set.
theorem
Hex.GraphIso.Nauty.OtherSweep.hyp
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len : Nat}
{tcell : VSet n}
{codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{inf runFuel tv1 e loopFuel : Nat}
(h :
OtherSweep G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel cursor
tcell st best trail)
:
Every recorded sweep fragment exposes its entry invariant.