theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaEleven_eq_suzukiLemmaEightSevenPrimeSum (S : BoundingSieve) (β σ τ w v : ℝ) (N D znat : ℕ) (hw : w = ↑D ^ (1 / σ)) (hv : v = ↑D ^ (1 / τ)) (hvz : v ≤ ↑znat) : sigmaEleven (suzukiSupportedBelow S znat) (⇑S.nu) (fun (p : ℕ) => suzukiVProduct S ↑p) (suzukiVProduct S ↑znat) β N D σ τ = suzukiVProduct S ↑znat * suzukiLemmaEightSevenPrimeSum S (↑D) w v ↑znat fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)

Exact identification of the main term Σ₁₁ from equation (14.10) with Suzuki's genuine Lemma-8.7 middle-range prime sum.

The finite carrier is the supported set below the natural cutoff znat. The hypothesis v ≤ znat makes this support restriction redundant on the middle range w ≤ p < v. Termwise, positivity of V(znat) allows the normalization V(p) / V(znat) to be identified with the exact Euler suffix over p ≤ q < znat; no abstract ratio hypothesis is used.