theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_strictEndpoint_mainMass_lower (ε η : ℝ) (hε : 0 < ε) (hεu : ε < 1) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → have m := ⌈(1 - ε) * ↑N⌉₊ - 1; 2 ≤ m ∧ m ≤ N ∧ (1 - ε - η) * (↑N / Real.log ↑N) ≤ BombieriVinogradov.trueLogarithmicIntegral ↑m

A lower bound for the genuine AP main mass at the strict prime endpoint. The endpoint is the greatest integer strictly below (1-epsilon)*N. No new prime number theorem or distribution premise is used.