theorem G12SafeGridBudget.all_fees (B : ℕ) {η e : ℝ} (hη : 0 < η) (hηu : η < 1 / 8) (he : 0 < e) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (x Q Z : ℝ), e * ↑N ≤ x → x ≤ 4 * ↑N → ↑N ^ (1 / 3) ≤ Q → Q ≤ ↑N → 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η → Z = √Q → have S := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z; 400 * ↑S.card * (x / Real.log x ^ (B + 1)) + 400 * ↑S.card * G12FlexibleWF.correctionBudget N Q η + 8000 * ↑⌈Z⌉₊ ≤ ↑N / Real.log ↑N ^ B

All three fees from moving normalization, including the numerical correction budget itself. The stronger C2 exponent is fixed before N and every cell.

theorem G12SafeGridBudget.exists_rectangle_paid : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (δ : ℝ), 0 < δ → ∃ (ζ : ℝ), 0 < ζ ∧ ζ ≤ 1 / 100 ∧ ∃ (η : ℝ), 0 < η ∧ η < 1 / 8 ∧ ∀ (e : ℝ), 0 < e → e ≤ 1 → ∀ (B : ℕ), ∃ (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 → ∀ (ε : ℝ), have A := G12FlexibleRectangle.rectangle N ε M U T V; (400 * ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0) ≤ (36 / (5 * (1 - Real.log ↑T / Real.log ↑N)) + δ) * 400 * G12FlexibleWF.mass N A * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N + ↑N / Real.log ↑N ^ B

A real scaled rectangle with every additive fee discharged.