theorem
Hex.GraphIso.Nauty.OtherSweep.reference
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel runFuel level numcells tc len tv1 e boundary : Nat}
{codes fs targets : List Nat}
{rsLab rsPtn : Array Nat}
{base : SearchSt n}
{key : Key n}
(hg : ctx.g = rowsOf G)
(hinf : inf = n + 2)
(hpath : level = codes.length)
(hrun : n + 2 < level + 1 + runFuel)
(hboundary : level < boundary)
(hvisit :
∀ {bs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {tv o : Nat} {tcell : VSet n}
{cursor : Option Nat},
OtherLoopHyp G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor e base st best
trail →
tcell.nextElem cursor = some tv →
o < len →
rsLab[tc + o]! = tv →
Generation.Matches ctx (level + 1) st targets key →
st.eqlevFirst = level →
boundary ≤ st.allsamelevel →
st.gcaFirst < level →
Generation.ChildPath ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc targets key
o →
have 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 };
Generation.RefReturn ctx (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) child).snd
(otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) child).fst)
{loopFuel : Nat}
{cursor : Option Nat}
{tcell : VSet n}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(sweep :
OtherSweep G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn base loopFuel cursor
tcell st best trail)
(hcover :
Generation.PathCover ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc len targets key tcell cursor)
(hocc :
∃ (o : Nat), o < len ∧ Generation.ChildPath ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc targets key o)
(hpast : Generation.CanonPast level tc cursor st)
(hm : Generation.Matches ctx (level + 1) st targets key)
(heq : st.eqlevFirst = level)
(hsame : boundary ≤ st.allsamelevel)
(hguide : st.gcaFirst < level)
(hcheap : level < st.noncheaplevel)
:
Above both saved pruning boundaries, a sweep containing the sought reference returns automorphism evidence. The child premise is the recursive generation obligation; the sweep proof follows the recorded visits and their actual short- and long-prune filters.