theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.advance
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel runFuel : Nat}
{c : Cell n}
{st out : State n}
{cell : VSet n}
{tv tv1 index : Nat}
{bs : List Nat}
{first short : Bool}
{witness : Nat → Option (Key n) → Prop}
{next : Generic.SweepFn (State n) n}
{result : Exit × Nat × State n → Prop}
(h : Cover G.graph tcLevel c (Remaining (some tv) cell) (State.key G.graph bs st))
(hc : Valid G c)
(he : FrameOut G c.level c.level c.entry st)
(hp : PairsReady G tcLevel c.level c.numcells st)
(ht : Generic.Target State.frame c.level c.tc cell st)
(hv : cell.mem tv = true)
(hs : ∀ (v : Nat), cell.mem v = true → c.vertices.mem v = true)
(hrecord : CheapRecorded c.level c.tc st)
(hcanon : st.gcaCanon ≤ c.level)
(hcap : 0 < st.wsCap)
(hguide : CanonGuide c.level c.tc c.entry (key G.graph tcLevel c) (State.key G.graph bs st) st)
(hcall :
Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel runFuel (c.level + 1) (c.numcells + 1)
(Generic.Policy.child first c.level c.tc tv st) = (Generic.Exit.unwind c.level short, out))
(hr :
MaxResult (Frame.key G.graph tcLevel (c.child first st tv)) (State.key G.graph bs (c.child first st tv).entry)
(State.best G.graph out) c.level witness (Generic.Exit.unwind c.level short))
(hnext :
have back := Generic.Policy.recover (n + 2) c.level (Generic.Policy.leaveChild tv out);
∀ (smaller : VSet n),
(∀ (v : Nat), smaller.mem v = true → cell.mem v = true) →
∀ (index : Nat),
FrameOut G c.level c.level c.entry back →
PairsReady G tcLevel c.level c.numcells back →
Cover G.graph tcLevel c (Remaining (smaller.nextElem (some tv)) smaller) (State.best G.graph back) →
result (next first c.level c.numcells c.tc tv1 (smaller.nextElem (some tv)) smaller index back))
:
result
(Generic.advance (n + 2) next first c.level c.numcells c.tc tv1 tv cell index (Generic.Policy.leaveChild tv out)
(Generic.Exit.unwind c.level short))
Receiving an actual off-path child composes its maximum result with both native filters, parent recovery and the next executable cursor. The workspace validity and frame of the resumed state come from the complete native child call, rather than additional continuation assumptions.