theorem
Hex.GraphIso.Nauty.Max.Loop.ancestors
{n : Nat}
(ctx : Ctx n)
(tcLevel : Nat)
(l : Loop n)
:
Internal preparation preserves both saved ancestor counters.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.references
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
:
At sweep initialization both reference-coverage conditions are vacuous; the entry bounds hold at the actual root and are preserved at every first-child descent.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.small
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
(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)
(hinternal :
first = false →
have p := prepareOther ctx tcLevel f.level f.numcells f.entry;
(classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.internal)
:
have l := { node := f, first := first };
have p := Loop.prepare ctx tcLevel l;
p.snd.snd.snd.snd.noncheaplevel ≤ f.level →
SubtreeOk ctx f.level
{ lab := p.snd.snd.snd.snd.lab, ptn := p.snd.snd.snd.snd.ptn, active := p.snd.snd.snd.snd.active, numcells := p.fst,
hint := 0, maxpos := 0, longcode := 0 }
The actual internal preparation initializes the sweep's small-cell premise on both first-path and off-path entries.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.recovered_small
{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)
(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)
:
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 };
have ready := recover (n + 2) level left;
ready.noncheaplevel ≤ level →
SubtreeOk ctx level
{ lab := ready.lab, ptn := ready.ptn, active := ready.active, numcells := numcells, hint := 0, maxpos := 0,
longcode := 0 }
An actual child return preserves the receiving sweep's small-cell premise through first-child cleanup and partition recovery.