theorem G12MovingEuler.mass_nonneg (N : ℕ) (B : Finset (ℕ × ℕ)) : 0 ≤ G12FlexibleWF.mass N B

The original mother mass is nonnegative; no division by the mass is used.

theorem G12MovingEuler.exists_scaled_rectangle_normalized : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (δ : ℝ), 0 < δ → ∃ (ζ : ℝ), 0 < ζ ∧ ζ ≤ 1 / 100 ∧ ∃ (η : ℝ), 0 < η ∧ η < 1 / 8 ∧ ∀ (e : ℝ), 0 < e → e ≤ 1 → ∀ (A : ℕ), ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (M U T V : ℕ), 1 ≤ M → M ≤ U → U ≤ 2 * M → 1 ≤ T → T ≤ V → V ≤ 2 * T → ↑N ^ (4 / 53) ≤ ↑T → ↑V < ↑N ^ (1 / 10) → e * ↑N ≤ 4 * ↑M * ↑T → 4 * ↑M * ↑T ≤ 4 * ↑N → ∀ (r : ℝ), ↑T ≤ r → ↑N ^ (4 / 53) ≤ r → r ≤ ↑N ^ (1 / 10) → have x := 4 * ↑M * ↑T; have Q := G12LocalScale.level x (↑T) ζ; have Z := √Q; have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z; have D := MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η; have S := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z; (↑N ^ (1 / 3) ≤ Q ∧ Q ≤ ↑N ∧ 2 ≤ D) ∧ 2 ≤ Z ∧ ∀ (ε : ℝ), have B := G12FlexibleRectangle.rectangle N ε M U T V; (400 * ∑ p ∈ B, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ ⋯ / Real.log ↑N + 400 * ↑S.card * (x / Real.log x ^ A) + 400 * ↑S.card * G12FlexibleWF.correctionBudget N Q η + 8000 * ↑⌈Z⌉₊

Actual fine-cell main-term consumer. It preserves the physical C2 tag fee, signed-correction budget, and small-output fee. It is not a low-band integral closure. Choices are K,C then delta then zeta then eta, with e fixed before the common N0.