theorem
Hex.GraphIso.Nauty.Sparse.recover_best
{n : Nat}
(G : SparseGraph n)
(inf level : Nat)
(st : State n)
:
Native recovery changes neither the readable incumbent nor its code array.
theorem
Hex.GraphIso.Nauty.Sparse.recover_long
{n : Nat}
(inf level : Nat)
(st : State n)
(cell : VSet n)
:
Generic.Policy.longprune cell (Generic.Policy.recover inf level st) = Generic.Policy.longprune cell st
The native long filter observes the same fixed set and workspace before and after recovery, including its cache invalidation.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.resume
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{c : Cell n}
{out : State n}
{cell : VSet n}
{tv tv1 index : Nat}
{first : Bool}
{next : Generic.SweepFn (State n) n}
{result : Exit × Nat × State n → Prop}
(h : Cover G.graph tcLevel c (Remaining (cell.nextElem (some tv)) cell) (State.best G.graph out))
(hc : Valid G c)
(he : FrameOut G c.level c.level c.entry (Generic.Policy.recover (n + 2) c.level out))
(hp : PairsReady G tcLevel c.level c.numcells (Generic.Policy.recover (n + 2) c.level out))
(hs : ∀ (v : Nat), cell.mem v = true → c.vertices.mem v = true)
(hnext :
∀ (smaller : VSet n),
(∀ (v : Nat), smaller.mem v = true → cell.mem v = true) →
∀ (index : Nat),
Cover G.graph tcLevel c (Remaining (smaller.nextElem (some tv)) smaller)
(State.best G.graph (Generic.Policy.recover (n + 2) c.level out)) →
result
(next first c.level c.numcells c.tc tv1 (smaller.nextElem (some tv)) smaller index
(Generic.Policy.recover (n + 2) c.level out)))
:
result (Generic.resume (n + 2) next first c.level c.numcells c.tc tv1 tv cell index out)
The actual native resumption supplies the next continuation with coverage of its literal cursor and filtered target. Pair validity is used after recovery; the filter observes identical fields before recovery.