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 τ) : 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)

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.