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

Uniformity in the exponent in MainScale allows a genuine moving root cutoff. The loss from the effective exponent is paid before selecting the N threshold.