theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10Retained.goldbachB10I10_eight_mul_le_540995781 : 8 * goldbachB10I10 ≤ 540995781 / 100000000

Unconditional purely analytic bound for the unchanged production integral I10.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10Retained.goldbachB10SiftedCount_540995781_upper (δ : ℝ) (hδ : 0 < δ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → have Δ := ↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1); have Z := Δ ^ (1 / 2); ↑(goldbachB10SiftedCount N ε (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma) Z) ≤ (540995781 / 100000000 * (1 - ε) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Actual B10SiftedCount at the unchanged legal cutoff, retaining (1-ε). This statement concerns neither an original G10 count nor a corrected G10 count.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10Retained.retained_scalar_gain : 540996 / 100000 - 540995781 / 100000000 = 219 / 100000000

Exact recovery from the previously published rational scalar.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.B10Retained.retained_scalar_strict_improvement : 540995781 / 100000000 < 540996 / 100000