theorem Hex.GraphIso.Nauty.Sparse.pairs_sweep {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel : Nat) (hd : ∀ (level numcells : Nat) (st : State n), 1 ≤ level → PairsEntry G tcLevel level numcells st → PairsOk 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 : PairsReady 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) : PairsOk G (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

Later sibling sweeps preserve the root pruning workspace. Each child return restores its path, boundary and trace histories before another sibling can classify or admit a pair; skipped vertices require only filter inclusion.