noncomputable def MathlibNt.SieveTheory.suzukiFiniteLowerFactor (N : ℕ) (s : ℝ) : ℝ

The honest finite lower factor attached to an even Suzuki truncation. This is not the limiting Rosser--Iwaniec factor F⁻(s): identifying the two requires the even-depth limit in Suzuki (14.29).

Equations

• MathlibNt.SieveTheory.suzukiFiniteLowerFactor N s = 1 - MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s

theorem MathlibNt.SieveTheory.finiteSourceLayer_two_mul_eq_sum_evenLayers (m : ℕ) (s : ℝ) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * m) s = ∑ k ∈ Finset.range m, SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) s

At depth 2*m, the continuous source layer is exactly the first m even Suzuki layers. This is the finite normalization preceding the N → ∞, N ≡ 0 (mod 2) passage in Suzuki (14.29).

theorem MathlibNt.SieveTheory.suzukiFiniteLowerFactor_two_mul (m : ℕ) (s : ℝ) : suzukiFiniteLowerFactor (2 * m) s = 1 - ∑ k ∈ Finset.range m, SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) s

The finite lower factor is therefore one minus the exact finite sum of the first m even continuous layers.

theorem MathlibNt.SieveTheory.sourceDiscreteEuler_eq_suzukiVProduct_nat (S : BoundingSieve) (z : ℕ) : sourceDiscreteEuler S z = SwitchingPrinciple.suzukiVProduct S ↑z

On a natural cutoff, Suzuki's V(z) product is the discrete Euler product used by the exact lower-Rosser identity.

theorem MathlibNt.SieveTheory.exists_lowerRosserDensity_finiteLowerFactor_of_suzuki_literal_allDepth (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ), 0 < C1min ∧ ∀ (C1 : ℝ), C1min ≤ C1 → ∃ (C145 : ℝ) (Clow : ℝ) (C : ℝ), 0 < C145 ∧ 0 ≤ Clow ∧ 3 ≤ C ∧ ∀ (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (D : ℕ), 2 ≤ D → ∀ (s : ℝ), 2 ≤ s → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → have z := ⌈↑D ^ (1 / s)⌉₊; have N := 2 * ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1); SwitchingPrinciple.suzukiVProduct S ↑z * (suzukiFiniteLowerFactor N s - C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ)) ≤ LinearSieve.lowerRosserSetDensitySum (⇑S.nu) D (SwitchingPrinciple.suzukiSupportedBelow S z)

The already closed all-supported lower-Rosser identity and Lemma 14.4 give an actual finite lower factor, with no discrepancy. The adaptive depth is used only for the finite discrete support; the conclusion deliberately retains suzukiFiniteLowerFactor N s and does not identify it with the N → ∞ factor F⁻(s) from Lemma 14.7.