theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedIntegral_logError_paid (C δ : ℝ) (hδ : 0 < δ) : ∀ᶠ (N : ℕ) in Filter.atTop, C * ↑N / Real.log ↑N ^ 3 ≤ δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Scalar log payment, reusing the proof of the private B8 normalized-main-mass helper. No new analytic input: only divergence of log and the universal singular-series floor.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedIntegral_envelope_loss (B C τ η ν d W : ℝ) (hB : 0 ≤ B) (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hη : 0 < η) (hν : 0 < ν) (hd : 0 < d) (hW0 : 0 ≤ W) (hW : ∀ u ∈ Set.Icc (17 / 4) (37 / 4), LiLiuPrereqBuchstab.buchstab u ≤ W) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → goldbachG11BuchstabSieveEnvelope N (goldbachG11SieveCutoff B N) 3 C (τ * Real.exp Real.eulerMascheroniConstant) η ≤ (8 * (1 + τ) ^ 3 * (W + η) * ((goldbachG11PrimeIntegral fun (x : ℝ) => 1) + ν) + 3 * d) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Exact envelope: exponent A=3; the three actual remainders are paid separately. The coefficient is the uniform level coefficient 8, not the author's low-band weight.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedIntegral_choose_loss (W δ : ℝ) (hδ : 0 < δ) : ∃ (t : ℝ), 0 < t ∧ t ≤ 1 ∧ 8 * (1 + t) ^ 3 * (W + t) * ((goldbachG11PrimeIntegral fun (x : ℝ) => 1) + t) < (8 * W * goldbachG11PrimeIntegral fun (x : ℝ) => 1) + δ

Continuity selects one strictly positive common loss; no free mesh, distribution, or target-shaped premise is left in the final consumers.