theorem MathlibNt.SieveTheory.exists_actual_lowerRosser_jr_powerBudget : ∃ (A : ℝ), 0 < A ∧ ∀ (S : BoundingSieve) (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (D : ℕ) (z : ℝ), 2 ≤ D → 1 < z → (∀ p ∈ S.prodPrimes.primeFactors, ↑p < z) → have t := Real.log ↑D / Real.log z; 2 ≤ t → t ^ 13 ≤ Real.log ↑D → Real.exp 1 ≤ Real.log ↑D → AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S * (JurkatRichert1965ChenGammaOneQOne.jr1965f t - A * Real.exp √K * Real.log ↑D ^ (-(1 / 3))) ≤ BoundingSieve.mainSum (LinearSieve.lowerRosserWeight S.prodPrimes D)

A single positive constant works for every sieve, local-product constant, integer level and real cutoff. The coefficient is the original lower Rosser weight; neither a source contract nor a density estimate is a premise.