Exact final bridge for the upper Rosser density

This module isolates the exact finite bookkeeping between the explicit upper Rosser weight and a fixed prefix plus one uniformly indexed boundary block. The block has common length P.card + 1 - T, so it matches the weighted aggregate-tail producer literally.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mainSum_upperRosserWeight_eq_relativeBoundaryPrefix_add_paddedTail {S : BoundingSieve} {z Δ s : ℝ} (T : ℕ) (hz : 2 ≤ z) (hΔ : 0 < Δ) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) (hT : T ≤ S.prodPrimes.primeFactors.card + 1) : BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) = (1 + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ∑ k ∈ Finset.range T, LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ∑ j ∈ Finset.range (S.prodPrimes.primeFactors.card + 1 - T), LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (T + j)) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S

Exact decomposition of the explicit upper Rosser main sum at an arbitrary prefix threshold T ≤ P.card+1. Every terminal uses the same remainder range P.card+1-T; shorter terminal carriers are padded by identically zero relative boundary layers. Thus there is no off-by-one or terminal-dependent block length left when invoking the weighted aggregate-tail theorem.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mainSum_upperRosserWeight_eq_relativeBoundaryPrefix_add_weightedTail {S : BoundingSieve} {z Δ s : ℝ} (L N : ℕ) (hz : 2 ≤ z) (hΔ : 0 < Δ) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) (hLN : L + N ≤ S.prodPrimes.primeFactors.card + 1) : BoundingSieve.mainSum (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) = (1 + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ∑ k ∈ Finset.range (L + N), LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ∑ j ∈ Finset.range (S.prodPrimes.primeFactors.card + 1 - (L + N)), LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N)) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S

The same exact bridge in the coordinates of the weighted aggregate-tail producer. The prefix threshold is literally L+N, while the remainder is indexed literally by L+j+N; the common block length is P.card+1-(L+N).

def MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserScaledPrefixTailComparison (H : SuzukiLemma144KappaOne.Section13HatLayers) (_hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) : Prop

The exact remaining analytic interface after the finite decomposition. It deliberately keeps the Euler product on both sides. An absolute estimate weightedTail * V ≤ τ L with τ L → 0 does not inhabit this interface: the needed conclusion is at scale ρ * V, uniformly in the varying sieve.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserScaledPrefixTailComparison H _hH = ∀ (K ρ : ℝ), 1 < K → 0 < ρ → ∃ (T : ℕ) (z₀ : ℝ), ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 2 ≤ z → 0 < Δ → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → have T' := min T (S.prodPrimes.primeFactors.card + 1); (1 + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ∑ k ∈ Finset.range T', MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ∑ j ∈ Finset.range (S.prodPrimes.primeFactors.card + 1 - T'), MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (T' + j)) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S ≤ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S

theorem MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneUpperRosserDensityFundamentalLemma_of_scaledPrefixTail (H : SuzukiLemma144KappaOne.Section13HatLayers) (hH : SuzukiLemma144KappaOne.Section13HatSourceContract H) (hfinal : UpperRosserScaledPrefixTailComparison H hH) : DimensionOneUpperRosserDensityFundamentalLemma

Once the scale-faithful prefix-plus-tail comparison is supplied, the target fundamental lemma follows with exactly the required ∃ z₀, ∀ S,z order.