Finite conservation behind Suzuki's first lower interval

This module freezes the normalization in Suzuki Proposition 9.3(iv)--(v) before any passage to the parity-layer limit. At κ = 1, β = 2, the finite constants are

• A_m = 3 (1 + T_{2m-1}(3)), and
• B_m = 2 (1 - T_{2m}(2)).

The main theorem proves the exact finite identity

1 - T_{2m}(s) = B_m / s + A_m / s * ∫₂ˢ dt/(t-1)

for m ≥ 1 and 2 ≤ s ≤ 4. Its final corollary isolates, without a conclusion-shaped hypothesis, the two genuine tails still needed to identify the explicit first-interval factor with 1 minus the even continuous-layer limit.

noncomputable def MathlibNt.SieveTheory.suzukiOddSourceUpperPartialSum (m : ℕ) (s : ℝ) : ℝ

Suzuki's odd finite partial sum T_{2m-1}.

Equations

• MathlibNt.SieveTheory.suzukiOddSourceUpperPartialSum m s = ∑ k ∈ Finset.range m, MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) s

noncomputable def MathlibNt.SieveTheory.suzukiFiniteLowerAmplitude (m : ℕ) : ℝ

The finite constant A_{2m-1} in Proposition 9.3(iv).

Equations

• MathlibNt.SieveTheory.suzukiFiniteLowerAmplitude m = 3 * (1 + MathlibNt.SieveTheory.suzukiOddSourceUpperPartialSum m 3)

noncomputable def MathlibNt.SieveTheory.suzukiFiniteLowerBoundary (m : ℕ) : ℝ

The finite constant B_{2m} in Proposition 9.3(v).

Equations

• MathlibNt.SieveTheory.suzukiFiniteLowerBoundary m = 2 * (1 - MathlibNt.SieveTheory.suzukiEvenSourceLowerPartialSum m 2)

theorem MathlibNt.SieveTheory.mul_suzukiLayer_one_two_odd_eq_three_mul_at_three {n : ℕ} (hn : n % 2 = 1) (hn3 : 3 ≤ n) {u : ℝ} (hu1 : 1 ≤ u) (hu3 : u ≤ 3) : u * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 n u = 3 * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 n 3

For every odd source layer beyond the base layer, its weighted value is constant on Suzuki's first upper strip 1 < u ≤ 3.

theorem MathlibNt.SieveTheory.mul_suzukiOddSourceUpperPartialSum_eq_finiteAmplitude_sub {m : ℕ} (hm : 1 ≤ m) {u : ℝ} (hu1 : 1 ≤ u) (hu3 : u ≤ 3) : u * suzukiOddSourceUpperPartialSum m u = suzukiFiniteLowerAmplitude m - u

Finite Proposition 9.3(iv), specialized to κ = 1, β = 2 and the odd partial sum ending at 2m-1.

theorem MathlibNt.SieveTheory.suzukiOddSourceUpperPartialSum_sub_one {m : ℕ} (hm : 1 ≤ m) {t : ℝ} (ht2 : 2 ≤ t) (ht4 : t ≤ 4) : suzukiOddSourceUpperPartialSum m (t - 1) = suzukiFiniteLowerAmplitude m / (t - 1) - 1

On 2 ≤ t ≤ 4, the preceding odd partial sum has the exact integrand A_m/(t-1)-1 used in Proposition 9.3(v).

theorem MathlibNt.SieveTheory.mul_suzukiLayer_one_two_even_eq_integral (k : ℕ) {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : s * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) s = ∫ (t : ℝ) in s..2 + ↑(2 * (k + 1)), SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) (t - 1)

Each even layer is obtained by integrating its preceding odd layer from the current point to its closed support endpoint.

theorem MathlibNt.SieveTheory.mul_suzukiLayer_one_two_even_eq_at_two_sub_integral (k : ℕ) {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : s * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) s = 2 * SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) 2 - ∫ (t : ℝ) in 2..s, SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) (t - 1)

Moving the lower endpoint from 2 to s gives one exact finite conservation step.

theorem MathlibNt.SieveTheory.suzuki_even_partial_finite_conservation {m : ℕ} (hm : 1 ≤ m) {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : s * suzukiEvenSourceLowerPartialSum m s = -suzukiFiniteLowerBoundary m + s - suzukiFiniteLowerAmplitude m * ∫ (t : ℝ) in 2..s, (t - 1)⁻¹

Exact finite form of Suzuki Proposition 9.3(v) on the first lower interval.

theorem MathlibNt.SieveTheory.one_sub_evenPartialSum_eq_firstInterval_add_residuals {m : ℕ} (hm : 1 ≤ m) {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : 1 - suzukiEvenSourceLowerPartialSum m s = SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval s + suzukiFiniteLowerBoundary m / s + (suzukiFiniteLowerAmplitude m - SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude) / s * ∫ (t : ℝ) in 2..s, (t - 1)⁻¹

The finite lower factor is exactly the source first-interval expression plus its two honest truncation residuals. No convergence premise is hidden here.