Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLemma144CaseIIBaseOneSameC

At depth one the finite continuous source layer is the literal initial function (3-s)/s throughout the low strip.

The Section 13 plus-hat initial condition at β=2, written in the normalization occurring in the depth-one error envelope.

On the low strip the exact hat initial value gives the uniform lower bound 1/s for the depth-one production error envelope.

theorem MathlibNt.SieveTheory.exists_baseOne_localError_sameC_threshold {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : } (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 < C) (hK : 2 K) :
∃ (D₀ : ), 1 < D₀ ∀ (D : ), D₀ D∀ (s : ), 1 < ss 39 * K / (s * Real.log D) C * Real.exp K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H 1 D d s * Real.log D ^ (-Δ)

A completely explicit eventual comparison of the local depth-one remainder with the same fixed C error budget. The threshold is chosen before s, so this is uniform on 1 < s ≤ 3.

The Euler product multiplying both base-one brackets is nonnegative.

theorem MathlibNt.SieveTheory.two_le_rpow_inv_lowStrip {D s : } (hD : 0 < D) (hlog3 : 3 Real.log D) (hs : 1 < s) (hs3 : s 3) :
2 D ^ (1 / s)

log D ≥ 3 is a uniform root threshold for every 1 < s ≤ 3.

theorem MathlibNt.SieveTheory.lemma14_4_caseII_base_one_sameC_uniform {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) {d Δ C K : } (hd : 0 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 < C) (hK : 2 K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) :
∃ (D₀ : ), 1 < D₀ ∀ (D : ), D₀ D3 SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ∀ (s : ), 1 < ss 3Lemma144CaseIISameCAt S H 1 D d Δ C K s

Actual Case-II N=1 closure with one fixed C. A single threshold is chosen before the low-strip parameter s; it simultaneously enforces the source value 3 ≤ sourceSigma D d, the natural-ceiling base geometry, and the uniform absorption of 9K/(s log D).

The exact producer requested by the Case-II dispatcher, now discharged from source data. It is a specialization of the stronger threshold-before-s uniform theorem above and therefore uses the identical constant C.