MathlibNt.SieveTheory.LiLiuGoldbachS4RetainedEndpoints

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S4Retained.goldbachB8MainIntegral_eight_mul_le_60961168 :

8 * goldbachB8MainIntegral ≤ 60961168 / 100000000

Pure analytic scalar estimate for the actual production double integral I8.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S4Retained.goldbachB8MainIntegral_eight_mul_le_60961168 · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S4Retained.goldbachS4_normalized_upper_60961168 (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) :

∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ (3 / 11))) ≤ (60961168 / 100000000 + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The unchanged actual S4 count, with all upstream analytic errors already paid.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S4Retained.goldbachS4_normalized_upper_60961168 · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S4Retained.retained_scalar_gain :

60962 / 100000 - 60961168 / 100000000 = 13 / 1562500

Exact recovery from the previously published rational scalar.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S4Retained.retained_scalar_gain · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S4Retained.retained_scalar_strict_improvement :

60961168 / 100000000 < 60962 / 100000

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S4Retained.retained_scalar_strict_improvement · compiled type and proof/definition references.