Finite-depth geometric control of the relative upper Rosser iterate

The depth-zero state is kept as the exact quotient by the ambient Euler product. The dimension-one local-product estimate is used once, at initialization; later reverse-pair steps are paid by the relative Lyapunov contraction.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeIterate_zero_eq_and_le_localProduct {S : BoundingSieve} {K z r : ℝ} {q : ℕ} {P : Finset ℕ} (hq : Nat.Prime q) (hlocal : HasDimensionOneLocalProductBound S K) (hqz : ↑q ≤ z) (hP : P ⊆ S.prodPrimes.primeFactors) (hqP : ∀ p ∈ P, q < p) (hzP : ∀ p ∈ P, ↑p ≤ z) : upperRosserAlternatingPairDiscreteRelativeIterate (⇑S.nu) 0 q r P = r ^ 2 / ∏ p ∈ P, (1 - S.nu p) ∧ upperRosserAlternatingPairDiscreteRelativeIterate (⇑S.nu) 0 q r P ≤ r ^ 2 * (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)))

Depth-zero initialization, with the Euler-product denominator displayed before it is paid by the existing local-product bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscreteRelativeIterate_finiteDepth_geometric (K : ℝ) (hK : 1 ≤ K) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (k q : ℕ) (r z : ℝ) (P : Finset ℕ), Q ≤ ↑q → Nat.Prime q → HasDimensionOneLocalProductBound S K → 3 ≤ r → ↑q ≤ z → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q < p) → (∀ p ∈ P, ↑p ≤ z) → upperRosserAlternatingPairDiscreteRelativeIterate (⇑S.nu) k q r P ≤ 101 / 100 * (Real.log (z + 1) / Real.log (↑q + 1)) * (9 / 10) ^ k * r ^ 2

Finite-depth geometric estimate for the relative reverse-pair state.

The prefactor is exactly the one-time initialization cost of the depth-zero Euler-product denominator. It is not charged again at recursive depths.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthRelativeDensity_geometric (K : ℝ) (hK : 1 ≤ K) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (k q : ℕ) (z Δ s : ℝ), Q ≤ ↑q → 2 ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → q ∈ S.prodPrimes.primeFactors → LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ 9 * (101 / 100) * (Real.log (z + 1) / Real.log (↑q + 1)) * (9 / 10) ^ k

Consumer for the actual fixed-depth boundary-chain relative density.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChains_finiteRelativeBlock_geometric (K : ℝ) (hK : 1 ≤ K) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (L n q : ℕ) (z Δ s : ℝ), Q ≤ ↑q → 2 ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → q ∈ S.prodPrimes.primeFactors → ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j) ≤ 90 * (101 / 100) * (Real.log (z + 1) / Real.log (↑q + 1)) * (9 / 10) ^ L

Every finite block of relative boundary layers has a geometric tail bound. The remaining logarithmic prefactor is precisely the one-time depth-zero initialization cost; this statement does not mislabel it as carrier-uniform.