Source-faithful statement of Claim 14.5 (κ = 1)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct (S : BoundingSieve) (x : ℝ) : ℝ

The finite Euler product V(x) on the production support, repeated here because the older base-case temporary module cannot be jointly imported with the current Lemma-8.7 umbrella without a declaration collision.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S x = ∏ p ∈ S.prodPrimes.primeFactors with ↑p < x, (1 - S.nu p)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale (S : BoundingSieve) (H : Section13HatLayers) (N : ℕ) (D d Δ σ K s : ℝ) : ℝ

The explicit quantity on the right of Claim 14.5 after replacing the source ≪ by a named multiplicative constant. At κ=1 this uses the literal E_N, represented by errorEnvelope, and the finite Euler product V(D). The source has exp (sqrt K)/(σ log D) and a further (log D)^(-Δ).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N D d Δ σ K s = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S D * (Real.exp √K / (Real.log D * σ)) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s * Real.log D ^ (-Δ)

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Bound (Tdisc : ℕ → ℝ → ℝ → ℝ) (S : BoundingSieve) (H : Section13HatLayers) (N : ℕ) (D z d Δ σ K s C145 : ℝ) : Prop

Exact non-asymptotic interface for Claim 14.5. Tdisc N D z is the (real-parameter) discrete parity sum from the paper; no such object currently exists in the production API, whose source-faithful discrete model has natural cutoffs. C145 records precisely the implicit absolute constant in ≪.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Bound Tdisc S H N D z d Δ σ K s C145 = (Tdisc N D z ≤ C145 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5Scale S H N D d Δ σ K s)

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime (β D σ C1 K ΘK s : ℝ) : Prop

The exact range in which Suzuki invokes Claim 14.5.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime β D σ C1 K ΘK s = (β ≤ s ∧ (Real.log D ≤ C1 * K ^ ΘK ∨ σ ≤ s))

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseI (β : ℝ) (N : ℕ) (s σ : ℝ) : Prop

Case I in the source, specialized to κ=1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseI β N s σ = (β + ↑(N % 2) ≤ s ∧ s ≤ σ)

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseII (β : ℝ) (N : ℕ) (s : ℝ) : Prop

Case II in the source. It exists only at odd depth.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseII β N s = (Odd N ∧ β - 1 < s ∧ s ≤ β + 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5_exact_case_split {β D σ C1 K ΘK s : ℝ} {N : ℕ} (hdom : s ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne β N) (hsσ : s ≤ σ) (_hlarge : C1 * K ^ ΘK < Real.log D) : Claim14_5CaseI β N s σ ∨ Claim14_5CaseII β N s

After Claim 14.5 removes small D and large s, Suzuki's parity domain splits exactly into Case I and Case II. In particular, Case II is not an optional analytic branch: it is forced by the open odd parity interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5_regime_or_caseI_or_caseII {β D σ C1 K ΘK s : ℝ} {N : ℕ} (hdom : s ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne β N) (hsσor : s ≤ σ ∨ σ ≤ s) : Claim14_5Regime β D σ C1 K ΘK s ∨ Claim14_5CaseI β N s σ ∨ Claim14_5CaseII β N s

Full range partition used before the induction step: either Claim 14.5 already applies, or one is in exactly Case I/II.

Lemma 8.7 connected to Claim 14.6

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qDClamp (H : Section13HatLayers) (sign : ErrorSign) (D d Δ τ t : ℝ) : ℝ

Global continuous clamp of q_D; it agrees with q_D on [τ,∞) and allows direct use of the global-continuity interface of Lemma 8.7.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qDClamp H sign D d Δ τ t = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign D d Δ (max τ t)

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qDClamp_eq_of_le (H : Section13HatLayers) (sign : ErrorSign) (D d Δ : ℝ) {τ t : ℝ} (hτt : τ ≤ t) : qDClamp H sign D d Δ τ t = qD H sign D d Δ t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qDClamp_conditions_of_claim14_6_ii {H : Section13HatLayers} {β D d Δ τ σ : ℝ} (hH : Section13HatContract H β) (sign : ErrorSign) (hD : 1 < D) (hτ : H.betaHat + sign.epsilon < τ) (_hτσ : τ ≤ σ) (hii : Claim14_6_MonotoneQPremise H D d Δ σ) : Continuous (qDClamp H sign.opposite D d Δ τ) ∧ (∀ t ∈ Set.Icc τ σ, 0 ≤ qDClamp H sign.opposite D d Δ τ t) ∧ AntitoneOn (fun (t : ℝ) => qDClamp H sign.opposite D d Δ τ t * t) (Set.Icc τ σ)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma8_7_qD_of_claim14_6_ii {S : BoundingSieve} {H : Section13HatLayers} {β D z v w s τ σ K d Δ : ℝ} (sign : ErrorSign) (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 (qD H sign.opposite D d Δ) ≤ (1 / s * ∫ (t : ℝ) in τ..σ, qD H sign.opposite D d Δ t) + 6 * K ^ 2 * qD H sign.opposite D d Δ τ / Real.log w * (τ / s)

Lemma 8.7 applied to the exact q_D^∓ of (14.13), with Claim 14.6(ii) discharging its weighted-antitonicity hypothesis.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.one_div_mul_lambda_eq_errorEnvelope (H : Section13HatLayers) {N : ℕ} {D d s : ℝ} (hs : 0 < s) : 1 / s * lambda H (ErrorSign.ofDepth N) D d 0 s = errorEnvelope H N D d s

At κ=1, the normalized endpoint s⁻¹ Λ₀ is literally the current source-correct error envelope E_N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma8_7_qD_of_claim14_6_i_ii_iii {S : BoundingSieve} {H : Section13HatLayers} {β D z v w s τ σ K d Δ : ℝ} {N : ℕ} (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 + (ErrorSign.ofDepth N).epsilon < τ) (hβs : H.betaHat + (ErrorSign.ofDepth N).epsilon ≤ s) (hsτ : s ≤ τ) (hτσ : τ ≤ σ) (hs : 0 < s) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) (hi : Claim14_6_MonotoneLambdaPremise H D d σ) (hii : Claim14_6_MonotoneQPremise H D d Δ σ) (hiiiτ : ∫ (t : ℝ) in τ..σ, qD H (ErrorSign.ofDepth N).opposite D d Δ t < (1 - 1 / σ) ^ (1 - Δ) * lambda H (ErrorSign.ofDepth N) D d 0 τ) : suzukiLemmaEightSevenPrimeSum S D w v z (qD H (ErrorSign.ofDepth N).opposite D d Δ) < (1 - 1 / σ) ^ (1 - Δ) * errorEnvelope H N D d s + 6 * K ^ 2 * qD H (ErrorSign.ofDepth N).opposite D d Δ τ / Real.log w * (τ / s)

Finite algebraic assembly of (14.18): Lemma 8.7 plus Claim 14.6(i)--(iii) gives the strict contraction main term (1-1/σ)^(1-Δ) E_N; only the explicit Lemma-8.7 endpoint error remains. No final Claim 14.5 or Lemma 14.4 assumption is used.