Suzuki Lemma 14.7: continuous lower factor on the first interval

This module upgrades the finite-factor lower Rosser density estimate to the actual first-interval continuous factor. It uses only the one-sided fact that the carrier-adaptive finite even source sum is bounded by the full summable source series. In particular, it makes no claim that an adaptive finite depth is itself a limit.

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

Every carrier-adaptive finite even source layer is bounded by the genuine summable lower source series T⁻(s).

theorem MathlibNt.SieveTheory.suzukiLowerSieveFactorFirstInterval_le_adaptive_finiteLowerFactor {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {α : Type u_1} (carrier : Finset α) {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval s ≤ suzukiFiniteLowerFactor (2 * (carrier.card + 1)) s

On 2 ≤ s ≤ 4, the actual first-interval continuous lower factor is no larger than every carrier-adaptive finite lower factor.

theorem MathlibNt.SieveTheory.exists_lowerRosserDensity_continuousLowerFactorFirstInterval_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 ≤ 4 → 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 * (SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval 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 on its first lower interval, in the production lower-Rosser quantifier order. Relative to the finite theorem, only the factor is replaced: suzukiFiniteLowerFactor N s becomes the genuine explicit continuous factor suzukiLowerSieveFactorFirstInterval s; the error term and adaptive depth N are unchanged.