Alternating-pair contraction and geometric iteration

Near-pair estimates combine with far tails to give quadratic contraction. Relative transitions, Euler products, and logarithmic cocycles yield geometric bounds for the iterated discrete alternating-pair operator.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_filter_swap_of_imp {α : Type u_1} {β : Type u_2} {M : Type u_3} [DecidableEq α] [DecidableEq β] [AddCommMonoid M] (A : Finset α) (B : Finset β) (rel : α → β → Prop) [DecidableRel rel] (keep : β → Prop) [DecidablePred keep] (f : α → β → M) (hkeep : ∀ a ∈ A, ∀ b ∈ B, rel a b → keep b) : ∑ a ∈ A, ∑ b ∈ B with (rel a) b, f a b = ∑ b ∈ B with keep b, ∑ a ∈ A with rel a b, f a b

A filtered finite double sum may be transposed after discarding outer indices that cannot support the relation.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_normalized_near_le (K ρ R : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hR : 3 ≤ R) : ∃ (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 with Real.log ↑p₀ / Real.log ↑q < R, ∑ 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₁)) * LinearSieve.upperRosserAlternatingPairNormalizedKernel r (Real.log ↑p₁ / Real.log ↑q) (Real.log ↑p₀ / Real.log ↑q) ≤ 4 / 5 + ρ

On a fixed logarithmic-ratio window, one discrete reverse Rosser pair has the same strict contraction as its continuous model, up to an arbitrarily small uniform error.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_quadratic_near_le (K ρ R : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hR : 3 ≤ R) : ∃ (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 with Real.log ↑p₀ / Real.log ↑q < R, ∑ 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 ≤ (4 / 5 + ρ) * r ^ 2

Compact-ratio reverse-pair contraction in the unnormalized quadratic form used by the Rosser recursion.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_quadratic_le_nine_tenths (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 ≤ 9 / 10 * r ^ 2

A full discrete reverse Rosser pair contracts the quadratic suffix envelope by a fixed factor strictly below one, uniformly in the terminal prime.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteIterate (w : ℕ → ℝ) : ℕ → ℕ → ℝ → Finset ℕ → ℝ

The finite discrete reverse-pair iterate. At each step the larger newly adjoined prime becomes the terminal scale, so the residual state is renormalized by its logarithmic ratio and the remaining ambient primes are restricted above it.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteIterate w 0 x✝² x✝¹ x✝ = x✝¹ ^ 2
• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteIterate w k.succ x✝² x✝¹ x✝ = ∑ p₀ ∈ x✝, ∑ p₁ ∈ x✝ with p₁ < p₀ ∧ 2 * (Real.log ↑p₀ / Real.log ↑x✝²) < Real.log ↑p₁ / Real.log ↑x✝² + x✝¹, w p₀ * w p₁ * MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteIterate w k p₀ ((x✝¹ + Real.log ↑p₁ / Real.log ↑x✝² + Real.log ↑p₀ / Real.log ↑x✝²) / (Real.log ↑p₀ / Real.log ↑x✝²)) ({p ∈ x✝ | p₀ < p})

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeIterate (nu : ℕ → ℝ) (k q : ℕ) (r : ℝ) (P : Finset ℕ) : ℝ

The reverse-pair iterate on the relative Euler-product scale. Unlike the selected-weight iterate, this state keeps the complete ambient denominator and therefore retains all primes skipped before the newly selected pair.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeIterate nu k q r P = MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteIterate nu k q r P / ∏ p ∈ P, (1 - nu p)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeTransition (nu : ℕ → ℝ) (P : Finset ℕ) (p₀ p₁ : ℕ) : ℝ

The exact relative transition for adjoining the two smallest selected primes in a reverse-built Rosser chain.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeTransition nu P p₀ p₁ = (nu p₀ * nu p₁ * ∏ p ∈ P with p₀ < p, (1 - nu p)) / ∏ p ∈ P, (1 - nu p)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeIterate_zero (nu : ℕ → ℝ) (q : ℕ) (r : ℝ) (P : Finset ℕ) : upperRosserAlternatingPairDiscreteRelativeIterate nu 0 q r P = r ^ 2 / ∏ p ∈ P, (1 - nu p)

At depth zero the relative adaptive state is the quadratic envelope divided by the full ambient Euler product.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeIterate_succ (nu : ℕ → ℝ) {k q : ℕ} {r : ℝ} {P : Finset ℕ} (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserAlternatingPairDiscreteRelativeIterate nu (k + 1) q r P = ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ 2 * (Real.log ↑p₀ / Real.log ↑q) < Real.log ↑p₁ / Real.log ↑q + r, upperRosserAlternatingPairDiscreteRelativeTransition nu P p₀ p₁ * upperRosserAlternatingPairDiscreteRelativeIterate nu k p₀ ((r + Real.log ↑p₁ / Real.log ↑q + Real.log ↑p₀ / Real.log ↑q) / (Real.log ↑p₀ / Real.log ↑q)) ({p ∈ P | p₀ < p})

Exact successor recursion for the relative adaptive state. The quotient of residual and ambient Euler products is part of each transition, so the recursion does not discard the sieve-product scale.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeTransition_mul_eulerProduct (nu : ℕ → ℝ) {P : Finset ℕ} {p₀ p₁ : ℕ} (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserAlternatingPairDiscreteRelativeTransition nu P p₀ p₁ * ∏ p ∈ P, (1 - nu p) = nu p₀ * nu p₁ * ∏ p ∈ P with p₀ < p, (1 - nu p)

Restoring the ambient Euler product cancels one relative reverse-pair transition exactly.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeTransition_eq_div_lowerProduct (nu : ℕ → ℝ) {P : Finset ℕ} {p₀ p₁ : ℕ} (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserAlternatingPairDiscreteRelativeTransition nu P p₀ p₁ = nu p₀ * nu p₁ / ∏ p ∈ P with p ≤ p₀, (1 - nu p)

A relative reverse-pair transition is the selected pair divided by the Euler product through the larger new prime. This form isolates precisely the skipped lower-prime mass that the next quantitative contraction must control.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.prod_one_sub_filter_le_eq_two_gaps (nu : ℕ → ℝ) {P : Finset ℕ} {p₀ p₁ : ℕ} (hp₀ : p₀ ∈ P) (hp₁ : p₁ ∈ P) (h10 : p₁ < p₀) : ∏ p ∈ P with p ≤ p₀, (1 - nu p) = ((1 - nu p₀) * (1 - nu p₁) * ∏ p ∈ P with p < p₁, (1 - nu p)) * ∏ p ∈ P with p₁ < p ∧ p < p₀, (1 - nu p)

The Euler product through two ordered selected primes splits into the two skipped gaps and the factors at the selected primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeTransition_eq_normalized_twoGapProducts (nu : ℕ → ℝ) {P : Finset ℕ} {p₀ p₁ : ℕ} (hp₀ : p₀ ∈ P) (hp₁ : p₁ ∈ P) (h10 : p₁ < p₀) (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserAlternatingPairDiscreteRelativeTransition nu P p₀ p₁ = (nu p₀ / (1 - nu p₀) * (nu p₁ / (1 - nu p₁)) * ∏ p ∈ P with p < p₁, (1 - nu p)⁻¹) * ∏ p ∈ P with p₁ < p ∧ p < p₀, (1 - nu p)⁻¹

Exact two-gap form of a relative reverse-pair transition. Every ambient prime below p₀ occurs exactly once, either as one of the selected primes or in one of the two skipped inverse-Euler products.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserRelativeSkippedGaps_le_logCocycle {S : BoundingSieve} {K : ℝ} {q p₀ p₁ : ℕ} {P : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hq : Nat.Prime q) (hP : P ⊆ S.prodPrimes.primeFactors) (hqP : ∀ p ∈ P, q < p) (hp₀ : p₀ ∈ P) (hp₁ : p₁ ∈ P) (h10 : p₁ < p₀) : (∏ p ∈ P with p < p₁, (1 - S.nu p)⁻¹) * ∏ p ∈ P with p₁ < p ∧ p < p₀, (1 - S.nu p)⁻¹ ≤ Real.log ↑p₀ / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) * (1 + K / Real.log (↑p₁ + 1))

The two skipped Euler gaps form a logarithmic cocycle. Their main logarithmic ratios telescope from q directly to p₀; only the local-product errors at the two successive base scales remain.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeTransition_le_logCocycle {S : BoundingSieve} {K : ℝ} {q p₀ p₁ : ℕ} {P : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hq : q ∈ S.prodPrimes.primeFactors) (hP : P ⊆ S.prodPrimes.primeFactors) (hqP : ∀ p ∈ P, q < p) (hp₀ : p₀ ∈ P) (hp₁ : p₁ ∈ P) (h10 : p₁ < p₀) : upperRosserAlternatingPairDiscreteRelativeTransition (⇑S.nu) P p₀ p₁ ≤ S.nu p₀ / (1 - S.nu p₀) * (S.nu p₁ / (1 - S.nu p₁)) * (Real.log ↑p₀ / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) * (1 + K / Real.log (↑p₁ + 1)))

Quantitative two-gap bound for one relative reverse-pair transition. This is the cocycle-preserving replacement for charging the whole lower interval as an unrelated factor at every recursive step.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeTransition_mul_logScale_le {S : BoundingSieve} {K : ℝ} {q p₀ p₁ : ℕ} {P : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hq : q ∈ S.prodPrimes.primeFactors) (hP : P ⊆ S.prodPrimes.primeFactors) (hqP : ∀ p ∈ P, q < p) (hp₀ : p₀ ∈ P) (hp₁ : p₁ ∈ P) (h10 : p₁ < p₀) : upperRosserAlternatingPairDiscreteRelativeTransition (⇑S.nu) P p₀ p₁ * (Real.log (↑q + 1) / Real.log ↑p₀) ≤ S.nu p₀ / (1 - S.nu p₀) * (S.nu p₁ / (1 - S.nu p₁)) * ((1 + K / Real.log (↑q + 1)) * (1 + K / Real.log (↑p₁ + 1)))

Multiplying by the natural terminal-scale ratio cancels the full main logarithmic growth of a relative transition. This is the one-step Lyapunov transfer needed to iterate the completed operator without paying a fresh Euler-product factor at every pair.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteRelativeTransition_le_localProduct {S : BoundingSieve} {K : ℝ} {q p₀ p₁ : ℕ} {P : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hq : q ∈ S.prodPrimes.primeFactors) (hP : P ⊆ S.prodPrimes.primeFactors) (hqP : ∀ p ∈ P, q < p) (hp₀ : p₀ ∈ P) (hp₁ : p₁ ∈ P) : upperRosserAlternatingPairDiscreteRelativeTransition (⇑S.nu) P p₀ p₁ ≤ S.nu p₀ * S.nu p₁ * (Real.log (↑p₀ + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)))

The local-product hypothesis gives the first quantitative bound for a relative reverse-pair transition. It charges exactly one interval factor from the previous terminal prime through the larger new prime; retaining this factor inside the recursive state avoids the invalid absolute-tail cancellation.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscreteIterate_le (K : ℝ) (hK : 1 ≤ K) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (k q : ℕ) (r : ℝ) (P : Finset ℕ), Q ≤ ↑q → Nat.Prime q → HasDimensionOneLocalProductBound S K → 3 ≤ r → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q < p) → upperRosserAlternatingPairDiscreteIterate (fun (p : ℕ) => S.nu p / (1 - S.nu p)) k q r P ≤ (9 / 10) ^ k * r ^ 2

Iterating the uniform discrete reverse-pair contraction gives a geometric depth bound. This is the quantitative tail estimate for reverse-built Rosser chains whose terminal prime is above the uniform local-product cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscrete_quadratic_le_coarse {S : BoundingSieve} {K r : ℝ} {q : ℕ} {P : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hr : 3 ≤ r) (hq : Nat.Prime q) (hP : P ⊆ S.prodPrimes.primeFactors) (hqP : ∀ 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 ≤ 18 * (1 + K / Real.log 2) * (1 + 2 * (K / Real.log 2)) * r ^ 2

A coarse reverse-pair bound valid at every prime terminal. Unlike the contractive estimate, its constant need not be below one; it is used only for the finitely many steps before the terminal prime reaches the uniform Stieltjes cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscreteIterate_shifted_le (K : ℝ) (hK : 1 ≤ K) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (S : BoundingSieve) (k n q : ℕ) (r : ℝ) (P : Finset ℕ), Q ≤ ↑q + 2 * ↑n → Nat.Prime q → HasDimensionOneLocalProductBound S K → 3 ≤ r → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q < p) → upperRosserAlternatingPairDiscreteIterate (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (k + n) q r P ≤ (18 * (1 + K / Real.log 2) * (1 + 2 * (K / Real.log 2))) ^ n * (9 / 10) ^ k * r ^ 2

After n preliminary reverse pairs, the terminal prime is at least 2n larger. Thus only finitely many coarse steps are needed before every remaining pair contracts geometrically.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscreteIterate_eventually_geometric (K : ℝ) (hK : 1 ≤ K) : ∃ (N : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (S : BoundingSieve) (k q : ℕ) (r : ℝ) (P : Finset ℕ), Nat.Prime q → HasDimensionOneLocalProductBound S K → 3 ≤ r → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q < p) → upperRosserAlternatingPairDiscreteIterate (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (k + N) q r P ≤ C * (9 / 10) ^ k * r ^ 2

Uniformly in the initial terminal prime, a fixed number of preliminary reverse pairs reaches the contractive range. Every later depth therefore has one geometric envelope, with a constant depending only on the dimension-one local-product constant.