theorem G12FlexibleWF.exists_rectangle_paid_sieve : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (η : ℝ), 0 < η → η < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (Q : ℝ), Q₀ ≤ Q → ∀ (N : ℕ), 2 ≤ N → Even N → ∀ (ε Z : ℝ) (M U T V : ℕ), ↑N ^ (4 / 53) ≤ ↑T → ↑V < ↑N ^ (1 / 10) → 2 ≤ Z → Z ≤ √Q → Q ≤ ↑N → 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η → have A := G12FlexibleRectangle.rectangle N ε M U T V; have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z; have D := MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η; have Euler := ∏ p ∈ P, (1 - AnalyticNumberTheory.Sieve.goldbachNu p); have E := C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); (∀ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z, MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t) Q ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable 1 Q fun (d : ℕ) => (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t) d) ∧ (400 * ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ 400 * mass N A * Euler * (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log Z) + E) + 400 * ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z, |G12FlexibleRectangle.discrepancy N A (Finset.Ioc 0 ⌊Q⌋₊) ⇑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t)| + 400 * ↑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z).card * correctionBudget N Q η + 8000 * ↑⌈Z⌉₊

Actual arbitrary-endpoint output sieve with both full-carrier corrections replaced by proved quantitative budgets; the original full C2 sums remain.