Boundary-chain tails and recursive integrals

Reversed finite Rosser chains embed into alternating-pair iterates. Uniform absolute tails and inner/outer Darboux comparisons connect their fixed-depth densities to continuous boundary-mass integrals.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteChains : ℕ → ℕ → ℝ → Finset ℕ → Finset (List ℕ)

The finite carrier generated by the reverse Rosser-pair recursion. Lists are stored in reverse order, so the innermost pair is visible at the head.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteChains 0 x✝² x✝¹ x✝ = {[]}
• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteChains k.succ x✝² x✝¹ x✝ = Finset.image (fun (b : (_ : ℕ) × (_ : ℕ) × List ℕ) => b.snd.fst :: b.fst :: b.snd.snd) (x✝.sigma fun (p₀ : ℕ) => {p₁ ∈ x✝ | p₁ < p₀ ∧ 2 * (Real.log ↑p₀ / Real.log ↑x✝²) < Real.log ↑p₁ / Real.log ↑x✝² + x✝¹}.sigma fun (p₁ : ℕ) => MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteChains 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}))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteChains_length {k q : ℕ} {r : ℝ} {P : Finset ℕ} {l : List ℕ} (hl : l ∈ upperRosserAlternatingPairDiscreteChains k q r P) : l.length = 2 * k

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserAlternatingPairDiscreteChains_mem_ambient {k q : ℕ} {r : ℝ} {P : Finset ℕ} {l : List ℕ} (hl : l ∈ upperRosserAlternatingPairDiscreteChains k q r P) (p : ℕ) : p ∈ l → p ∈ P

def MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserEvenSuffixCondition (z : ℝ) (q : ℕ) (r : ℝ) (l : List ℕ) : Prop

The exact even-suffix inequalities carried by a reverse-built chain, at the current terminal prime and adaptive state.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserEvenSuffixCondition z q r l = ∀ (i : ℕ) (hi : i < l.length), Even i → 2 * (Real.log ↑l[i] / Real.log z) < (List.map (fun (p : ℕ) => Real.log ↑p / Real.log z) (List.drop (i + 1) l)).sum + r * (Real.log ↑q / Real.log z)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.reverse_mem_upperRosserAlternatingPairDiscreteChains {z r : ℝ} {q k : ℕ} {P : Finset ℕ} {l : List ℕ} (hz : 1 < z) (hq : Nat.Prime q) (hP : ∀ p ∈ l, p ∈ P) (hprime : ∀ p ∈ P, Nat.Prime p) (hqP : ∀ p ∈ P, q < p) (hsorted : l.SortedGT) (hlen : l.length = 2 * k) (hsuffix : UpperRosserEvenSuffixCondition z q r l) : l.reverse ∈ upperRosserAlternatingPairDiscreteChains k q r P

Exact alternating-prefix inequalities embed a decreasing chain, reversed, in the adaptive pair carrier. Thus every inherited screen and cutoff is retained at every recursive pair.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_upperRosserAlternatingPairDiscreteChains_le_iterate (w : ℕ → ℝ) {k q : ℕ} {r : ℝ} {P : Finset ℕ} (hr : 3 ≤ r) (hq : Nat.Prime q) (hP : ∀ p ∈ P, Nat.Prime p) (hqP : ∀ p ∈ P, q < p) (hw : ∀ p ∈ P, 0 ≤ w p) : ∑ l ∈ upperRosserAlternatingPairDiscreteChains k q r P, (List.map w l).prod ≤ upperRosserAlternatingPairDiscreteIterate w k q r P

The weighted reverse-chain carrier is bounded by the existing adaptive pair iterate. Nonnegativity permits enlargement to every admissible pair at each stage.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChains_reverse_mem_alternatingPairDiscreteChains {S : BoundingSieve} {z Δ s : ℝ} {q k : ℕ} {l : List ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (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) : l.reverse ∈ upperRosserAlternatingPairDiscreteChains k q 3 ({p ∈ S.prodPrimes.primeFactors | q < p})

Every actual boundary chain of depth 2k lies in the reverse-pair carrier. This is the bridge from the natural Rosser cutoff to the adaptive discrete iterate; it uses every even-prefix inequality through its suffix form.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthDensity_le_alternatingPairDiscreteIterate_of_nonneg (w : ℕ → ℝ) {S : BoundingSieve} {z Δ s : ℝ} {q k : ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) (hw : ∀ p ∈ S.prodPrimes.primeFactors, 0 ≤ w p) : LinearSieve.upperRosserBoundaryChainsFixedDepthDensity w (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ upperRosserAlternatingPairDiscreteIterate w k q 3 ({p ∈ S.prodPrimes.primeFactors | q < p})

The reverse-pair carrier dominates the fixed-depth boundary density for any nonnegative ambient weight. This weight-generic form is what permits the same geometric carrier to be used before or after Euler normalization.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthDensity_le_alternatingPairDiscreteIterate {S : BoundingSieve} {z Δ s : ℝ} {q k : ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) : LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ upperRosserAlternatingPairDiscreteIterate (fun (p : ℕ) => S.nu p / (1 - S.nu p)) k q 3 ({p ∈ S.prodPrimes.primeFactors | q < p})

The actual normalized fixed-depth boundary-chain density is dominated by the reverse-pair iterate. No unordered or factorial majorant is used: the injection reverses each canonical chain and preserves its monomial exactly.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthRelativeDensity_le_alternatingPairDiscreteRelativeIterate {S : BoundingSieve} {z Δ s : ℝ} {q k : ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) : LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ upperRosserAlternatingPairDiscreteRelativeIterate (⇑S.nu) k q 3 ({p ∈ S.prodPrimes.primeFactors | q < p})

The actual fixed-depth boundary density on the relative Euler-product scale is dominated by the relative adaptive reverse-pair state. This is the exact embedding needed before proving a contraction that preserves the sieve product.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_eventually_geometric (K : ℝ) (hK : 1 ≤ K) : ∃ (N : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (S : BoundingSieve) (k 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 → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (k + N) ≤ 9 * C * (9 / 10) ^ k

The geometric reverse-pair estimate applies to the actual normalized boundary-chain density, uniformly in the level, sieve, and terminal prime.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_uniform_tail (K : ℝ) (hK : 1 ≤ K) : ∃ (N : ℕ) (τ : ℕ → ℝ), Filter.Tendsto τ Filter.atTop (nhds 0) ∧ ∀ (S : BoundingSieve) (L n 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 → ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N) ≤ τ L

A genuine uniform tail function for the actual normalized boundary-chain density at each terminal prime. The offset is the finite number of coarse steps, and the displayed envelope tends to zero independently of all sieve parameters.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_uniform_tail_lt (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (N : ℕ) (L : ℕ), ∀ (S : BoundingSieve) (n 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 → ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N) < ρ

Equivalently, after one uniform pair-depth cutoff, every finite remaining block of the actual normalized boundary-chain density is smaller than a prescribed error.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.normalizedBoundaryTail_mul_eulerProduct_eq_orderedMass {P : Finset ℕ} {q : ℕ} {f : ℕ → ℝ} (hq : q ∈ P) (hfactor : ∀ p ∈ P, 1 - f p ≠ 0) (A : ℝ) : f q / (1 - f q) * (A / ∏ p ∈ P with q < p, (1 - f p)) * ∏ p ∈ P, (1 - f p) = (f q * ∏ p ∈ P with p < q, (1 - f p)) * A

Multiplication by the complete Euler product cancels the normalized denominators above a distinguished prime. What remains is its density times the product of the factors at all earlier primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.nu_le_nu_div_one_sub_of_mem {S : BoundingSieve} {p : ℕ} (hp : p ∈ S.prodPrimes.primeFactors) : S.nu p ≤ S.nu p / (1 - S.nu p)

A sieve density is bounded by its normalized Euler increment.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_nu_mul_prod_one_sub_lt_le_one (S : BoundingSieve) : ∑ q ∈ S.prodPrimes.primeFactors, S.nu q * ∏ p ∈ S.prodPrimes.primeFactors with p < q, (1 - S.nu p) ≤ 1

The ordered masses left after exact Euler cancellation have total at most one. This is the finite telescoping identity behind the global Rosser tail.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChains_global_uniform_absolute_tail (K : ℝ) (hK : 1 ≤ K) : ∃ (N : ℕ) (τ : ℕ → ℝ), Filter.Tendsto τ Filter.atTop (nhds 0) ∧ (∀ (L : ℕ), 0 ≤ τ L) ∧ ∀ (S : BoundingSieve) (L n : ℕ) (z Δ s : ℝ), 2 ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → (∑ q ∈ S.prodPrimes.primeFactors, S.nu q / (1 - S.nu q) * ((∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N)) / ∏ p ∈ S.prodPrimes.primeFactors with q < p, (1 - S.nu p))) * ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p) ≤ τ L

After exact cancellation of the skipped Euler factors, the geometric reverse-pair estimate gives a uniform absolute tail for the complete outer-prime sum. Unlike a pointwise terminal-prime estimate, this bound is summable because the remaining ordered terminal masses telescope to at most one. The bound is absolute; it does not contain an additional full Euler-product factor.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_screened_upperRosserBoundaryMassAux_succ_le (k : ℕ) {c s a r w : ℝ} (hc : 0 < c) (hca : c ≤ a) (har : a ≤ r) (hr : r ≤ 1) (hw : 0 ≤ w) : (∫ (x : ℝ) in Set.Ioo c 1, x⁻¹ * if x < r + w then LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - r - x) a x else 0) ≤ (∫ (x : ℝ) in Set.Ioo a r, x⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - r - x) a x) + c⁻¹ * (c⁻¹ * c⁻¹) ^ (k + 1) * w

Removing a one-cell thickening from the inherited upper face costs at most its width times the uniform screened integrand bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_innerDarboux_succ_le_integral_add (k : ℕ) {s₀ s₁ c ε η : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 ≤ ε) (hη : 0 < η) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ (h j : Fin (m + 1)), upperRosserFixedDepthMeshLeft c m h ≤ upperRosserFixedDepthMeshRight c m j → ∑ i : Fin (m + 1), (if upperRosserFixedDepthMeshLeft c m i < upperRosserFixedDepthMeshRight c m j then LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - upperRosserFixedDepthMeshRight c m i) (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m i) + ε else 0) * (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i - 1) ≤ (∫ (x : ℝ) in Set.Ioo (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m j), x⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x) (upperRosserFixedDepthMeshLeft c m h) x) + (η + ε) / c + (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m / c ^ 2 + c⁻¹ * (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m

The fixed-depth inner Darboux sum is bounded by the exact inner integral in the Rosser recursion. The extra term is the cost of deleting the one-cell thickening used to absorb the ordered-prime boundary.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_innerIntegral_lower_le_add (k : ℕ) {s₀ s₁ c ε : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ (h j : Fin (m + 1)), ∀ a ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m h), ∫ (x : ℝ) in Set.Ioo (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m j), x⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x) (upperRosserFixedDepthMeshLeft c m h) x ≤ (∫ (x : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight c m j), x⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x) a x) + ε

On a sufficiently fine fixed mesh, the inner Rosser integral based at the cell's lower endpoint is uniformly approximated from above by the integral based at the true cutoff anywhere in that cell.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_innerDarboux_succ_le_trueIntegral_add (k : ℕ) {s₀ s₁ c ε η : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 ≤ ε) (hη : 0 < η) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ (h j : Fin (m + 1)), ∀ a ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m h), upperRosserFixedDepthMeshLeft c m h ≤ upperRosserFixedDepthMeshRight c m j → ∑ i : Fin (m + 1), (if upperRosserFixedDepthMeshLeft c m i < upperRosserFixedDepthMeshRight c m j then LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - upperRosserFixedDepthMeshRight c m i) (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m i) + ε else 0) * (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i - 1) ≤ (∫ (x : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight c m j), x⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x) a x) + η + (η + ε) / c + (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m / c ^ 2 + c⁻¹ * (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m

The positive-depth inner Darboux sum is bounded by the exact recursive integral at the true distinguished-prime cutoff. This simultaneously removes the ordered-prime screen thickening and the cellwise lower-cutoff displacement.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_correctedInnerDarboux_succ_le_trueIntegral_add (k : ℕ) {K s₀ s₁ c ε η ρ B : ℝ} (hK : 0 ≤ K) (hc : 0 < c) (hc1 : c < 1) (hε : 0 ≤ ε) (hη : 0 < η) (hρ : 0 < ρ) (hB : 0 ≤ B) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (z : ℝ), z₀ ≤ z → ∀ s ∈ Set.Icc s₀ s₁, ∀ (h j : Fin (m + 1)), ∀ a ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m h), upperRosserFixedDepthMeshLeft c m h ≤ upperRosserFixedDepthMeshRight c m j → (∀ (i : Fin (m + 1)), LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - upperRosserFixedDepthMeshRight c m i) (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m i) + ε ≤ B) → ∑ i : Fin (m + 1), (if upperRosserFixedDepthMeshLeft c m i < upperRosserFixedDepthMeshRight c m j then LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - upperRosserFixedDepthMeshRight c m i) (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m i) + ε else 0) * (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i * (1 + K / (upperRosserFixedDepthMeshLeft c m i * Real.log z)) - 1) ≤ (∫ (x : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight c m j), x⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x) a x) + η + (η + ε) / c + (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m / c ^ 2 + c⁻¹ * (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m + ρ

The inner successor estimate with its local-product correction included. The cutoff is uniform over the compact residual range and every distinguished prime in its mesh cell.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_outerDarboux_succ_le_integral_add (k : ℕ) {s₀ s₁ a ε : ℝ} (ha : 0 < a) (ha1 : a < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∑ j : Fin (m + 1), (∫ (x₁ : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight a m j), x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight a m j - x₁) a x₁) * (upperRosserFixedDepthMeshRight a m j / upperRosserFixedDepthMeshLeft a m j - 1) ≤ (∫ (x₀ : ℝ) in Set.Ioo a 1, x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁) + ε / a + a⁻¹ * (a⁻¹ * a⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth a m / a ^ 2

A sufficiently fine fixed mesh turns the exact positive-depth inner integrals at its right endpoints into an outer Darboux sum. The estimate is uniform over a compact interval of residual levels.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_outerDarboux_succ_movingLower_le_integral_add (k : ℕ) {s₀ s₁ c ε : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ a ∈ Set.Icc c 1, ∑ j : Fin (m + 1), (∫ (x₁ : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight c m j), x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x₁) a x₁) * (upperRosserFixedDepthMeshRight c m j / upperRosserFixedDepthMeshLeft c m j - 1) ≤ (∫ (x₀ : ℝ) in Set.Ioo c 1, x₀⁻¹ * ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁) + ε / c + c⁻¹ * (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m / c ^ 2

A fixed mesh based at a uniform support cutoff also controls inner Rosser integrals whose actual lower cutoff varies above it. The crossing cell is covered by the global outer-endpoint modulus.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_screenedOuterDarboux_succ_movingLower_le_integral_add (k : ℕ) {s₀ s₁ c ε : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ a ∈ Set.Icc c 1, ∀ (r w : ℝ), ∑ j : Fin (m + 1), (if upperRosserFixedDepthMeshRight c m j ≤ r + w then ∫ (x₁ : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight c m j), x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x₁) a x₁ else 0) * (upperRosserFixedDepthMeshRight c m j / upperRosserFixedDepthMeshLeft c m j - 1) ≤ (∫ (x₀ : ℝ) in Set.Ioo c 1, x₀⁻¹ * if x₀ < r + w then ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁ else 0) + ε / c + c⁻¹ * (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m / c ^ 2

A fixed mesh based at a uniform support cutoff controls the screened outer Rosser sum even when the true lower cutoff varies above the mesh base. Both the lower cutoff and the moving upper screen are retained for recursive use.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_screenedOuterDarboux_succ_le_integral_add (k : ℕ) {s₀ s₁ a ε : ℝ} (ha : 0 < a) (ha1 : a < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ (r w : ℝ), ∑ j : Fin (m + 1), (if upperRosserFixedDepthMeshRight a m j < r + w then ∫ (x₁ : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight a m j), x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight a m j - x₁) a x₁ else 0) * (upperRosserFixedDepthMeshRight a m j / upperRosserFixedDepthMeshLeft a m j - 1) ≤ (∫ (x₀ : ℝ) in Set.Ioo a 1, x₀⁻¹ * if x₀ < r + w then ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁ else 0) + ε / a + a⁻¹ * (a⁻¹ * a⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth a m / a ^ 2

The outer positive-depth Darboux estimate remains uniform after imposing a moving upper screen. Right-endpoint evaluation makes the discontinuity one-sided: an active mesh endpoint forces its whole open cell to be active.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_screened_outerRosserBoundaryMassAux_succ_le_massAux (k : ℕ) {s a b r w : ℝ} (ha : 0 < a) (har : a ≤ r) (hb1 : b ≤ 1) (hw : 0 ≤ w) (hr : r = min b (s / 3)) : (∫ (x₀ : ℝ) in Set.Ioo a 1, x₀⁻¹ * if x₀ < r + w then ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁ else 0) ≤ LinearSieve.upperRosserBoundaryMassAux (k + 2) s a b + (a⁻¹ * a⁻¹) ^ (k + 2) * w

Removing a one-cell thickening from an inherited moving outer Rosser face costs at most the mesh width times the uniform bound for the complete outer integrand. The endpoint b is retained for recursive applications.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_screened_outerRosserBoundaryMassAux_succ_le (k : ℕ) {s a r w : ℝ} (ha : 0 < a) (har : a ≤ r) (_hr1 : r ≤ 1) (hw : 0 ≤ w) (hr : r = min 1 (s / 3)) : (∫ (x₀ : ℝ) in Set.Ioo a 1, x₀⁻¹ * if x₀ < r + w then ∫ (x₁ : ℝ) in Set.Ioo a x₀, x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - x₀ - x₁) a x₁ else 0) ≤ LinearSieve.upperRosserBoundaryMassAux (k + 2) s a 1 + (a⁻¹ * a⁻¹) ^ (k + 2) * w

Removing the one-cell thickening from the global moving outer Rosser face costs at most the mesh width times the uniform bound for the complete outer integrand.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_screenedOuterDarboux_succ_movingLower_le_massAux_add (k : ℕ) {s₀ s₁ c ε : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, ∀ a ∈ Set.Icc c 1, ∀ b ≤ 1, a ≤ min b (s / 3) → ∑ j : Fin (m + 1), (if upperRosserFixedDepthMeshRight c m j ≤ min b (s / 3) + upperRosserFixedDepthMeshWidth c m then ∫ (x₁ : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight c m j), x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x₁) a x₁ else 0) * (upperRosserFixedDepthMeshRight c m j / upperRosserFixedDepthMeshLeft c m j - 1) ≤ LinearSieve.upperRosserBoundaryMassAux (k + 2) s a b + (a⁻¹ * a⁻¹) ^ (k + 2) * upperRosserFixedDepthMeshWidth c m + ε / c + c⁻¹ * (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m / c ^ 2

The moving-lower outer Darboux sum is bounded by the recursive Rosser mass with its inherited upper face. This is the induction-closed outer quadrature: the exact screen is min b (s / 3), while the mesh itself only uses the common positive support cutoff c.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_correctedScreenedOuterDarboux_succ_movingLower_le_massAux_add (k : ℕ) {K s₀ s₁ c ε ρ : ℝ} (hK : 0 ≤ K) (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) (hρ : 0 < ρ) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (z : ℝ), z₀ ≤ z → ∀ s ∈ Set.Icc s₀ s₁, ∀ a ∈ Set.Icc c 1, ∀ b ≤ 1, a ≤ min b (s / 3) → ∑ j : Fin (m + 1), (if upperRosserFixedDepthMeshRight c m j ≤ min b (s / 3) + upperRosserFixedDepthMeshWidth c m then ∫ (x₁ : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight c m j), x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x₁) a x₁ else 0) * (upperRosserFixedDepthMeshRight c m j / upperRosserFixedDepthMeshLeft c m j * (1 + K / (upperRosserFixedDepthMeshLeft c m j * Real.log z)) - 1) ≤ LinearSieve.upperRosserBoundaryMassAux (k + 2) s a b + (a⁻¹ * a⁻¹) ^ (k + 2) * upperRosserFixedDepthMeshWidth c m + ε / c + c⁻¹ * (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m / c ^ 2 + ρ

Corrected form of the induction-closed outer quadrature. The local-product correction is absorbed uniformly while both the true lower cutoff and inherited upper face remain variable.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_screenedOuterDarboux_succ_le_mass_add (k : ℕ) {s₀ s₁ a ε : ℝ} (ha : 0 < a) (ha1 : a < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc s₀ s₁, a ≤ min 1 (s / 3) → ∑ j : Fin (m + 1), (if upperRosserFixedDepthMeshRight a m j < min 1 (s / 3) + upperRosserFixedDepthMeshWidth a m then ∫ (x₁ : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight a m j), x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight a m j - x₁) a x₁ else 0) * (upperRosserFixedDepthMeshRight a m j / upperRosserFixedDepthMeshLeft a m j - 1) ≤ LinearSieve.upperRosserBoundaryMassAux (k + 2) s a 1 + (a⁻¹ * a⁻¹) ^ (k + 2) * upperRosserFixedDepthMeshWidth a m + ε / a + a⁻¹ * (a⁻¹ * a⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth a m / a ^ 2

The screened outer Darboux sum is bounded directly by the next continuous Rosser mass, with explicit losses for the one-cell moving-face thickening and for right-endpoint quadrature.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_correctedScreenedOuterDarboux_succ_le_mass_add (k : ℕ) {K s₀ s₁ a ε ρ : ℝ} (hK : 0 ≤ K) (ha : 0 < a) (ha1 : a < 1) (hε : 0 < ε) (hρ : 0 < ρ) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (z : ℝ), z₀ ≤ z → ∀ s ∈ Set.Icc s₀ s₁, a ≤ min 1 (s / 3) → ∑ j : Fin (m + 1), (if upperRosserFixedDepthMeshRight a m j < min 1 (s / 3) + upperRosserFixedDepthMeshWidth a m then ∫ (x₁ : ℝ) in Set.Ioo a (upperRosserFixedDepthMeshRight a m j), x₁⁻¹ * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight a m j - x₁) a x₁ else 0) * (upperRosserFixedDepthMeshRight a m j / upperRosserFixedDepthMeshLeft a m j * (1 + K / (upperRosserFixedDepthMeshLeft a m j * Real.log z)) - 1) ≤ LinearSieve.upperRosserBoundaryMassAux (k + 2) s a 1 + (a⁻¹ * a⁻¹) ^ (k + 2) * upperRosserFixedDepthMeshWidth a m + ε / a + a⁻¹ * (a⁻¹ * a⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth a m / a ^ 2 + ρ

The complete corrected outer mesh sum is bounded by the next continuous Rosser mass. Both the local-product correction and the moving-face cell are absorbed into explicit errors.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_nu_div_one_sub_mul_upperRosserBoundaryMassAux_zero_le_logKernel_add_screened (K ρ c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hc : 0 < c) (hc1 : c < 1) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z s x₀ a : ℝ) (T : Finset ℕ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → c ≤ a → x₀ ≤ 1 → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, a < Real.log ↑p / Real.log z ∧ Real.log ↑p / Real.log z < x₀) → ∑ p ∈ T, S.nu p / (1 - S.nu p) * LinearSieve.upperRosserBoundaryMassAux 0 (s - x₀ - Real.log ↑p / Real.log z) a (Real.log ↑p / Real.log z) ≤ LinearSieve.upperRosserBoundaryLogKernel s a x₀ + ρ

Uniform inner Stieltjes comparison for the terminal depth-zero residual. After the ordering constraints are imposed, its support is the single moving logarithmic interval defining upperRosserBoundaryLogKernel.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_nu_div_one_sub_mul_upperRosserBoundaryMassAux_zero_le_logKernel_add (K ρ : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z s x₀ a : ℝ) (T : Finset ℕ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → 1 / 6 ≤ a → x₀ ≤ 1 → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, a < Real.log ↑p / Real.log z ∧ Real.log ↑p / Real.log z < x₀) → ∑ p ∈ T, S.nu p / (1 - S.nu p) * LinearSieve.upperRosserBoundaryMassAux 0 (s - x₀ - Real.log ↑p / Real.log z) a (Real.log ↑p / Real.log z) ≤ LinearSieve.upperRosserBoundaryLogKernel s a x₀ + ρ

Compatibility specialization of the terminal inner comparison to the traditional one-sixth screen.