Rosser boundary densities and dyadic tails

Dyadic log-ratio cells control far alternating pairs. Mesh corrections, atomic bounds, and factorial density estimates majorize finite Rosser boundary chains.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserLogRatioDyadicCell (x : ℝ) : ℕ

The dyadic cell containing a real number at least one. It is used with x = log p / log q, so the cells rescale with the current terminal prime instead of with the global sieve cutoff.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserLogRatioDyadicCell x = if hx : 1 ≤ x then Classical.choose ⋯ else 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserLogRatioDyadicCell_spec {x : ℝ} (hx : 1 ≤ x) : 2 ^ upperRosserLogRatioDyadicCell x ≤ x ∧ x < 2 ^ (upperRosserLogRatioDyadicCell x + 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_nu_div_one_sub_le_logRatio_dyadicCell {S : BoundingSieve} {K η : ℝ} {q n : ℕ} {T : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hq : Nat.Prime q) (herror : K / Real.log ↑q ≤ η) (hT : T ⊆ S.prodPrimes.primeFactors) (hqT : ∀ p ∈ T, q < p) : ∑ p ∈ T with upperRosserLogRatioDyadicCell (Real.log ↑p / Real.log ↑q) = n, S.nu p / (1 - S.nu p) ≤ 1 + 2 * η

A dyadic logarithmic-ratio cell has uniformly bounded normalized density mass once the local-product correction is small at the cell's base prime.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_nu_div_one_sub_mul_inv_logRatio_le_geometric_tail {S : BoundingSieve} {K η : ℝ} {q m : ℕ} {T : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hη : 0 ≤ η) (hq : Nat.Prime q) (herror : K / Real.log ↑q ≤ η) (hT : T ⊆ S.prodPrimes.primeFactors) (hqT : ∀ p ∈ T, q < p) (hfar : ∀ p ∈ T, 2 ^ m ≤ Real.log ↑p / Real.log ↑q) : ∑ p ∈ T, S.nu p / (1 - S.nu p) * (Real.log ↑p / Real.log ↑q)⁻¹ ≤ 2 * (1 + 2 * η) * (1 / 2) ^ m

A scale-adaptive inverse-log moment bound. Unlike a fixed logarithmic screen, the dyadic cells are based at q; hence the estimate remains uniform when log q / log z tends to zero.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscrete_quadratic_far_le {S : BoundingSieve} {K η r : ℝ} {q m : ℕ} {P T : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hη : 0 ≤ η) (hr : 3 ≤ r) (hq : Nat.Prime q) (herror : K / Real.log ↑q ≤ η) (hP : P ⊆ S.prodPrimes.primeFactors) (hqP : ∀ p ∈ P, q < p) (hT : T ⊆ P) (hfar : ∀ p ∈ T, 2 ^ m ≤ Real.log ↑p / Real.log ↑q) : ∑ p₀ ∈ T, ∑ 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 + η) * (1 + 2 * η) * (1 / 2) ^ m * r ^ 2

The part of a discrete reverse Rosser pair whose larger logarithmic ratio lies beyond the m-th dyadic scale has a uniform quadratic tail. The proof uses the alternating-prefix face 2x < y + r to force x < r; the remaining inverse-log moment is controlled by scale-adaptive cells based at q, not by a fixed lower bound for log q / log z.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_quadratic_far_lt (K ρ : ℝ) (hK : 0 ≤ K) (hρ : 0 < ρ) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∃ (m : ℕ), ∀ (S : BoundingSieve) (q : ℕ) (r : ℝ) (P T : Finset ℕ), Q ≤ ↑q → HasDimensionOneLocalProductBound S K → 3 ≤ r → Nat.Prime q → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q < p) → T ⊆ P → (∀ p ∈ T, 2 ^ m ≤ Real.log ↑p / Real.log ↑q) → ∑ p₀ ∈ T, ∑ 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 < ρ * r ^ 2

Uniform tightness of one discrete reverse Rosser pair. Once the terminal prime is above an absolute cutoff, the contribution of larger ratios outside a fixed dyadic window is arbitrarily small relative to the quadratic envelope, uniformly in the sieve, the terminal coordinate, and the state r ≥ 3.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_quadratic_far_lt_uniform (K ρ : ℝ) (hK : 0 ≤ K) (hρ : 0 < ρ) : ∃ (m : ℕ), ∀ (S : BoundingSieve) (q : ℕ) (r : ℝ) (P T : Finset ℕ), HasDimensionOneLocalProductBound S K → 3 ≤ r → Nat.Prime q → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q < p) → T ⊆ P → (∀ p ∈ T, 2 ^ m ≤ Real.log ↑p / Real.log ↑q) → ∑ p₀ ∈ T, ∑ 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 < ρ * r ^ 2

Uniform tightness of one discrete reverse Rosser pair, including terminal primes whose global logarithmic coordinate tends to zero. The dyadic cutoff depends only on K and the requested error.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscrete_quadratic_le_near_add {S : BoundingSieve} {K η r : ℝ} {q m : ℕ} {P : Finset ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hK : 0 ≤ K) (hη : 0 ≤ η) (hr : 3 ≤ r) (hq : Nat.Prime q) (herror : K / Real.log ↑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 ≤ ∑ p₀ ∈ P with Real.log ↑p₀ / Real.log ↑q < 2 ^ m, ∑ 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 + η) * (1 + 2 * η) * (1 / 2) ^ m * r ^ 2

Splitting at a relative dyadic scale reduces the full discrete reverse-pair sum to a compact-ratio part and an explicit geometric remainder.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserAlternatingPairDiscrete_quadratic_le_near_add (K ρ : ℝ) (hK : 0 ≤ K) (hρ : 0 < ρ) : ∃ (m : ℕ), ∀ (S : BoundingSieve) (q : ℕ) (r : ℝ) (P : Finset ℕ), HasDimensionOneLocalProductBound S K → 3 ≤ r → Nat.Prime q → 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 < ∑ p₀ ∈ P with Real.log ↑p₀ / Real.log ↑q < 2 ^ m, ∑ 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 + ρ * r ^ 2

Uniform compactness reduction for the discrete reverse-pair operator. A single dyadic window, depending only on K and ρ, works for every sieve and every terminal prime, even when its global logarithmic coordinate vanishes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_correctedDarboux_le_add (m : ℕ) {K ρ B c : ℝ} (hK : 0 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hc : 0 < c) (hc1 : c < 1) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (z : ℝ), z₀ ≤ z → ∀ (M : Fin (m + 1) → ℝ), (∀ (i : Fin (m + 1)), 0 ≤ M i ∧ M i ≤ B) → ∑ i : Fin (m + 1), M i * (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i * (1 + K / (upperRosserFixedDepthMeshLeft c m i * Real.log z)) - 1) ≤ ∑ i : Fin (m + 1), M i * (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i - 1) + ρ

On any fixed positive mesh, all local-product correction factors can be removed from a bounded nonnegative Darboux sum at a prescribed total cost.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserFixedDepthMesh_incrementSum_le (m : ℕ) {c : ℝ} (hc : 0 < c) (hc1 : c < 1) : ∑ i : Fin (m + 1), (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i - 1) ≤ c⁻¹

The total uncorrected logarithmic increment of a fixed mesh is uniformly bounded by the reciprocal of its positive lower endpoint.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_correctedIncrementSum_le (m : ℕ) {K ρ c : ℝ} (hK : 0 ≤ K) (hρ : 0 < ρ) (hc : 0 < c) (hc1 : c < 1) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (z : ℝ), z₀ ≤ z → ∑ i : Fin (m + 1), (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i * (1 + K / (upperRosserFixedDepthMeshLeft c m i * Real.log z)) - 1) ≤ c⁻¹ + ρ

The corrected outer-mesh increments have bounded total mass. This turns a uniform additive error in every inner cell into one controlled outer error in the two-partition Rosser successor.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_dimensionOne_atom_cutoff (K η c : ℝ) (hK : 1 ≤ K) (hη : 0 < η) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (q : ℕ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → q ∈ S.prodPrimes.primeFactors → z ^ c ≤ ↑q → S.nu q / (1 - S.nu q) ≤ η

Above any fixed positive logarithmic coordinate, every individual normalized density atom is uniformly small once the global cutoff is large. This controls the hyperplane and endpoint atoms in fixed-depth Darboux sums.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChains_fixed_length_atom_le (K η : ℝ) (k : ℕ) (hK : 1 ≤ K) (hη : 0 < η) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ) (q : ℕ) (l : List ℕ), z₀ ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → q ∈ S.prodPrimes.primeFactors → l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) → l.length = 2 * k → S.nu q / (1 - S.nu q) ≤ η ∧ ∀ p ∈ l, S.nu p / (1 - S.nu p) ≤ η

At fixed Rosser depth, one cutoff makes the normalized density of the distinguished prime and of every selected prime uniformly smaller than a prescribed tolerance.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_fixed_length_localProduct_error_le {S : BoundingSieve} {K z Δ s : ℝ} {q k : ℕ} {l : List ℕ} (hK : 0 ≤ K) (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (hl : l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p})) (hlen : l.length = 2 * k) : K / (Real.log ↑q / Real.log z * Real.log z) ≤ 2 * 3 ^ k * K / Real.log z ∧ ∀ x ∈ LinearSieve.logarithmicCoordinates z l, K / (x * Real.log z) ≤ 2 * 3 ^ k * K / Real.log z

On depth-2k boundary carriers, every local-product correction is at most 2 * 3^k * K / log z. Thus the K / log errors are uniformly harmless after the depth cutoff has been fixed.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChains_fixed_length_localProduct_error_le (K η : ℝ) (k : ℕ) (hK : 0 ≤ K) (hη : 0 < η) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ) (q : ℕ) (l : List ℕ), z₀ ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → q ∈ S.prodPrimes.primeFactors → l ∈ LinearSieve.upperRosserBoundaryChains (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) → l.length = 2 * k → K / (Real.log ↑q / Real.log z * Real.log z) ≤ η ∧ ∀ x ∈ LinearSieve.logarithmicCoordinates z l, K / (x * Real.log z) ≤ η

After fixing the Rosser depth, one cutoff makes every local-product correction on every boundary carrier smaller than a prescribed tolerance.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.factorial_mul_upperRosserBoundaryChains_fixed_length_density_le {S : BoundingSieve} {K z : ℝ} {D q ell : ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) : ↑ell.factorial * ∑ l ∈ LinearSieve.upperRosserBoundaryChains D q ({p ∈ S.prodPrimes.primeFactors | q < p}) with l.length = ell, (List.map (fun (p : ℕ) => S.nu p / (1 - S.nu p)) l).prod ≤ (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) - 1) ^ ell

The selected part of a fixed-depth Rosser boundary has factorial decay. The base of the power is the dimension-one mass of the complete prime tail above q; imposing the Rosser region can only decrease this mass.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_fixed_length_density_le_pow_div_factorial {S : BoundingSieve} {K z : ℝ} {D q ell : ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) : ∑ l ∈ LinearSieve.upperRosserBoundaryChains D q ({p ∈ S.prodPrimes.primeFactors | q < p}) with l.length = ell, (List.map (fun (p : ℕ) => S.nu p / (1 - S.nu p)) l).prod ≤ (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) - 1) ^ ell / ↑ell.factorial

Direct M ^ ell / ell! form of the dimension-one fixed-depth bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserTailComplement_invProduct_le {S : BoundingSieve} {K z : ℝ} {q : ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (s : Finset ℕ) : ∏ p ∈ {p ∈ S.prodPrimes.primeFactors | q < p} \ s, (1 - S.nu p)⁻¹ ≤ Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1))

A skipped complement in the tail above q is controlled by the dimension-one product estimate on [q + 1, z + 1).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserTailFactor_le_logCoordinate {K z η : ℝ} {q : ℕ} (hK : 0 ≤ K) (hz : 1 < z) (hq : Nat.Prime q) (hη : 0 ≤ η) (hlogRatio : Real.log (z + 1) / Real.log z ≤ 1 + η) (herror : K / (Real.log ↑q / Real.log z * Real.log z) ≤ η) : Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) ≤ (1 + η) ^ 2 * (Real.log ↑q / Real.log z)⁻¹

On a logarithmic coordinate bounded away from zero, the skipped-prime tail factor contributes at most one further reciprocal-coordinate factor, up to the two uniform local-product errors. This is the factor-bearing estimate needed when the outer Rosser prime is inserted into a logarithmic mesh.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryPathTerm_le {S : BoundingSieve} {K z : ℝ} {q : ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) {s : Finset ℕ} (hs : s ⊆ {p ∈ S.prodPrimes.primeFactors | q < p}) : (∏ p ∈ s, S.nu p / (1 - S.nu p)) * ∏ p ∈ {p ∈ S.prodPrimes.primeFactors | q < p} \ s, (1 - S.nu p)⁻¹ ≤ (∏ p ∈ s, S.nu p / (1 - S.nu p)) * (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)))

The skipped-prime part of one Rosser boundary path can be replaced by the dimension-one interval factor, leaving only the selected prime ratios.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryDensity_div_eulerProduct_le {S : BoundingSieve} {K z : ℝ} {D q : ℕ} (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) : (∑ s ∈ {p ∈ S.prodPrimes.primeFactors | q < p}.powerset with (LinearSieve.UpperRosserBoundarySet D q) s, ∏ p ∈ s, S.nu p) / ∏ p ∈ S.prodPrimes.primeFactors with q < p, (1 - S.nu p) ≤ Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) * ∑ s ∈ {p ∈ S.prodPrimes.primeFactors | q < p}.powerset with (LinearSieve.UpperRosserBoundarySet D q) s, ∏ p ∈ s, S.nu p / (1 - S.nu p)

Quantitative reduction of a normalized boundary mass to the selected Rosser chains. This removes all skipped primes using only the local-product hypothesis; the remaining sum carries the cubic boundary condition.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserSetDensityRatio_le_one_add_boundaryChains {S : BoundingSieve} {K z : ℝ} {D : ℕ} (hD : 1 < D) (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hlevel : ∀ p ∈ S.prodPrimes.primeFactors, p < D) : LinearSieve.upperRosserSetDensitySum (⇑S.nu) D S.prodPrimes.primeFactors / ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p) ≤ 1 + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) * ∑ s ∈ {p ∈ S.prodPrimes.primeFactors | q < p}.powerset with (LinearSieve.UpperRosserBoundarySet D q) s, ∏ p ∈ s, S.nu p / (1 - S.nu p))

The normalized upper Rosser density is bounded by an explicit finite sum over selected cubic-boundary chains. All unselected Euler factors have been absorbed by the dimension-one interval estimate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserSetDensityRatio_le_one_add_boundaryChains_by_even_length {S : BoundingSieve} {K z : ℝ} {D : ℕ} (hD : 1 < D) (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hlevel : ∀ p ∈ S.prodPrimes.primeFactors, p < D) : LinearSieve.upperRosserSetDensitySum (⇑S.nu) D S.prodPrimes.primeFactors / ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p) ≤ 1 + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) * ∑ ell ∈ Finset.range ({p ∈ S.prodPrimes.primeFactors | q < p}.card + 1) with Even ell, ∑ l ∈ LinearSieve.upperRosserBoundaryChains D q ({p ∈ S.prodPrimes.primeFactors | q < p}) with l.length = ell, (List.map (fun (p : ℕ) => S.nu p / (1 - S.nu p)) l).prod)

The normalized density bound grouped by the even length of each canonical decreasing Rosser boundary chain. This exposes exactly the finite depth parameter to which the factorial estimate applies.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserSetDensityRatio_le_one_add_boundaryChains_by_depth {S : BoundingSieve} {K z : ℝ} {D : ℕ} (hD : 1 < D) (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hlevel : ∀ p ∈ S.prodPrimes.primeFactors, p < D) : LinearSieve.upperRosserSetDensitySum (⇑S.nu) D S.prodPrimes.primeFactors / ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p) ≤ 1 + ∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * (Real.log (z + 1) / Real.log (↑q + 1) * (1 + K / Real.log (↑q + 1)) * ∑ k ∈ Finset.range ({p ∈ S.prodPrimes.primeFactors | q < p}.card + 1), LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) D q ({p ∈ S.prodPrimes.primeFactors | q < p}) k)

The normalized upper Rosser density bound indexed directly by Buchstab pair depth. Each inner term is now exactly the quantity governed by upperRosserBoundaryChainsFixedDepthDensity_succ.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.lt_floor_add_one_of_le_of_log_ratio {p : ℕ} {z Δ s : ℝ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hp : ↑p ≤ z) (hs : s = Real.log Δ / Real.log z) (hslo : 3 / 2 ≤ s) : p < ⌊Δ⌋₊ + 1

A sieve ratio strictly larger than one places every integer below the sifting cutoff strictly below the natural Rosser level ⌊Δ⌋ + 1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.ceilDiv_floor_add_one_eq_floor_div_add_one {Δ : ℝ} {c : ℕ} (hΔ : 0 ≤ Δ) (hc : 0 < c) : (⌊Δ⌋₊ + 1) ⌈/⌉ c = ⌊Δ / ↑c⌋₊ + 1

Dividing a strict real cutoff by a positive integer commutes exactly with the floor + 1 convention used for Rosser levels.