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

Actual S1 at the original alpha endpoint, with the standard BV error paid. The remaining main sum is the genuine lower Rosser density, not an assumed f-bound.