theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightFiveCoefficient_zero_ge_allRetained : 124341093 / 200000000 ≤ goldbachWeightFiveCoefficient 0

All already-proved endpoint bounds, with the external S4 multiplier two.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_remainingFive_allRetained_small_epsilon (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightRemainingFive (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) + (124341093 / 200000000 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

The improved constant is consumed in the actual remaining-five theorem.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_allRetainedUniform_consumed_small_epsilon (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z) + (-(682021431 / 200000000) - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Fully connected retained-constant ledger; no estimate of the remaining signed counts.