theorem MathlibNt.SieveTheory.filter_range_real_window_eq_sdiff (N : ℕ) (L U : ℝ) (P : ℕ → Prop) [DecidablePred P] (hL : 0 ≤ L) (hLU : L ≤ U) (hUN : U ≤ ↑N) : {r ∈ Finset.range (N + 1) | P r ∧ L < ↑r ∧ ↑r ≤ U} = Finset.filter P (Finset.range (⌊U⌋₊ + 1)) \ Finset.filter P (Finset.range (⌊L⌋₊ + 1))

A finite real half-open window is the difference of its closed prefixes. The arbitrary predicate retains all arithmetic gates, including a product residue.