theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.recovered {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel : Nat} {l : Loop n} {bs fs ds : List Nat} {cursor : Option Nat} {cell smaller : VSet n} {st : State n} {parents : Parents n} {tv : Nat} (h : SweepInput G tcLevel l bs fs cursor cell st parents) (htv : cursor = some tv) (hr : have p := Loop.parent G.graph tcLevel l st bs cell tv; have ch := Parent.child G.graph tcLevel p; ReturnCodes G.graph ch.codes ds fs (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd) (resume : have p := Loop.parent G.graph tcLevel l st bs cell tv; Resumed G tcLevel p ds fs (Parent.back G.graph tcLevel fuel p) parents) (hd : have p := Loop.parent G.graph tcLevel l st bs cell tv; have ch := Parent.child G.graph tcLevel p; Covers (Frame.key G.graph tcLevel ch) (State.best G.graph (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd)) (hsub : ∀ (v : Nat), smaller.mem v = true → cell.mem v = true) (hc : have p := Loop.parent G.graph tcLevel l st bs cell tv; Cell.Cover G.graph tcLevel (Loop.cell G.graph tcLevel l) (Remaining (smaller.nextElem (some tv)) smaller) (State.key G.graph ds (Parent.back G.graph tcLevel fuel p))) : have p := Loop.parent G.graph tcLevel l st bs cell tv; SweepInput G tcLevel l ds fs (smaller.nextElem (some tv)) smaller (Parent.back G.graph tcLevel fuel p) parents

Once an actual off-path child is covered, recovery establishes the complete next-sibling context for every filtered subset with proved ranked coverage. Code histories and geometry come from the native receiving theorem; no full-search correctness is required to restore them.