theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachDifferenceCarrier_bounds {N n : ℕ} {ε : ℝ} (hlarge : 1 < ε * ↑N) (hn : n ∈ goldbachDifferenceCarrier N ε) : 2 ≤ n ∧ n < N

Every actual difference is at least two and strictly below N once the uniform epsilon growth condition holds. No coprimality is assumed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_two_basic_sieve_eventually (ε : ℝ) (hε : 0 < ε) (hεupper : ε < 2 / 15) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (κ σ : ℝ), 1 / 21 < κ → κ < σ → σ ≤ 1 / 3 → goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ κ) + goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ σ) - 2 * goldbachS2 (goldbachDifferenceCarrier N ε) N (↑N ^ (9 / 19 - ε)) - goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ κ) - goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ σ) - 2 * goldbachBadCount (goldbachDifferenceCarrier N ε) N ≤ 2 * ↑(D19 N)

Li--Liu's two actual basic inequalities, before the subsequent Buchstab expansions. The one threshold precedes N, kappa and sigma; the bad count is retained, not assumed negligible. This does not assert positivity of D19.