theorem MathlibNt.SieveTheory.suzukiActualT_odd_lowStrip_le_exp_sourceL (S : BoundingSieve) {N D z : ℕ} {K s : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 1 < D) (hs : 1 < s) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : suzukiActualT S N D z ≤ Real.exp (suzukiSourceL (↑z) K)

In the odd strip 1 < s < 2, Lemma 14.1 with lower tail index zero bounds the actual parity sum by the full exponential series.

theorem MathlibNt.SieveTheory.odd_lowStrip_half_le_errorEnvelope {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {N : ℕ} {D d s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (hN : Odd N) (hD : 1 < D) (hs1 : 1 < s) (hs2 : s ≤ 2) : 1 / 2 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s

The Section-13 initial profile gives a uniform positive odd error envelope throughout the whole low strip.

theorem MathlibNt.SieveTheory.one_le_lowStrip_localFactor_mul_claimV (S : BoundingSieve) {D : ℕ} {K : ℝ} (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hD : 2 ≤ D) : 1 ≤ Real.log ↑D / Real.log 2 * (1 + K / Real.log 2) * SwitchingPrinciple.SuzukiLemma144KappaOne.claim14_5VProduct S ↑D

The local Euler-product contract at the fixed lower endpoint 2.

theorem MathlibNt.SieveTheory.claim145_odd_lowStrip_pointwise_of_scalar (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N D : ℕ} {d Δ K s A : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (hN : Odd N) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hA : 0 ≤ A) (hD : 2 ≤ D) (hs1 : 1 < s) (hs2 : s ≤ 2) (hscalar : 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 ^ Δ ≤ A * Real.exp √K) : ActualClaim145BoundAt S H N D d Δ K s A

Pointwise Claim 14.5 on 1 < s ≤ 2, reduced only to the uniform scalar domination above. In particular no finite scan, Claim 14.5 hypothesis, or desired pointwise conclusion is used.

theorem MathlibNt.SieveTheory.claim145_odd_lowStrip_smallLog_actual (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ C1 Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC1 : 0 ≤ C1) (hΘ : 0 < Θ) (hd : 0 < d) (hsource : 2 / d < 1 / Θ) (hΔ0 : 0 ≤ Δ) (hΔ1 : Δ ≤ 1) : ∃ (C145 : ℝ), 0 ≤ C145 ∧ ∀ (K : ℝ) (N D : ℕ) (s : ℝ), 2 ≤ K → Odd N → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → 2 ≤ D → 1 < s → s ≤ 2 → Real.log ↑D ≤ C1 * K ^ Θ → ActualClaim145BoundAt S H N D d Δ K s C145

Production-facing completion of Suzuki's omitted source-small odd strip. The chosen coefficient precedes K,N,D,s literally, and the conclusion now covers every K ≥ 2.