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

Equation (14.11), with the finite Euler quotient expanded into the exact Lemma-8.7 suffix. The upper prime carrier is v; z remains the independent Euler-product cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigmaEleven_eq_lemmaEightSevenPrimeSum_natCeil (S : BoundingSieve) (β σ τ w v r : ℝ) (N D z : ℕ) (hw : w = ↑D ^ (1 / σ)) (hv : v = ↑D ^ (1 / τ)) (hvr : v ≤ r) (hz : z = ⌈r⌉₊) : SuzukiLemma144Equation1410.sigmaEleven (suzukiSupportedBelow S z) (⇑S.nu) (fun (p : ℕ) => suzukiVProduct S ↑p) (suzukiVProduct S ↑z) β N D σ τ = suzukiVProduct S ↑z * suzukiLemmaEightSevenPrimeSum S (↑D) w v r fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)

Strict finite carriers, Euler products, and Lemma-8.7 suffixes are unchanged when the real cutoff is replaced by its natural ceiling.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.caseI_sigmaEleven_le_finiteSourceLayer_add_endpoint {S : BoundingSieve} {β s τ σ K : ℝ} {N D z : ℕ} (hβ : 1 < β) (hsdom : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hsτ : s ≤ τ) (hτσ : τ ≤ σ) (hD : 1 < ↑D) (hroot2 : 2 ≤ ↑D ^ (1 / s)) (hv2 : 2 ≤ ↑D ^ (1 / τ)) (hw2 : 2 ≤ ↑D ^ (1 / σ)) (hwv : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / τ)) (hvroot : ↑D ^ (1 / τ) ≤ ↑D ^ (1 / s)) (hz : z = ⌈↑D ^ (1 / s)⌉₊) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : SuzukiLemma144Equation1410.sigmaEleven (suzukiSupportedBelow S z) (⇑S.nu) (fun (p : ℕ) => suzukiVProduct S ↑p) (suzukiVProduct S ↑z) β N D σ τ ≤ suzukiVProduct S ↑z * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + suzukiVProduct S ↑z * (6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (τ - 1) / Real.log (↑D ^ (1 / σ)) * (τ / s))

Internalized Case-I hSigma11. Lemma 8.7 gives the main integral plus its (14.12) endpoint remainder; the finite (9.2) recurrence bounds that integral by T_N(s). Thus neither a mainSum/finite-layer identification nor a packaged middle-endpoint estimate is a premise.