theorem MathlibNt.SieveTheory.claim145_sourceSigma_allS_scalar_eventually (S : BoundingSieve) {d Δ K C C145 M : ℝ} (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 < K) (hC145 : 0 < C145) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) : ∀ᶠ (D : ℝ) in Filter.atTop, ∀ (s : ℝ), SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ≤ s → 0 < SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ M ≤ s ∧ Real.exp 1 * suzukiSourceL D K ≤ s - 2 ∧ Real.exp (suzukiSourceL D K + (s - 2) * (1 + Real.log (suzukiSourceL D K) - Real.log (s - 2))) ≤ C145 * (SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.exp √K / (Real.log D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) * ((1 + s ^ d / Real.log D) ^ s * s * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C s) * Real.log D ^ (-Δ))

Suzuki p.83, Case B, uniformly at every coordinate above the moving sourceSigma endpoint. The proof keeps s free: the logarithmic loss is transported with u = s / sourceSigma, while the s^d / log D gain supplies d * log u.