Finite-to-continuous upper Rosser producer

This module isolates the normalization bridge between the finite continuous boundary factors already used by the upper Rosser mesh argument and Suzuki's actual odd source series. It does not assume an upper-density conclusion.

def MathlibNt.SieveTheory.SuzukiUpperRosserBoundarySourceLayerIdentity : Prop

Exact layerwise normalization required to identify the continuous Rosser boundary recursion with Suzuki's odd source layers. This is strictly a source identity: it mentions neither a BoundingSieve nor a Rosser-density bound.

Equations

• MathlibNt.SieveTheory.SuzukiUpperRosserBoundarySourceLayerIdentity = ∀ (k : ℕ) (s : ℝ), 3 / 2 ≤ s → s ≤ 4 → ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass k s a = MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) s

def MathlibNt.SieveTheory.SuzukiUpperRosserBoundarySourceSuccLayerIdentity : Prop

The genuinely recursive residual after the first odd source layer has been identified. Its indexing starts at Rosser pair-depth one / Suzuki source index three, so the already closed depth-zero shell is not hidden in the interface.

Equations

• MathlibNt.SieveTheory.SuzukiUpperRosserBoundarySourceSuccLayerIdentity = ∀ (k : ℕ) (s : ℝ), 3 / 2 ≤ s → s ≤ 4 → ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass (k + 1) s a = MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1) + 1) s

theorem MathlibNt.SieveTheory.upperRosserBoundarySourceLayerIdentity_zero {s : ℝ} (hs : 0 < s) : ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * LinearSieve.upperRosserBoundaryMass 0 s a = SuzukiFiniteContinuousLayers.suzukiLayer 1 2 1 s

The outer cubic shell is exactly Suzuki's first odd source layer.

theorem MathlibNt.SieveTheory.SuzukiUpperRosserBoundarySourceLayerIdentity.of_succ (h : SuzukiUpperRosserBoundarySourceSuccLayerIdentity) : SuzukiUpperRosserBoundarySourceLayerIdentity

Closing the positive pair-depth recursion is now exactly sufficient for the full layerwise identity; depth zero is discharged by the cubic-shell theorem.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFiniteBoundaryFactor_le_suzukiContinuousUpperFactor (H : SuzukiLemma144KappaOne.Section13HatLayers) (hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) (hlayerSucc : SuzukiUpperRosserBoundarySourceSuccLayerIdentity) (L : ℕ) {s : ℝ} (hslo : 3 / 2 ≤ s) (hshi : s ≤ 4) : LinearSieve.upperRosserFiniteBoundaryFactor L s ≤ suzukiContinuousUpperFactor s

Every finite continuous boundary prefix is bounded by Suzuki's genuine continuous upper factor. The proof uses the actual summability supplied by the Section-13 source contract and leaves the adaptive discrete depth untouched.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryPrefix_le_suzukiContinuousUpperFactor_sub_one_add (H : SuzukiLemma144KappaOne.Section13HatLayers) (hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) (hlayerSucc : SuzukiUpperRosserBoundarySourceSuccLayerIdentity) (L : ℕ) (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → ∑ k ∈ Finset.range L, ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ suzukiContinuousUpperFactor s - 1 + ρ

The existing fixed-depth mesh estimates therefore land directly below the actual continuous upper source factor, with one cutoff selected before the sieve. No density fundamental lemma is used as an input.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryPrefix_le_jurkatRichertUpperFactor_sub_one_add (H : SuzukiLemma144KappaOne.Section13HatLayers) (hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) (hlayerSucc : SuzukiUpperRosserBoundarySourceSuccLayerIdentity) (L : ℕ) (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → ∑ k ∈ Finset.range L, ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ jurkatRichertUpperLinearSieveFactor s - 1 + ρ

Jurkat--Richert rewrite of the finite-prefix producer. The genuine source contract now supplies both the source-factor identity and its amplitude.