noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachSharpElementaryMargin : ℝ

The remaining fixed scalar margin, with a proved elementary lower bound for C67.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachSharpElementaryMargin = 4 * G67SumCoordinate.piecewiseIntegral + 124341093 / 200000000 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PaperSplitIntegral - 10385101 / 100000000 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12SharpIntegralConstant

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

Actual D19 ledger with every integral on fixed, explicitly known intervals.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.eventually_onePlusOneNine_of_sharp_margin_pos (hpos : 0 < goldbachSharpElementaryMargin) : ∃ (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

Conditional proof exit only: the numerical scalar positivity is NOT supplied here.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.sharp_margin_lower_of_integral_bounds (h67 : 54233 / 10000 ≤ 4 * G67SumCoordinate.piecewiseIntegral) (h9 : goldbachB9PaperSplitIntegral ≤ 527231 / 100000) (h12 : goldbachG12SharpIntegralConstant ≤ 66821 / 100000) : 1 / 2000 ≤ goldbachSharpElementaryMargin

Three explicit scalar bounds suffice; none of the three bounds is asserted here.