Source factor for the dimension-one upper Rosser density

This module closes the source-normalization side of the upper Rosser density producer on Chen's varying-q window. It deliberately does not postulate a Rosser-density inequality. The only residual source input below is the literal first-interval identity for Suzuki's already-defined odd layer series. Above 3, the identity is derived from the parity integral DDE; the amplitude remains separate and is then replaced by its independently produced value 2 exp γ.

def MathlibNt.SieveTheory.SuzukiContinuousUpperFactorFirstIntervalIdentity : Prop

The literal first-interval statement for Suzuki's upper parity source. This is a source-series identification, not an upper-density conclusion.

Equations

• MathlibNt.SieveTheory.SuzukiContinuousUpperFactorFirstIntervalIdentity = ∀ (s : ℝ), 3 / 2 ≤ s → s ≤ 3 → MathlibNt.SieveTheory.suzukiContinuousUpperFactor s = MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude / s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiContinuousUpperFactorFirstIntervalIdentity_of_sourceContract (H : SuzukiLemma144KappaOne.Section13HatLayers) (hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) : SuzukiContinuousUpperFactorFirstIntervalIdentity

The first upper source interval follows from the genuine source-series finite-prefix identity and its proved summable limit.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiContinuousUpperFactor_eq_jurkatRichertUpperLinearSieveFactor (H : SuzukiLemma144KappaOne.Section13HatLayers) (hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) (hA : SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude = 2 * Real.exp Real.eulerMascheroniConstant) {s : ℝ} (hslo : 3 / 2 ≤ s) (hshi : s ≤ 4) : suzukiContinuousUpperFactor s = jurkatRichertUpperLinearSieveFactor s

On the complete varying-q window, Suzuki's genuine upper source factor is exactly the Jurkat--Richert factor. The first interval and post-3 source formula are both consumed from the actual Section-13 source contract; no finite Rosser-density estimate is assumed.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiContinuousUpperFactor_eq_jurkatRichertUpperLinearSieveFactor_of_sourceContract (H : SuzukiLemma144KappaOne.Section13HatLayers) (hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hslo : 3 / 2 ≤ s) (hshi : s ≤ 4) : suzukiContinuousUpperFactor s = jurkatRichertUpperLinearSieveFactor s

The complete upper-factor identification on Chen's varying-q window, with the amplitude normalization discharged by the same genuine source contract.