theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstEntry.sweep_upper
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel tv last : Nat}
{f : Frame n}
{leaf : State n}
{parents : Parents n}
(h : FirstEntry G f)
(hs : Scope G tcLevel f [] f.entry parents)
(hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n)
(htv :
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv)
(horbit :
(cheapCheck true f.level
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells
f.entry).snd.snd.snd.snd).orbits[tv]! = tv)
(path :
have p := Frame.firstParent G.graph tcLevel f [] tv;
Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel (Parent.child G.graph tcLevel p).level
(Parent.child G.graph tcLevel p).numcells (Parent.child G.graph tcLevel p).entry last leaf)
(hf : n ≤ f.level + fuel)
(hchild :
have p := Frame.firstParent G.graph tcLevel f [] tv;
have ch := Parent.child G.graph tcLevel p;
Bounded (Frame.key G.graph tcLevel ch) none
(State.best G.graph
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd))
:
The actual first-child bound extends through the complete native sibling sweep, including local filters and nonlocal returns.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.first_sweep_step
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{f : Frame n}
(next : Generic.SweepFn (State n) n)
(hd : (Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry).fst ≠ n)
:
Generic.nodeStep (Graph.ofGraph G) tcLevel next true f.level f.numcells f.entry = have r := Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry;
have s :=
next true f.level r.fst r.snd.fst.toNat ((r.snd.snd.fst.nextElem none).getD 0) (r.snd.snd.fst.nextElem none)
r.snd.snd.fst 0 (cheapCheck true f.level r.snd.snd.snd.snd);
match s.fst with
| Generic.Exit.done =>
(Generic.Exit.unwind (f.level - 1) false, Generic.Policy.afterSweep true f.level r.snd.snd.snd.fst s.snd.fst s.snd.snd)
| x => (s.fst, s.snd.snd)
Native first preparation enters the literal sibling continuation when its refined partition remains nondiscrete.