theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1BoundingSieve_sieveProduct_eq (N : ℕ) (hEven : Even N) (ε z : ℝ) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS1BoundingSieve N hEven ε z) = MertensTheorem.goldbachSieveProduct N ⌈z⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_mainMass_mul_product_lower (ε η : ℝ) (hε : 0 < ε) (hεu : ε < 1) (hη : 0 < η) (hηu : η < 1 - ε) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (α : ℝ), 1 / 18 ≤ α → 2 * Real.exp (-Real.eulerMascheroniConstant) / α * (1 - ε - η) * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 ≤ (goldbachS1BoundingSieve N hEven ε (↑N ^ α)).totalMass * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS1BoundingSieve N hEven ε (↑N ^ α))

The actual S1 mass times its actual Euler product is bounded below on the true singular-series scale. This does not assert a lower Rosser density bound.