theorem G12RectangleWF.exists_rectangle_C2_sieve : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (η : ℝ), 0 < η → η < 1 / 8 → ∀ (Cscale ζ : ℝ), 1 ≤ Cscale → 0 < ζ → ζ ≤ 1 / 10 → ∀ (A : ℕ), ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T : ℕ), 1 ≤ M → 1 ≤ T → ∀ (ν : ℝ), 4 * ↑M * ↑T = x → ζ ≤ ν → ν ≤ 1 / 10 + ζ / 10 → ↑T = x ^ ν → ∀ (N : ℕ), 0 < N → ↑N ≤ Cscale * x → Even N → ∀ (ε Z : ℝ), 2 ≤ Z → Z ≤ √(x ^ ((5 - 5 * ν) / 9 - ζ)) → have Q := x ^ ((5 - 5 * ν) / 9 - ζ); 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; have V := ∏ p ∈ P, (1 - AnalyticNumberTheory.Sieve.goldbachNu p); have E := C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); (400 * ∑ p ∈ G12LowRectangle.rectangle N ε M T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ 400 * mass N ε M T * V * (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log Z) + E) + 400 * ↑S.card * (x / Real.log x ^ A) - 400 * ∑ t ∈ S, (gate N (G12LowRectangle.rectangle N ε M T) (Finset.Ioc 0 ⌊Q⌋₊) ⇑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t) + outsidePrimorial N ε Z Q M T ⇑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t)) + smallOutput N ε Z M T

The actual producer and C2 consume the same full family. The only signed remainders left here are the explicit gcd and outside-primorial corrections. No boundary payment or sharp low-band asymptotic is asserted.