theorem
Hex.GraphIso.Nauty.Max.SweepInput.canon_past
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
{previous : Option Nat}
(hp : Generation.CanonPast level tc previous st)
(hnext : cell.nextElem previous = some tv)
:
have raw :=
(Nauty.node (first && tv == tv1) ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(child first level tc tv st)).snd;
have middle := if (first && tv == tv1) = true then afterChildFirst level tv1 raw else raw;
have left :=
{ lab := middle.lab, ptn := middle.ptn, active := middle.active, orbits := middle.orbits,
fixedpts := middle.fixedpts.erase tv, autos := middle.autos, wsCap := middle.wsCap, firstcode := middle.firstcode,
canoncode := middle.canoncode, firsttc := middle.firsttc, firstlab := middle.firstlab, canonlab := middle.canonlab,
canong := middle.canong, samerows := middle.samerows, compCanon := middle.compCanon,
eqlevFirst := middle.eqlevFirst, eqlevCanon := middle.eqlevCanon, gcaFirst := middle.gcaFirst,
gcaCanon := middle.gcaCanon, canonlevel := middle.canonlevel, noncheaplevel := middle.noncheaplevel,
allsamelevel := middle.allsamelevel, cosetindex := middle.cosetindex, stabvertex := middle.stabvertex,
numnodes := middle.numnodes, tctotal := middle.tctotal, canupdates := middle.canupdates,
numorbits := middle.numorbits, numgenerators := middle.numgenerators, numbadleaves := middle.numbadleaves,
maxlevel := middle.maxlevel, order := middle.order, genTrace := middle.genTrace, workperm := middle.workperm };
Generation.CanonPast level tc (some tv) (recover (n + 2) level left)
Receiving an actual child keeps the canonical source behind the next cursor, whether the child retained or replaced the reference.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.canon_earlier
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first childFirst : Bool}
{level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
{previous : Option Nat}
(hp : Generation.CanonPast level tc previous st)
(hnext : cell.nextElem previous = some tv)
:
have out :=
(Nauty.node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd;
out.gcaCanon = level →
∃ (o : Nat), o < (Loop.prepare ctx tcLevel l).snd.snd.snd.fst ∧ out.canonlab[tc]! = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab[tc + o]! ∧ (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab[tc + o]! < tv ∧ cellsPerm (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn level
(Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab out.canonlab
A canonical return to this receiver names an earlier original child, including when a previous filter removed that child from the live set.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.return_chosen
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first childFirst : Bool}
{level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
:
The actual returned child still labels its individualized singleton by the chosen vertex, before partition recovery.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.reference_visit
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel boundary level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{short : Bool}
{st out : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel false level numcells tc tv1 (some tv) cell index st l bs fs parents)
{previous : Option Nat}
{R : RefineSt n}
{targets : List Nat}
{key : Key n}
(hit : IterOk ctx level R)
(hlab : R.lab = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab)
(hptn : R.ptn = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn)
(hcover :
Generation.PathCover ctx tcLevel boundary level R tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst targets key cell
previous)
(hpast : Generation.CanonPast level tc previous st)
(hnext : cell.nextElem previous = some tv)
(hguide : st.gcaFirst < level)
(hcall :
Nauty.node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child false level tc tv st) = (Generic.Exit.unwind level short, out))
(hsize : out.canonlab.size = n)
(hgsz : ctx.g.size = n)
(hreceipt :
∀ (o : Nat),
o < (Loop.prepare ctx tcLevel l).snd.snd.snd.fst →
R.lab[tc + o]! = tv →
Generation.ChildPath ctx tcLevel boundary level R tc targets key o → RefReturn ctx level out)
:
Generation.PathCover ctx tcLevel boundary level R tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst targets key cell
(some tv)
A received matching-reference return advances the absence ledger. Canonical returns use an earlier reference; first-reference and orbit returns cannot be received at an off-path frame.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.reference_filters
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel boundary : Nat}
{first short : Bool}
{level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st out : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
{R : RefineSt n}
{targets : List Nat}
{key : Key n}
(hit : IterOk ctx level R)
(hlab : R.lab = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab)
(hptn : R.ptn = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn)
(hcover :
Generation.PathCover ctx tcLevel boundary level R tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst targets key cell
(some tv))
(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)
(hcall :
Nauty.node (first && tv == tv1) ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st) = (Generic.Exit.unwind level short, out))
:
have middle := if (first && tv == tv1) = true then afterChildFirst level tv1 out else out;
have left :=
{ lab := middle.lab, ptn := middle.ptn, active := middle.active, orbits := middle.orbits,
fixedpts := middle.fixedpts.erase tv, autos := middle.autos, wsCap := middle.wsCap, firstcode := middle.firstcode,
canoncode := middle.canoncode, firsttc := middle.firsttc, firstlab := middle.firstlab, canonlab := middle.canonlab,
canong := middle.canong, samerows := middle.samerows, compCanon := middle.compCanon,
eqlevFirst := middle.eqlevFirst, eqlevCanon := middle.eqlevCanon, gcaFirst := middle.gcaFirst,
gcaCanon := middle.gcaCanon, canonlevel := middle.canonlevel, noncheaplevel := middle.noncheaplevel,
allsamelevel := middle.allsamelevel, cosetindex := middle.cosetindex, stabvertex := middle.stabvertex,
numnodes := middle.numnodes, tctotal := middle.tctotal, canupdates := middle.canupdates,
numorbits := middle.numorbits, numgenerators := middle.numgenerators, numbadleaves := middle.numbadleaves,
maxlevel := middle.maxlevel, order := middle.order, genTrace := middle.genTrace, workperm := middle.workperm };
have small := if short = true then shortprune cell left else cell;
have filtered := if (!first && tv == tv1) = true then longprune small left.fixedpts left.autos else small;
Generation.PathCover ctx tcLevel boundary level R tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst targets key filtered
(some tv)
Both executable pruning filters preserve the matching-reference ledger using the checked workspace from the actual returned child.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.reference_child
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel boundary : Nat}
{first : Bool}
{level numcells tc tv1 tv index o : Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
{R : RefineSt n}
{targets : List Nat}
{key : Key n}
(hit : IterOk ctx level R)
(hlab : R.lab = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab)
(hptn : R.ptn = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn)
(hnc : R.numcells = numcells)
(hgsz : ctx.g.size = n)
(ho : o < (Loop.prepare ctx tcLevel l).snd.snd.snd.fst)
(hat : R.lab[tc + o]! = tv)
(href : Generation.ChildPath ctx tcLevel boundary level R tc targets key o)
:
Generation.RefPath ctx tcLevel boundary (level + 1)
(SearchState.refined ctx (level + 1) (numcells + 1) (child first level tc tv st)) targets key
Reordering the receiving frame transports its frozen child reference to the exact arrays individualized by the search.