Adaptive finite-carrier bridge for the upper Rosser tail

This file keeps three different facts separate:

• a finite boundary carrier has an exact support depth;
• the already proved fixed-terminal geometric estimate controls every finite block beginning at one cutoff, uniformly in the carrier size;
• passing from that absolute block estimate to the Euler-product-preserving recursive state still needs a one-step relative Lyapunov contraction.

In particular, the continuous 45 * (4 / 5) ^ L volume tail is not used as a bound for a discrete prime sum.

def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryCarrierSupportDepth (P : Finset ℕ) : ℕ

The first pair depth which is forced to vanish solely by the cardinality of its finite ambient carrier.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryCarrierSupportDepth P = P.card / 2 + 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthDensity_eq_zero_at_carrierSupportDepth (w : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) : LinearSieve.upperRosserBoundaryChainsFixedDepthDensity w D q P (upperRosserBoundaryCarrierSupportDepth P) = 0

Exact carrier-support cutoff. This is a finite combinatorial statement; it contains no continuous-volume comparison.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthDensity_eq_zero_of_carrierSupportDepth_le (w : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) {k : ℕ} (hk : upperRosserBoundaryCarrierSupportDepth P ≤ k) : LinearSieve.upperRosserBoundaryChainsFixedDepthDensity w D q P k = 0

Every depth after the adaptive support cutoff vanishes as well.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChains_completeAdaptiveDepth_le_prefix_add_uniformTail (K : ℝ) (hK : 1 ≤ K) : ∃ (N : ℕ) (τ : ℕ → ℝ), Filter.Tendsto τ Filter.atTop (nhds 0) ∧ (∀ (L : ℕ), 0 ≤ τ L) ∧ ∀ (S : BoundingSieve) (L q : ℕ) (z Δ s : ℝ), 2 ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → q ∈ S.prodPrimes.primeFactors → have P := {p ∈ S.prodPrimes.primeFactors | q < p}; ∑ k ∈ Finset.range (P.card + 1), LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P k ≤ ∑ k ∈ Finset.range (L + N), LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P k + τ L

The first honest uniform-in-carrier completion bridge.

The complete adaptive finite sum is bounded by a fixed prefix plus the existing discrete geometric block tail. The carrier cardinality occurs only as the length of the finite remainder block; the cutoff N + L and the error τ L are selected before the sieve and carrier. No continuous tail is substituted for the discrete remainder.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_quadratic_le_seventeen_twentieth (K : ℝ) (hK : 1 ≤ K) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (q : ℕ) (r : ℝ) (P : Finset ℕ), Q ≤ ↑q → Nat.Prime q → HasDimensionOneLocalProductBound S K → 3 ≤ r → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q < p) → ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ 2 * (Real.log ↑p₀ / Real.log ↑q) < Real.log ↑p₁ / Real.log ↑q + r, S.nu p₀ / (1 - S.nu p₀) * (S.nu p₁ / (1 - S.nu p₁)) * ((r + Real.log ↑p₁ / Real.log ↑q + Real.log ↑p₀ / Real.log ↑q) / (Real.log ↑p₀ / Real.log ↑q)) ^ 2 ≤ 17 / 20 * r ^ 2

The absolute reverse-pair operator has spare room below 9/10. This quantitative strengthening is what absorbs the two local-product error factors in the relative transition.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_localProductError_le_one_hundredth (K : ℝ) (_hK : 1 ≤ K) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (x : ℝ), Q ≤ x → K / Real.log (x + 1) ≤ 1 / 100

Uniform smallness of the local-product error once the terminal prime is large. The explicit 1/100 is chosen only to leave ample room between the absolute coefficient 17/20 and the requested relative coefficient 9/10.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserRelativeLyapunovOneStepContraction (K : ℝ) : 1 ≤ K → ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (q : ℕ) (r : ℝ) (P : Finset ℕ), Q ≤ ↑q → Nat.Prime q → HasDimensionOneLocalProductBound S K → 3 ≤ r → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q < p) → ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ 2 * (Real.log ↑p₀ / Real.log ↑q) < Real.log ↑p₁ / Real.log ↑q + r, upperRosserAlternatingPairDiscreteRelativeTransition (⇑S.nu) P p₀ p₁ * (Real.log (↑q + 1) / Real.log ↑p₀) * ((r + Real.log ↑p₁ / Real.log ↑q + Real.log ↑p₀ / Real.log ↑q) / (Real.log ↑p₀ / Real.log ↑q)) ^ 2 ≤ 9 / 10 * r ^ 2

One reverse pair contracts the Euler-product-preserving Lyapunov envelope.

The proof needs the spare 17/20 absolute contraction: the two local-product errors are positive, so the already rounded 9/10 estimate alone cannot imply a 9/10 relative estimate. Above a larger cutoff each error is at most 1/100, and (17/20) * (101/100)^2 < 9/10.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthRelativeDensity_eq_zero_of_carrierSupportDepth_le (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) {k : ℕ} (hk : upperRosserBoundaryCarrierSupportDepth P ≤ k) : LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q P k = 0

Exact finite-boundary relative tail. Once the pair depth reaches the carrier support cutoff, division by the residual Euler product cannot revive a vanishing boundary density. This is the honest finite endpoint to which a future recursive relative-iterate estimate can be attached.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_finiteRelativeTail_eq_zero (nu : ℕ → ℝ) (D q n : ℕ) (P : Finset ℕ) : ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q P (upperRosserBoundaryCarrierSupportDepth P + j) = 0

Every finite block beginning at the adaptive support cutoff is identically zero on the relative Euler-product scale.