theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_authorG11_numericLedger (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (515093 / 200000000 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

The author G11 estimate and the previously certified G67/G9/G12 estimates are all applied to their original counts before the signed ledger is closed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_D19_author_lower_of_coefficient_lt (κ : ℝ) (hκ : κ < 515093 / 800000000) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → κ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(D19 N)

Any fixed coefficient strictly below the retained author-G11 ceiling. The common natural threshold follows the coefficient, and no epsilon remains.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_D19_gt_paper_0004 : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → 1 / 2500 * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) < ↑(D19 N)

The paper's strict 0.0004 bound for the original number of distinct primes. A fixed stronger certified coefficient pays strictness; no limiting endpoint coefficient is asserted.