theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_antitone_cutoff (A : Finset ℕ) (N : ℕ) {x y : ℝ} (hxy : x ≤ y) : goldbachS1 A N y ≤ goldbachS1 A N x

Increasing the strict prime cutoff can only decrease the literal S1 count.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_beta_lower_paid (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∀ (s : ℝ), 4 ≤ s → s < 33 / 8 → ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * ∑ d ∈ (goldbachS1ProdPrimes N (S1BetaGeometryZeta N s)).divisors, LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N (S1BetaGeometryZeta N s)) (S1BetaGeometryD N s) d / ↑d.totient - C * ↑N / Real.log ↑N ^ U ≤ ↑(goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 33)))

The original beta endpoint is bounded below using the slightly larger real root cutoff. The BV constant is chosen before both s and epsilon.