theorem
Hex.GraphIso.Nauty.Max.SweepInput.received
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : 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)
(hr :
have p := { loop := l, state := st, chosen := tv, bs := bs, fs := fs };
Generic.Result (Frame.key ctx tcLevel (Parent.child ctx tcLevel p))
(SearchState.key ctx bs (Parent.child ctx tcLevel p).entry) (SearchState.best ctx out) level
(Witness ctx tcLevel (Parents.frames ctx tcLevel (parents.push p))) (Generic.Exit.unwind level short))
:
CellCover ctx tcLevel (n - level) level numcells tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst (Loop.codes ctx l)
(Loop.prepare ctx tcLevel l).snd.snd.snd.snd (fun (v : Nat) => Remaining (some tv) cell v ∧ tv < v)
(SearchState.best ctx out)
Reception uses the child's coverage clause at precisely its stop level, then absorbs that child into the sweep's prior coverage.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.pair
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{level numcells tc tv1 index : Nat}
{cursor : Option Nat}
{cell fix mcr : 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 cursor cell index st l bs fs parents)
(hp : PairOk ctx.g st.ptn st.lab level fix mcr)
:
A local pair valid in the sweep's current ordering is also valid in its frozen ordering, with the same carrier and fixed vertices.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.short_pair
{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 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)
(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 true, out))
(fix mcr : VSet n)
:
A received short return supplies a valid pair in the frozen parent frame from its actual checked output and the parent's reference guide.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.short_cover
{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 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)
(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 true, out))
(hr :
have p := { loop := l, state := st, chosen := tv, bs := bs, fs := fs };
Generic.Result (Frame.key ctx tcLevel (Parent.child ctx tcLevel p))
(SearchState.key ctx bs (Parent.child ctx tcLevel p).entry) (SearchState.best ctx out) level
(Witness ctx tcLevel (Parents.frames ctx tcLevel (parents.push p))) (Generic.Exit.unwind level true))
:
CellCover ctx tcLevel (n - level) level numcells tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst (Loop.codes ctx l)
(Loop.prepare ctx tcLevel l).snd.snd.snd.snd
(fun (v : Nat) => (Remaining (some tv) cell v ∧ tv < v) ∧ (shortprune cell out).mem v = true)
(SearchState.best ctx out)
The actual received short filter preserves prior coverage after the child's stop-level coverage has been incorporated.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.long_cover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{level numcells tc tv1 tv index : Nat}
{cell smaller : VSet n}
{st out : Search n}
{exit : Generic.Exit}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
{live : Nat → Prop}
{best : Option (Key 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)
(hcall :
Nauty.node (first && tv == tv1) ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st) = (exit, out))
(hc :
CellCover ctx tcLevel (n - level) level numcells tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst (Loop.codes ctx l)
(Loop.prepare ctx tcLevel l).snd.snd.snd.snd live best)
(hsub :
∀ (v : Nat),
live v →
(windowSet n (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst).mem
v = true)
(hmem : ∀ (v : Nat), live v → smaller.mem v = true)
:
The long filter after an actual child uses the restored parent fixed set to interpret every admitted pair in the original target frame.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.filtered
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : 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)
(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))
(hr :
have p := { loop := l, state := st, chosen := tv, bs := bs, fs := fs };
Generic.Result (Frame.key ctx tcLevel (Parent.child ctx tcLevel p))
(SearchState.key ctx bs (Parent.child ctx tcLevel p).entry) (SearchState.best ctx out) level
(Witness ctx tcLevel (Parents.frames ctx tcLevel (parents.push p))) (Generic.Exit.unwind level short))
:
have small := if short = true then shortprune cell out else cell;
have filtered := if (!first && tv == tv1) = true then longprune small (out.fixedpts.erase tv) out.autos else small;
CellCover ctx tcLevel (n - level) level numcells tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst (Loop.codes ctx l)
(Loop.prepare ctx tcLevel l).snd.snd.snd.snd (Remaining (filtered.nextElem (some tv)) filtered)
(SearchState.best ctx out)
Reception composes child coverage, both actual filters, and cursor advance in the frozen target frame for either short-return flag.
theorem
Hex.GraphIso.Nauty.Max.recover_best
{n : Nat}
(ctx : Ctx n)
(inf level : Nat)
(st : Search n)
:
Partition recovery changes neither the installed codes nor their labelling.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.receive_call
{n k : Nat}
{G : Colored n k}
{tcLevel fuel cfuel : 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 { g := rowsOf G } tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
(hvisit : (!first || st.orbits[tv]! == tv) = true)
(hcall :
Nauty.node (first && tv == tv1) { g := rowsOf G } (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(child first level tc tv st) = (Generic.Exit.unwind level short, out))
(next : Generic.SweepFn (Search n) n)
:
have ctx := { g := rowsOf G };
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;
have ready := recover (n + 2) level left;
have nextIndex := if (first && ready.orbits[tv]! == tv1) = true then index + 1 else index;
Generic.sweepStep (n + 2) (Generic.nodeCall ctx (n + 2) tcLevel fuel) next first level numcells tc tv1 tv cell index
st = next first level numcells tc tv1 (filtered.nextElem (some tv)) filtered nextIndex ready ∧ CellCover ctx tcLevel (n - level) level numcells tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst (Loop.codes ctx l)
(Loop.prepare ctx tcLevel l).snd.snd.snd.snd (Remaining (filtered.nextElem (some tv)) filtered)
(SearchState.best ctx ready)
At the receiving level, the actual sweep calls its suffix with coverage produced by the child induction hypothesis, both filters, and recovery. First-child cleanup and either short flag are included.