theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_beta_fixed_normalized_lower (s δ : ℝ) (hs4 : 4 ≤ s) (hslt : s < 33 / 8) (hδ : 0 < δ) (ε : ℝ) : 0 < ε → ε < 1 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (33 / 2 * Real.exp (-Real.eulerMascheroniConstant) * (1 - ε) * SwitchingPrinciple.dimensionOneLowerLinearSieveFactor s - δ) * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 ≤ ↑(goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 33)))

Fixed-s normalized lower bound at the original beta cutoff. The lower-density factor is paid at fixed s, the actual main mass and actual sieve product are normalized on the true singular-series scale, and the paid Bombieri--Vinogradov remainder is absorbed into an arbitrary δ budget.