theorem Hex.GraphIso.Nauty.Sparse.trace_sweep {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel : Nat) (hd : ∀ (level numcells : Nat) (st : State n), 1 ≤ level → TraceEntry G tcLevel level numcells st → TraceOk G (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd) (cfuel : Nat) (first : Bool) (level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ level) (h : TraceReady G tcLevel level numcells st) (ht : Generic.Target State.frame level tc cell st) (hv : ∀ (v : Nat), cursor = some v → cell.mem v = true) (hpast : Generic.Past first tv1 cursor) (hrecord : CheapRecorded level tc st) : TraceOk G (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

Later siblings preserve trace soundness from the smaller-depth node induction hypothesis. Every resumption reconstructs its native history and target membership after the actual filters and recovery.