Power-controlled initialization for the relative upper Rosser iterate

The relative finite-depth estimate carries the one-time factor log (z + 1) / log (q + 1). This module removes that factor only under the explicit, quantitatively sufficient hypothesis z + 1 ≤ ((q : ℝ) + 1) ^ C.

The Chen upper-source window assumption s ≤ 4 does not by itself have this shape: the currently callable upper Rosser producers assume only that every carrier prime is at most z. Thus the final definition records the exact additional bridge needed to make the estimate uniform over all large terminal primes in a carrier; no such bridge is asserted here.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.log_add_one_div_log_nat_add_one_le_of_le_rpow {q : ℕ} {z C : ℝ} (hq : Nat.Prime q) (hqz : ↑q ≤ z) (hpow : z + 1 ≤ (↑q + 1) ^ C) : Real.log (z + 1) / Real.log (↑q + 1) ≤ C

A power comparison gives the strongest corresponding logarithmic initialization-ratio comparison. Positivity of the denominator is supplied by primality, while q ≤ z supplies positivity of z + 1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscreteRelativeIterate_finiteDepth_uniform_of_rpow (K : ℝ) (hK : 1 ≤ K) (C : ℝ) : ∃ (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) → z + 1 ≤ (↑q + 1) ^ C → upperRosserAlternatingPairDiscreteRelativeIterate (⇑S.nu) k q r P ≤ 101 / 100 * C * (9 / 10) ^ k * r ^ 2

The relative reverse-pair iterate is genuinely uniform in the carrier once one supplies a fixed power bound between its ambient endpoint and terminal. The factor 101/100 is the already proved one-time local-product payment.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthRelativeDensity_uniform_of_rpow (K : ℝ) (hK : 1 ≤ K) (C : ℝ) : ∃ (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 → z + 1 ≤ (↑q + 1) ^ C → LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ 9 * (101 / 100) * C * (9 / 10) ^ k

Uniform-in-carrier fixed-depth estimate for the actual relative boundary chain density, conditional only on the explicit endpoint power comparison.

def MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserLargeTerminalInitializationPowerBound (C Q z : ℝ) (S : BoundingSieve) : Prop

Exact missing interface for using the preceding theorem uniformly over the large-terminal part of an upper Rosser carrier.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserLargeTerminalInitializationPowerBound C Q z S = ∀ (q : ℕ), Q ≤ ↑q → q ∈ S.prodPrimes.primeFactors → z + 1 ≤ (↑q + 1) ^ C

def MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserChenWindowInitializationPowerBridge (C : ℝ) : Prop

The missing bridge in the actual Chen upper-source parameter window, stated with the same q,z information exposed by the current finite-prefix and adaptive-tail producers. In particular, s ≤ 4 and s = log Δ / log z are recorded, but the existing carrier hypothesis only says q ≤ z; it does not prove the reverse power comparison required above.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserChenWindowInitializationPowerBridge C = ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ), 2 ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserLargeTerminalInitializationPowerBound C Q z S