theorem G12FlexibleWF.exists_scaled_rectangle_C2_sieve : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (δ : ℝ), 0 < δ → ∃ (ζ : ℝ), 0 < ζ ∧ ζ ≤ 1 / 100 ∧ ∀ (e η : ℝ), 0 < e → e ≤ 1 → 0 < η → η < 1 / 8 → ∀ (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) ζ; (↑N ^ (1 / 3) ≤ Q ∧ Q ≤ ↑N ∧ 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) ∧ 4 * Real.log ↑N / Real.log Q ≤ 36 / (5 * (1 - Real.log r / Real.log ↑N)) + δ ∧ ∀ (ε Z : ℝ), 2 ≤ Z → 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; have B := G12FlexibleRectangle.rectangle N ε M U T V; have Euler := ∏ p ∈ P, (1 - AnalyticNumberTheory.Sieve.goldbachNu p); have E := C * (η + ⋯ * Real.log Q ^ (-(1 / 3))); 400 * ∑ p ∈ B, ⋯ ≤ ⋯ + 400 * ↑S.card * correctionBudget N Q η + 8000 * ↑⌈Z⌉₊

Uniform ambient admission is genuinely fed to the physical same-family C2 sieve. The scalar coefficient estimate is retained alongside, not advertised as an already-normalized Euler or Buchstab main term.