theorem MathlibNt.SieveTheory.claim145_sourceSigma_scalar_eventually (S : BoundingSieve) {d Δ K C C145 : ℝ} (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, Real.exp 1 * suzukiSourceL D K ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d - 2 ∧ Real.exp (suzukiSourceL D K + (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d - 2) * (1 + Real.log (suzukiSourceL D K) - Real.log (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d - 2))) ≤ C145 * (SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.exp √K / (Real.log D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) * ((1 + SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ^ d / Real.log D) ^ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d * SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiLowerProfile C (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)) * Real.log D ^ (-Δ))

At Suzuki's exact moving endpoint, both analytic premises required by the internal Claim-14.5 comparison hold eventually.