theorem G12ClippedWindow.residual_eq_ap_counts {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hN : 2 ≤ N) (h : Admissible N ε g L U) (d b : ℕ) : residual N g L U d b = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with m.Coprime d, g m * (↑{r ∈ window N L U m | m * r ≡ b [MOD d]}.card - ↑(window N L U m).card / ↑d.totient)

The distributed residual is exactly the actual AP window discrepancy.

theorem G12ClippedWindow.clamp_window_eq_filter (N m : ℕ) (ε : ℝ) (T V : ℕ → ℝ) : window N (clampLower N ε T V) (clampUpper N ε V) m = {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | T m < ↑r ∧ ↑r ≤ V m}

Empty normalization changes no prime atoms: the clamp is the literal intersection.

theorem G12ClippedWindow.longMask_mass_eq (N : ℕ) (ε : ℝ) (cellLong longOK : ℕ → Prop) (T V : ℕ → ℝ) : mass N (longMask N cellLong longOK) (clampLower N ε T V) (clampUpper N ε V) = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with cellLong m ∧ ¬longOK m, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | T m < ↑r ∧ ↑r ≤ V m}.card

The full clipped mass really is the coefficient-weighted cardinality of the cell.