theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67_piecewise_lower_certified : 54233 / 10000 ≤ 4 * G67SumCoordinate.piecewiseIntegral

Both independently proved halves use the same frozen polynomial and loss.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IntegralConstant_lower_certified : 54233 / 10000 ≤ goldbachG67IntegralConstant

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachSharpElementaryMargin_lower_certified : 126891 / 200000000 ≤ goldbachSharpElementaryMargin

Exact retained lower bound for the margin; all three integral estimates are supplied.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachSharpElementaryMargin_pos : 0 < goldbachSharpElementaryMargin

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

Quantitative lower bounds below the retained limit, with the coefficient fixed before the common natural cutoff. The normalization is the Liu singular series.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_onePlusOneNine_nat_unconditional : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9

Unconditional 1+1.9 in exact natural-power syntax.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_onePlusOneNine_unconditional : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ ↑r ≤ ↑q ^ (19 / 10 - 1)

Unconditional 1+1.9 in the source's real-exponent syntax. No integral-bound or positivity premises remain.