Natural-ceiling closure of the Σ₁₂ input. The finite sum itself, a Claim-14.6 conclusion, and mainSum are never assumed.

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

Natural-ceiling version of the global Σ₁₂ estimate. The strict carrier below D^(1/s) is transported exactly through z = ⌈D^(1/s)⌉₊; no equality between the real cast of z and the power cutoff is used.

noncomputable def MathlibNt.SieveTheory.sigma12ContractionMultiplier (σ Δ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.sigma12ContractionMultiplier σ Δ = (1 - 1 / σ) ^ (1 - Δ)

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

Equations

• MathlibNt.SieveTheory.sigma12InheritedBudget S H N D z C K d Δ s = C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * Real.log ↑D ^ (-Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s

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

Equations

• MathlibNt.SieveTheory.sigma12EndpointRemainder S H N D z C K d Δ s σ = C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * Real.log ↑D ^ (-Δ) * (6 * K ^ 2 * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ s / Real.log (↑D ^ (1 / σ)) * (s / s))

theorem MathlibNt.SieveTheory.exists_sigma12_sameC_strictFactor {σ Δ : ℝ} (hσ : 1 < σ) (hΔ : Δ < 1) : ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier σ Δ) / 2 ∧ sigma12ContractionMultiplier σ Δ < q.ρ

The source contraction has a canonical strict midpoint enlargement.

theorem MathlibNt.SieveTheory.eventually_sigmaTwelve_internal_contraction_sameC {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {C K d Δ s : ℝ} {N : ℕ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hN : 2 ≤ N) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hs0 : 0 < s) (hsLower : 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon ≤ s) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hC : 0 ≤ C) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D z : ℕ), D₀ ≤ ↑D → 1 < SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 1 < ↑D → 2 ≤ ↑D ^ (1 / s) → 2 ≤ ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) → ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑D ^ (1 / s) → z = ⌈↑D ^ (1 / s)⌉₊ → H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon < s → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 2 ≤ p ∧ 2 * p ≤ D) → (∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p)) → ∃ (q : Lemma144StrictFactor), q.ρ = (1 + sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) Δ) / 2 ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) (SwitchingPrinciple.suzukiVProduct S ↑z) C K Δ N D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) s ≤ sigma12ContractionMultiplier (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) Δ * sigma12InheritedBudget S H N D z C K d Δ s + sigma12EndpointRemainder S H N D z C K d Δ s (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaTwelve S.prodPrimes.primeFactors (⇑S.nu) (fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p) (fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) (SwitchingPrinciple.suzukiVProduct S ↑z) C K Δ N D (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) s ≤ q.ρ * sigma12InheritedBudget S H N D z C K d Δ s + sigma12EndpointRemainder S H N D z C K d Δ s (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

For all sufficiently large natural D, the raw moving Claim-14.6 sources, the natural-ceiling Σ₁₂ bridge, and Lemma 8.7 give a strict same-constant contraction.