theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_beta_lowerDensity (s ρ : ℝ) (hs4 : 4 ≤ s) (hslt : s < 33 / 8) (hρ : 0 < ρ) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (ε : ℝ), 0 < ε → ε < 1 → have S := goldbachS1BoundingSieve N hEven ε (S1BetaGeometryZeta N s); (SwitchingPrinciple.dimensionOneLowerLinearSieveFactor s - ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S ≤ BoundingSieve.mainSum (LinearSieve.lowerRosserWeight (goldbachS1ProdPrimes N (S1BetaGeometryZeta N s)) (S1BetaGeometryD N s))

Fixed-s lower-density producer for the genuine beta = 4 / 33 root cutoff ζ(N,s) = D(N,s)^(1/s) with D(N,s) = ceil(N^((4/33)s)). The source-relative Suzuki theorem provides the lower factor, the exact bridge identifies the finite Suzuki objects with the honest BoundingSieve main sum and sieve product, and the adaptive-depth error is absorbed uniformly at this fixed s.