theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalar_exact_bounds : goldbachPositiveScalarExactRational ≤ goldbachWeightFiveNegativeScalarCoefficient ∧ goldbachWeightFiveNegativeScalarCoefficient ≤ goldbachPositiveScalarExactRational + 3 / 5000000

Full analytic error budget, before the one final rational rounding.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightFiveNegativeScalarCoefficient_ge_62033529 : 62033529 / 100000000 ≤ goldbachWeightFiveNegativeScalarCoefficient

Unconditional named rational lower bound for the complete literal five-negative coefficient.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightFiveNegativeScalarCoefficient_rational_error : 0 ≤ goldbachWeightFiveNegativeScalarCoefficient - 62033529 / 100000000 ∧ goldbachWeightFiveNegativeScalarCoefficient - 62033529 / 100000000 ≤ 1 / 10 ^ 6

The whole certified gap, including the final downward rounding, is at most 10^-6.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_remainingFive_rationalPositiveScalar_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))) + (62033529 / 100000000 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Actual signed D19 terminal. No sign assertion is made for RemainingFive or D19.