theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_small_inflation {w a : ℝ} (hw : 0 ≤ w) (hw8 : w ≤ 8) (ha : 0 < a) (ha1 : a ≤ 1) : (1 + a / 128) ^ 2 * (w + a / 8) ≤ w + a

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorFactor_paid (C K τ : ℝ) (hC : 0 ≤ C) (hτ : 0 < τ) : ∃ (δ₀ : ℝ), 0 < δ₀ ∧ δ₀ < 1 / 4 ∧ ∃ (θ₀ : ℝ), 0 < θ₀ ∧ θ₀ < 1 / 8 ∧ ∀ (δ θ : ℝ), 0 ≤ δ → δ < δ₀ → 0 < θ → θ < θ₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (ε ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → ∀ k ∈ goldbachG11GridUsed N ε ρ, ∀ p ∈ goldbachG11GridShort N ρ k, fouvryG9UpperFactor N (goldbachG11MixedLevel N δ ρ k) C K θ * fouvryG9BaseEuler N √↑N * goldbachG11EulerCorrection N ≤ (goldbachG11AuthorWeight (Real.log ↑p / Real.log ↑N) + τ) * (SingularSeries.liuSingularSeries N / Real.log ↑N)

All auxiliary errors are absorbed BEFORE the moving grid and its primes. This is the actual author's weight, not a free coefficient hypothesis.