theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma8_7_qD_of_claim14_6_i_ii_direct_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 τ)
:
The finite (14.18) assembly with Claim 14.6(iii) supplied only at the
actual Case-I lower endpoint τ. This is the pointwise interface needed to
combine the independently eventual forms of Claims 14.6(i)--(iii).
theorem
MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lemma8_7_caseI_contraction_for_sufficiently_large_D
{S : BoundingSieve}
{H : Section13HatLayers}
{β s τ σ K d Δ : ℝ}
{N : ℕ}
(hH : Section13HatContract H β)
(hd : 0 ≤ d)
(hΔlower : -1 < Δ)
(hΔupper : Δ < 1)
(hσ : ∀ (sign : ErrorSign), β + sign.epsilon ≤ σ)
(hcaseI : Claim14_5CaseI β N s σ)
(hτ : H.betaHat + (ErrorSign.ofDepth N).epsilon < τ)
(hsτ : s ≤ τ)
(hτσ : τ ≤ σ)
(hK : 2 ≤ K)
(hlocal : HasDimensionOneLocalProductBound S K)
:
∃ (D₀ : ℝ),
1 < D₀ ∧ ∀ (D z v w : ℝ),
D₀ ≤ D →
2 ≤ z →
2 ≤ v →
2 ≤ w →
w ≤ v →
v ≤ z →
z = D ^ (1 / s) →
v = D ^ (1 / τ) →
w = D ^ (1 / σ) →
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)
Eventual Case-I form of (14.18), with no Claim 14.6 premise. All sieve geometry and the dimension-one local Euler-product hypothesis remain explicit at the final call site.