Suzuki Lemma 14.7 on the Jurkat--Richert interval

This module passes from the exact finite lower factor supplied by the literal all-depth theorem to Suzuki's canonical continuous factor. The comparison uses only nonnegativity and summability of the even source layers, so it is valid on the full legal range 2 ≤ s. On 4 ≤ s ≤ 6, the source normalization theorem then identifies that factor with the standard dimension-one Jurkat--Richert factor. The adaptive depth and the complete error term are unchanged.

theorem MathlibNt.SieveTheory.suzukiContinuousLowerFactor_le_adaptive_finiteLowerFactor {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {α : Type u_1} (carrier : Finset α) {s : ℝ} (hs : 2 ≤ s) : suzukiContinuousLowerFactor s ≤ suzukiFiniteLowerFactor (2 * (carrier.card + 1)) s

On the full legal source range, Suzuki's canonical continuous lower factor is bounded above by every carrier-adaptive finite lower factor.

theorem MathlibNt.SieveTheory.exists_lowerRosserDensity_continuousLowerFactor_of_suzuki_literal_allDepth_uniform_in_S_of_source (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 ∧ ∀ (S : BoundingSieve) (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 * (suzukiContinuousLowerFactor 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)

Uniform-in-sieve form of Lemma 14.7 with Suzuki's canonical continuous lower factor. In particular, all four constants are selected before S. The proof consumes the uniform literal all-depth Lemma 14.4 directly.

theorem MathlibNt.SieveTheory.exists_lowerRosserDensity_dimensionOneLowerFactor_of_suzuki_literal_allDepth_uniform_in_S_of_source (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 ∧ ∀ (S : BoundingSieve) (K : ℝ), 2 ≤ K → SwitchingPrinciple.HasDimensionOneLocalProductBound S K → ∀ (D : ℕ), 2 ≤ D → ∀ (s : ℝ), 4 ≤ s → s ≤ 6 → 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 * (SwitchingPrinciple.dimensionOneLowerLinearSieveFactor 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)

Uniform-in-sieve Suzuki Lemma 14.7 on 4 ≤ s ≤ 6, with the standard dimension-one Jurkat--Richert lower factor.

theorem MathlibNt.SieveTheory.exists_lowerRosserDensity_continuousLowerFactor_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 * (suzukiContinuousLowerFactor 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)

Lemma 14.7 with the canonical continuous lower factor on every legal source coordinate. Relative to the finite theorem, only the factor is strengthened; the quantifier order, adaptive depth, and error envelope are preserved exactly.

theorem MathlibNt.SieveTheory.exists_lowerRosserDensity_dimensionOneLowerFactor_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 : ℝ), 4 ≤ s → s ≤ 6 → 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 * (SwitchingPrinciple.dimensionOneLowerLinearSieveFactor 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)

Suzuki Lemma 14.7 on the Chen/Jurkat--Richert interval 4 ≤ s ≤ 6. The conclusion has the standard dimension-one lower factor, with precisely the same constants, adaptive depth, and error term as the all-depth finite theorem.