theorem
Hex.GraphIso.Nauty.Sparse.Max.SweepInput.finished
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{l : Loop n}
{bs fs : List Nat}
{cell : VSet n}
{st : State n}
{parents : Parents n}
(h : SweepInput G tcLevel l bs fs none cell st parents)
:
An exhausted native cursor covers every original selected child, and its settled code machine identifies the readable incumbent.
theorem
Hex.GraphIso.Nauty.Sparse.Max.SweepInput.skipped
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{l : Loop n}
{bs fs : List Nat}
{cell : VSet n}
{st : State n}
{parents : Parents n}
{tv : Nat}
(h : SweepInput G tcLevel l bs fs (some tv) cell st parents)
(hs : (!l.first || st.orbits[tv]! == tv) = false)
:
SweepInput G tcLevel l bs fs (cell.nextElem (some tv)) cell st parents
The actual orbit skip preserves the whole traversal context and advances ranked coverage in the frozen selected cell.
theorem
Hex.GraphIso.Nauty.Sparse.Max.lower_sweep
{n k : Nat}
(G : Sparse.Colored n k)
(tcLevel fuel : Nat)
(hd : NodeMax G tcLevel fuel)
(cfuel : Nat)
(l : Loop n)
(bs fs : List Nat)
(tv1 index : Nat)
(cursor : Option Nat)
(cell : VSet n)
(st : State n)
(parents : Parents n)
(h : SweepInput G tcLevel l bs fs cursor cell st parents)
(hfuel : n ≤ l.node.level + fuel)
(hcursor : Generic.CursorFuel n cfuel cursor)
(hpast : Generic.Past l.first tv1 cursor)
:
have out :=
Generic.sweep l.first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel l.node.level
(Loop.cell G.graph tcLevel l).numcells (Loop.cell G.graph tcLevel l).tc tv1 cursor cell index st;
ExitCover (Frame.key G.graph tcLevel l.node) (State.best G.graph out.snd.snd) l.node.level
(Witness G tcLevel (parents.frames.insert l.node)) out.fst
The complete native sibling recursion preserves lower coverage, including both pruning filters, orbit skips, hinted targets and nonlocal returns. Only the smaller off-path node result is an induction premise.