theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9_logCube_error_payment {ζ : ℝ} (hζ : 0 < ζ) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ↑N / Real.log ↑N ^ 3 ≤ ζ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The remaining log-cubed additive error is small on the true Liu scale, using the already proved positive uniform lower bound for the singular series.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9S5Low_weighted_mass_upper (τ ζ : ℝ) (hτ : 0 < τ) (hζ : 0 < ζ) {e ε δ ρ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ < 1 / 4) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → Even N → ↑(goldbachS5ClosedBelow (goldbachDifferenceCarrier N e) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10))) ≤ 4 * (1 + τ) * SingularSeries.liuSingularSeries N * ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9RectangleMass N ρ k / Real.log (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) + ζ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

A single remaining analytic object: the actual occupied weighted mass. All other errors have been absorbed on the original singular-series scale.