theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.suzukiVProduct_div_eq_suffix (S : BoundingSieve) {p : ℕ} {z : ℝ} (hpz : ↑p < z) : suzukiVProduct S ↑p / suzukiVProduct S z = ∏ q ∈ S.prodPrimes.primeFactors with p ≤ q ∧ ↑q < z, (1 - S.nu q)⁻¹

The concrete Euler-product quotient occurring in sigmaTwelve is exactly its Lemma-8.7 suffix product.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.naturalCeil_inherited_error_le_claim14_13 (H : Section13HatLayers) {N D p : ℕ} {d Δ : ℝ} (hp : 2 ≤ p) (hDp : 2 * p ≤ D) (hΔ : 0 ≤ Δ) (hT : 0 ≤ H.T (ErrorSign.ofDepth (N - 1)) (SuzukiLemma144Equation1410.inheritedCoordinate D p)) (h1413 : Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) : errorEnvelope H (N - 1) (↑(D ⌈/⌉ p)) d (SuzukiLemma144Equation1410.inheritedCoordinate D p) * Real.log ↑(D ⌈/⌉ p) ^ (-Δ) ≤ Real.log ↑D ^ (-Δ) * qD H (ErrorSign.ofDepth N).opposite (↑D) d Δ (Real.log ↑D / Real.log ↑p)

Source-coordinate version of the natural-ceiling error estimate. Unlike naturalCeil_error_le_claim14_13, this is the form needed by the literal equation14_10.sigmaTwelve, whose envelope is evaluated at the inherited coordinate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sigmaTwelve_suzukiVProduct_le_qD_lemma8_7 {S : BoundingSieve} {H : Section13HatLayers} {β C K d Δ w v s τ σ : ℝ} {N D znat : ℕ} (hH : Section13HatContract H β) (hD : 1 < ↑D) (hz2 : 2 ≤ ↑znat) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ ↑znat) (hz : ↑znat = ↑D ^ (1 / s)) (hv : v = ↑D ^ (1 / τ)) (hw : w = ↑D ^ (1 / σ)) (hτ : H.betaHat + (ErrorSign.ofDepth N).epsilon < τ) (hτσ : τ ≤ σ) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) (hii : Claim14_6_MonotoneQPremise H (↑D) d Δ σ) (hC : 0 ≤ C) (hΔ : 0 ≤ Δ) (hCeil : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → 2 ≤ p ∧ 2 * p ≤ D) (hT : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → 0 ≤ H.T (ErrorSign.ofDepth (N - 1)) (SuzukiLemma144Equation1410.inheritedCoordinate D p)) (h1413 : ∀ p ∈ S.prodPrimes.primeFactors, w ≤ ↑p → ↑p < v → Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p) (↑D / ↑p)) : SuzukiLemma144Equation1410.sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu) (fun (p : ℕ) => suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => errorEnvelope H n (↑D') d x) (suzukiVProduct S ↑znat) C K Δ N D σ τ ≤ C * Real.exp √K * suzukiVProduct S ↑znat * (Real.log ↑D ^ (-Δ) * ((1 / s * ∫ (t : ℝ) in τ..σ, qD H (ErrorSign.ofDepth N).opposite (↑D) d Δ t) + 6 * K ^ 2 * qD H (ErrorSign.ofDepth N).opposite (↑D) d Δ τ / Real.log w * (τ / s)))

Global scaling closure of the concrete sigmaTwelve from (14.10), followed by the exact integral-plus-endpoint conclusion of qD Lemma 8.7.