theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.reference_filters {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel boundary tv tv1 : Nat} {l : Loop n} {bs fs : List Nat} {cell : VSet n} {st out : State n} {parents : Parents n} {targets : List Nat} {key : Key n} {short : Bool} (h : SweepInput G tcLevel l bs fs (some tv) cell st parents) : have c := Loop.cell G.graph tcLevel l; have R := State.refined (Graph.ofGraph G.graph) l.node.level l.node.numcells l.node.entry; have left := Generic.Policy.leaveChild tv out; 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) → Generation.PathCover G.graph tcLevel boundary l.node.level R c.tc c.len targets key cell (some tv) → Generation.PathCover G.graph tcLevel boundary l.node.level R c.tc c.len targets key filtered (some tv)

Both filters after an actual off-path child preserve the richer reference ledger. The complete native child call supplies receiver pair validity; the recovered partition transports it to the frozen target.