def MathlibNt.SieveTheory.Claim145OddLowStripSmallLogScalarUniform (d Δ C1 Θ : ℝ) : Prop

The uniform scalar obligation in the source-small odd strip omitted by Suzuki's printed Case partition. The multiplicative constant is chosen after C1 and the source parameters, but before K and D; unlike the intermediate eventual estimate, this statement covers every K ≥ 2.

Equations

• MathlibNt.SieveTheory.Claim145OddLowStripSmallLogScalarUniform d Δ C1 Θ = ∃ (A : ℝ), 0 ≤ A ∧ ∀ (K : ℝ) (D : ℕ), 2 ≤ K → 2 ≤ D → Real.log ↑D ≤ C1 * K ^ Θ → have R := Real.log ↑D / Real.log 2 * (1 + K / Real.log 2); 2 * R ^ 2 * Real.log ↑D * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d * Real.log ↑D ^ Δ ≤ A * Real.exp √K

theorem MathlibNt.SieveTheory.claim145_odd_lowStrip_smallLog_scalarUniform_one {d Δ C1 Θ : ℝ} (hC1 : 0 ≤ C1) (hΘ : 0 < Θ) (hd : 0 < d) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) : ∃ (K0 : ℝ), 2 ≤ K0 ∧ ∀ (K : ℝ) (D : ℕ), K0 ≤ K → 2 ≤ D → Real.log ↑D ≤ C1 * K ^ Θ → have R := Real.log ↑D / Real.log 2 * (1 + K / Real.log 2); 2 * R ^ 2 * Real.log ↑D * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d * Real.log ↑D ^ Δ ≤ Real.exp √K

Uniform closure of the pure scalar obligation. In fact the source hypotheses permit the multiplicative constant A = 1; no finite range in D is scanned.

theorem MathlibNt.SieveTheory.claim145_odd_lowStrip_smallLog_scalarUniform {d Δ C1 Θ : ℝ} (hC1 : 0 ≤ C1) (hΘ : 0 < Θ) (hd : 0 < d) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) : Claim145OddLowStripSmallLogScalarUniform d Δ C1 Θ

All-K scalar closure. Above the eventual threshold the coefficient-one estimate applies. Below it, monotonicity in K moves the left side to the threshold, while the explicit coefficient exp (sqrt K0) absorbs that single analytic endpoint. Thus no finite scan of the bounded interval is used.