theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.received {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel tv tv1 : Nat} {l : Loop n} {bs fs : List Nat} {cell : VSet n} {st out : State n} {parents : Parents n} {short : Bool} (h : SweepInput G tcLevel l bs fs (some tv) cell st parents) (hbudget : n ≤ l.node.level + fuel) : have c := Loop.cell G.graph tcLevel l; have left := Generic.Policy.leaveChild tv out; have back := Generic.Policy.recover (n + 2) l.node.level left; have small := if short = true then Generic.Policy.shortprune cell left else cell; have filtered := if (!l.first && tv == tv1) = true then Generic.Policy.longprune small left else small; Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (l.node.level + 1) (c.numcells + 1) (Generic.Policy.child l.first l.node.level c.tc tv st) = (Generic.Exit.unwind l.node.level short, out) → ∃ (ds : List Nat), SweepInput G tcLevel l ds fs (filtered.nextElem (some tv)) filtered back parents

The actual returned child, both literal filters and recovery supply the next complete sweep context. Its maximum coverage comes from the proved native search theorem, independently of generator completeness.