noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma11ShiftClamp (β : ℝ) (M : ℕ) (τ t : ℝ) : ℝ

Global clamp for the Proposition-9.3 source layer in Lemma 8.7.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma11ShiftClamp β M τ t = MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β M (max (τ - 1) (t - 1))

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma11ShiftClamp_eq_of_le (β : ℝ) (M : ℕ) {τ t : ℝ} (hτt : τ ≤ t) : sigma11ShiftClamp β M τ t = SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β M (t - 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma11_finiteSourceLayer_lemma8_7 {S : BoundingSieve} {D z v w s τ σ K β : ℝ} {N : ℕ} (hβ : 1 < β) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hτσ : τ ≤ σ) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / s)) (hv : v = D ^ (1 / τ)) (hw : w = D ^ (1 / σ)) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : (suzukiLemmaEightSevenPrimeSum S D w v z fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)) ≤ (1 / s * ∫ (t : ℝ) in τ..σ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)) + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (τ - 1) / Real.log w * (τ / s)

Direct source-layer instance of Lemma 8.7, kept in the same import cone as Claim 14.5 to avoid the legacy/production finite-layer declaration collision.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.suzukiLemmaEightSevenPrimeSum_mono_on_middle (S : BoundingSieve) (D w v z : ℝ) (F G : ℝ → ℝ) (hFG : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → F (Real.log D / Real.log ↑p) ≤ G (Real.log D / Real.log ↑p)) : suzukiLemmaEightSevenPrimeSum S D w v z F ≤ suzukiLemmaEightSevenPrimeSum S D w v z G

Monotonicity of the source-faithful Lemma-8.7 middle-range functional. Only values at the actual prime coordinates are required. The Euler suffix continues to use the third cutoff z; the prime carrier stops at v.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma11_middle_le_finiteSourceLayer_add_endpoint {S : BoundingSieve} {D z v w s τ σ K β : ℝ} {N : ℕ} (hβ : 1 < β) (hsdom : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hsτ : s ≤ τ) (hτσ : τ ≤ σ) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / s)) (hv : v = D ^ (1 / τ)) (hw : w = D ^ (1 / σ)) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : (suzukiLemmaEightSevenPrimeSum S D w v z fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (τ - 1) / Real.log w * (τ / s)

Source-correct Σ₁₁ middle-range assembly. Lemma 8.7 is used only on w ≤ p < v, with H(t)=T_{N-1}(t-1). Proposition 9.3 supplies all analytic conditions, while the source recursion bounds the truncated main integral by T_N(s). No equality is asserted: it generally fails when τ > s or when σ truncates the source support.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma12_middle_le_qD_lemma8_7 {S : BoundingSieve} {H : Section13HatLayers} {β D z v w s τ σ K d Δ : ℝ} (sign : ErrorSign) (R : ℝ → ℝ) (hmajorant : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → R (Real.log D / Real.log ↑p) ≤ qD H sign.opposite D d Δ (Real.log D / Real.log ↑p)) (hH : Section13HatContract H β) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / s)) (hv : v = D ^ (1 / τ)) (hw : w = D ^ (1 / σ)) (hτ : H.betaHat + sign.epsilon < τ) (hτσ : τ ≤ σ) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) (hii : Claim14_6_MonotoneQPremise H D d Δ σ) : suzukiLemmaEightSevenPrimeSum S D w v z R ≤ (1 / s * ∫ (t : ℝ) in τ..σ, qD H sign.opposite D d Δ t) + 6 * K ^ 2 * qD H sign.opposite D d Δ τ / Real.log w * (τ / s)

Source-correct Σ₁₂ middle-range assembly after the pointwise majorant (14.13). The prime carrier is exactly w ≤ p < v; z is deliberately kept as the independent original sieve cutoff controlling V(p)/V(z).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigma11_add_sigma12_middle_le {S : BoundingSieve} {H : Section13HatLayers} {β D z v w s τ σ K d Δ : ℝ} {N : ℕ} (sign : ErrorSign) (R : ℝ → ℝ) (hβ : 1 < β) (hsdom : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hsτ : s ≤ τ) (hmajorant : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → R (Real.log D / Real.log ↑p) ≤ qD H sign.opposite D d Δ (Real.log D / Real.log ↑p)) (hH : Section13HatContract H β) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / s)) (hv : v = D ^ (1 / τ)) (hw : w = D ^ (1 / σ)) (hτ : H.betaHat + sign.epsilon < τ) (hτσ : τ ≤ σ) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) (hii : Claim14_6_MonotoneQPremise H D d Δ σ) : (suzukiLemmaEightSevenPrimeSum S D w v z fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)) + suzukiLemmaEightSevenPrimeSum S D w v z R ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (τ - 1) / Real.log w * (τ / s) + ((1 / s * ∫ (t : ℝ) in τ..σ, qD H sign.opposite D d Δ t) + 6 * K ^ 2 * qD H sign.opposite D d Δ τ / Real.log w * (τ / s))

Combined source-correct middle-range estimate for Σ₁₁ + Σ₁₂. Both terms use the same exact carrier w ≤ p < v and the same independent Euler-ratio cutoff z.