theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_smallOutput_paid (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (Z : ℝ), 0 ≤ Z → Z ≤ ↑N ^ (1 / 4) → 8000 * ↑⌈Z⌉₊ ≤ δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Pay the actual weighted small-output term, uniformly in the later sieve cutoff.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_buchstabExcess_paid (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (τ : ℝ), 0 ≤ τ → τ ≤ 1 → 8 * (1 + τ) ^ 3 * SingularSeries.liuSingularSeries N * (8400 * ↑N / ↑N ^ (4 / 53)) / Real.log ↑N ≤ δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Pay the ambient-prime-divisor excess after the proved uniform Euler factor. The prime-size threshold is uniform in every later tau in [0,1].