Suzuki's lower sieve factor on the first interval

This module passes the exact finite conservation identity to the genuine source series limit. For 2 ≤ s ≤ 4, the finite even partial sums converge to Suzuki's T⁻(s), while the finite amplitude and boundary residuals vanish. Consequently the explicit first-interval factor is exactly 1 - T⁻(s).

theorem MathlibNt.SieveTheory.one_sub_suzukiProposition118SourceTMinus_eq_lowerSieveFactorFirstInterval {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : 1 - suzukiProposition118SourceTMinus s = SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval s

On Suzuki's first lower interval, the genuine lower factor is exactly one minus the limiting even source series. The only premise is the production all-depth source contract; no factor identity or limiting conclusion is assumed.

theorem MathlibNt.SieveTheory.tendsto_suzukiFiniteLowerFactor_even_firstInterval {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : Filter.Tendsto (fun (m : ℕ) => suzukiFiniteLowerFactor (2 * m) s) Filter.atTop (nhds (SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval s))

The honest finite lower factors at even depths converge to the now-identified first-interval factor.

theorem MathlibNt.SieveTheory.suzukiEvenSourceLowerLayerSup_eq_ofReal_sourceTMinus {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs2 : 2 ≤ s) : suzukiEvenSourceLowerLayerSup s = ENNReal.ofReal (suzukiProposition118SourceTMinus s)

The unconditional ℝ≥0∞ supremum is the image of the genuine source T⁻ series once the production source contract supplies real summability.

theorem MathlibNt.SieveTheory.suzukiEvenSourceLowerLayerSup_eq_ofReal_one_sub_lowerSieveFactorFirstInterval {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : suzukiEvenSourceLowerLayerSup s = ENNReal.ofReal (1 - SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval s)

On the first interval, the same supremum is ofReal (1-F⁻(s)), linking the extended monotone limit directly to the explicit lower factor.