Screened Darboux comparisons for peeled prime pairs

Common fixed-depth meshes compare discrete peeled-pair sums with designated corner Darboux sums and continuous inner integrals, uniformly on positive screens.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_sum_pair_mul_upperRosserBoundaryMassAux_succ_le_meshCorners_add (k : ℕ) {s₀ s₁ c ε : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ {S : BoundingSieve} {K z s a : ℝ} {D : ℕ} {P : Finset ℕ} (h : Fin (m + 1)) (cell : ℕ → Fin (m + 1)), s ∈ Set.Icc s₀ s₁ → a ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m h) → HasDimensionOneLocalProductBound S K → 1 < z → 2 ≤ z ^ c → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, ↑p ≤ z) → (∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) → (∀ p ∈ P, Real.log ↑p / Real.log z ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m (cell p)) (upperRosserFixedDepthMeshRight c m (cell p))) → ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < D, S.nu p₀ / (1 - S.nu p₀) * (S.nu p₁ / (1 - S.nu p₁)) * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) a (Real.log ↑p₁ / Real.log z) ≤ ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < D, S.nu p₀ / (1 - S.nu p₀) * (S.nu p₁ / (1 - S.nu p₁)) * LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m (cell p₀) - upperRosserFixedDepthMeshRight c m (cell p₁)) (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m (cell p₁)) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

A common fixed-depth mesh turns every finite peeled-pair sum into its designated-corner Darboux sum. The continuity loss is paid once through the two-prime mass bound, rather than once for each pair of primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthDensity_succ_le_residualBoundaryMassAux_add_screened (k : ℕ) {S : BoundingSieve} {K z c c₀ Δ s ε s₁ : ℝ} {q : ℕ} {P : Finset ℕ} (hcomparison : UpperRosserBoundaryScreenedResidualComparison S z q k ε c₀ s₁) (hlocal : HasDimensionOneLocalProductBound S K) (hz : 1 < z) (hc1 : c ≤ 1) (hzc : 2 ≤ z ^ c) (hε : 0 ≤ ε) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hsUpper : s ≤ s₁) (hqprime : Nat.Prime q) (hqs : q ∉ P) (hP : P ⊆ S.prodPrimes.primeFactors) (hqmin : ∀ p ∈ P, q ≤ p) (hcut : ∀ p ∈ P, ↑p ≤ z) (hscreen : ∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) (hqscreen : c₀ ≤ Real.log ↑q / Real.log z) : LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 1) ≤ ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1, S.nu p₀ / (1 - S.nu p₀) * (S.nu p₁ / (1 - S.nu p₁)) * LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

Exact pair-recursion bound for a fixed distinguished prime, conditional on a residual comparison that preserves ambient support and the inherited upper face. This does not prove the residual comparison at successor depth: it substitutes the comparison after each peeled pair and explicitly aggregates its uniform pointwise error through the two prime sums.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthDensity_succ_le_residualBoundaryMassAux_add (k : ℕ) {S : BoundingSieve} {K z c Δ s ε : ℝ} {q : ℕ} {P : Finset ℕ} (hcomparison : UpperRosserBoundaryResidualComparison S z q k ε) (hlocal : HasDimensionOneLocalProductBound S K) (hz : 1 < z) (hc1 : c ≤ 1) (hzc : 2 ≤ z ^ c) (hε : 0 ≤ ε) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hqprime : Nat.Prime q) (hqs : q ∉ P) (hP : P ⊆ S.prodPrimes.primeFactors) (hqmin : ∀ p ∈ P, q ≤ p) (hcut : ∀ p ∈ P, ↑p ≤ z) (hscreen : ∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) : LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 1) ≤ ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1, S.nu p₀ / (1 - S.nu p₀) * (S.nu p₁ / (1 - S.nu p₁)) * LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

Exact pair-recursion bound with an unrestricted residual comparison. This is the compatibility form of the theorem; the screened induction uses upperRosserBoundaryChainsFixedDepthDensity_succ_le_residualBoundaryMassAux_add_screened.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_succ_le_innerPartition_add_screened (k : ℕ) (ι : Type u_1) [Fintype ι] [DecidableEq ι] (K ρ B c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s ε c₀ s₁ : ℝ) (q : ℕ) (P : Finset ℕ) (cell : ℕ → ℕ → ι) (u v : ι → ℝ) (M : ℕ → ι → ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → s ≤ s₁ → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, ↑p ≤ z) → c ≤ 1 → 2 ≤ z ^ c → 0 ≤ ε → (∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) → c₀ ≤ Real.log ↑q / Real.log z → UpperRosserBoundaryScreenedResidualComparison S z q k ε c₀ s₁ → (∀ (i : ι), c ≤ u i) → (∀ (i : ι), u i ≤ v i) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, z ^ u (cell p₀ p₁) ≤ ↑p₁ ∧ ↑p₁ ≤ z ^ v (cell p₀ p₁)) → (∀ p₀ ∈ P, ∀ (i : ι), 0 ≤ M p₀ i) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ M p₀ (cell p₀ p₁)) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ B) → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 1) ≤ ∑ p₀ ∈ P, S.nu p₀ / (1 - S.nu p₀) * ∑ i : ι, M p₀ i * (v i / u i * (1 + K / (u i * Real.log z)) - 1) + ρ * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

The first (inner-prime) Stieltjes stage of the fixed-depth Rosser successor. A finite upper Darboux majorant for the actual residual mass turns the exact two-prime recursion into a sum over the remaining outer prime. The closed-cell loss is summed once against the positive-screen prime-mass bound, while the residual-comparison error retains its quadratic mass bound. Thus only the outer Stieltjes stage and the construction of these finite majorants remain at arbitrary depth.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_succ_le_innerPartition_add (k : ℕ) (ι : Type u_1) [Fintype ι] [DecidableEq ι] (K ρ B c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s ε : ℝ) (q : ℕ) (P : Finset ℕ) (cell : ℕ → ℕ → ι) (u v : ι → ℝ) (M : ℕ → ι → ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, ↑p ≤ z) → c ≤ 1 → 2 ≤ z ^ c → 0 ≤ ε → (∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) → UpperRosserBoundaryResidualComparison S z q k ε → (∀ (i : ι), c ≤ u i) → (∀ (i : ι), u i ≤ v i) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, z ^ u (cell p₀ p₁) ≤ ↑p₁ ∧ ↑p₁ ≤ z ^ v (cell p₀ p₁)) → (∀ p₀ ∈ P, ∀ (i : ι), 0 ≤ M p₀ i) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ M p₀ (cell p₀ p₁)) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ B) → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 1) ≤ ∑ p₀ ∈ P, S.nu p₀ / (1 - S.nu p₀) * ∑ i : ι, M p₀ i * (v i / u i * (1 + K / (u i * Real.log z)) - 1) + ρ * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

The unrestricted compatibility form of the inner-partition successor.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_succ_le_twoPartitions_add_screened (k : ℕ) (ι : Type u_1) (κ : Type u_2) [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (K ρ BInner BOuter c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hBInner : 0 ≤ BInner) (hBOuter : 0 ≤ BOuter) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s ε c₀ s₁ : ℝ) (q : ℕ) (P : Finset ℕ) (innerCell : ℕ → ℕ → ι) (innerLeft innerRight : ι → ℝ) (innerMajorant : ℕ → ι → ℝ) (outerCell : ℕ → κ) (outerLeft outerRight outerMajorant : κ → ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → s ≤ s₁ → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, ↑p ≤ z) → c ≤ 1 → 2 ≤ z ^ c → 0 ≤ ε → (∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) → c₀ ≤ Real.log ↑q / Real.log z → UpperRosserBoundaryScreenedResidualComparison S z q k ε c₀ s₁ → (∀ (i : ι), c ≤ innerLeft i) → (∀ (i : ι), innerLeft i ≤ innerRight i) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, z ^ innerLeft (innerCell p₀ p₁) ≤ ↑p₁ ∧ ↑p₁ ≤ z ^ innerRight (innerCell p₀ p₁)) → (∀ p₀ ∈ P, ∀ (i : ι), 0 ≤ innerMajorant p₀ i) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ innerMajorant p₀ (innerCell p₀ p₁)) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ BInner) → (∀ (j : κ), c ≤ outerLeft j) → (∀ (j : κ), outerLeft j ≤ outerRight j) → (∀ p₀ ∈ P, z ^ outerLeft (outerCell p₀) ≤ ↑p₀ ∧ ↑p₀ ≤ z ^ outerRight (outerCell p₀)) → (∀ (j : κ), 0 ≤ outerMajorant j) → (∀ p₀ ∈ P, 0 ≤ ∑ i : ι, innerMajorant p₀ i * (innerRight i / innerLeft i * (1 + K / (innerLeft i * Real.log z)) - 1) ∧ ∑ i : ι, innerMajorant p₀ i * (innerRight i / innerLeft i * (1 + K / (innerLeft i * Real.log z)) - 1) ≤ outerMajorant (outerCell p₀)) → (∀ p₀ ∈ P, ∑ i : ι, innerMajorant p₀ i * (innerRight i / innerLeft i * (1 + K / (innerLeft i * Real.log z)) - 1) ≤ BOuter) → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 1) ≤ ∑ j : κ, outerMajorant j * (outerRight j / outerLeft j * (1 + K / (outerLeft j * Real.log z)) - 1) + ρ + ρ * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

The complete two-prime Stieltjes stage of the fixed-depth Rosser successor. Finite Darboux majorants for the residual mass and for the resulting inner upper sum reduce the discrete successor density to one outer logarithmic Darboux sum. All local-product, closed-face, and residual-induction errors remain explicit.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_succ_le_twoPartitions_add (k : ℕ) (ι : Type u_1) (κ : Type u_2) [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (K ρ BInner BOuter c : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hBInner : 0 ≤ BInner) (hBOuter : 0 ≤ BOuter) (hc : 0 < c) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s ε : ℝ) (q : ℕ) (P : Finset ℕ) (innerCell : ℕ → ℕ → ι) (innerLeft innerRight : ι → ℝ) (innerMajorant : ℕ → ι → ℝ) (outerCell : ℕ → κ) (outerLeft outerRight outerMajorant : κ → ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, ↑p ≤ z) → c ≤ 1 → 2 ≤ z ^ c → 0 ≤ ε → (∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) → UpperRosserBoundaryResidualComparison S z q k ε → (∀ (i : ι), c ≤ innerLeft i) → (∀ (i : ι), innerLeft i ≤ innerRight i) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, z ^ innerLeft (innerCell p₀ p₁) ≤ ↑p₁ ∧ ↑p₁ ≤ z ^ innerRight (innerCell p₀ p₁)) → (∀ p₀ ∈ P, ∀ (i : ι), 0 ≤ innerMajorant p₀ i) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ innerMajorant p₀ (innerCell p₀ p₁)) → (∀ p₀ ∈ P, ∀ p₁ ∈ {p₁ ∈ P | p₁ < p₀ ∧ p₀ ^ 3 < ⌊Δ⌋₊ + 1}, LinearSieve.upperRosserBoundaryMassAux k (s - Real.log ↑p₀ / Real.log z - Real.log ↑p₁ / Real.log z) (Real.log ↑q / Real.log z) (Real.log ↑p₁ / Real.log z) ≤ BInner) → (∀ (j : κ), c ≤ outerLeft j) → (∀ (j : κ), outerLeft j ≤ outerRight j) → (∀ p₀ ∈ P, z ^ outerLeft (outerCell p₀) ≤ ↑p₀ ∧ ↑p₀ ≤ z ^ outerRight (outerCell p₀)) → (∀ (j : κ), 0 ≤ outerMajorant j) → (∀ p₀ ∈ P, 0 ≤ ∑ i : ι, innerMajorant p₀ i * (innerRight i / innerLeft i * (1 + K / (innerLeft i * Real.log z)) - 1) ∧ ∑ i : ι, innerMajorant p₀ i * (innerRight i / innerLeft i * (1 + K / (innerLeft i * Real.log z)) - 1) ≤ outerMajorant (outerCell p₀)) → (∀ p₀ ∈ P, ∑ i : ι, innerMajorant p₀ i * (innerRight i / innerLeft i * (1 + K / (innerLeft i * Real.log z)) - 1) ≤ BOuter) → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 1) ≤ ∑ j : κ, outerMajorant j * (outerRight j / outerLeft j * (1 + K / (outerLeft j * Real.log z)) - 1) + ρ + ρ * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

The unrestricted compatibility form of the two-partition successor.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_succ_le_fixedDepthMesh_add_screened (k : ℕ) {s₀ s₁ c ε ρ BInner BOuter : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) (hρ : 0 < ρ) (hBInner : 0 ≤ BInner) (hBOuter : 0 ≤ BOuter) : ∃ (N : ℕ), ∀ (K : ℝ), 1 ≤ K → ∀ (m : ℕ), N ≤ m → ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s c₀ : ℝ) (q : ℕ) (P : Finset ℕ) (h : Fin (m + 1)) (M : Fin (m + 1) → ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → s ∈ Set.Icc s₀ s₁ → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, ↑p ≤ z) → 2 ≤ z ^ c → (∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) → c₀ ≤ Real.log ↑q / Real.log z → UpperRosserBoundaryScreenedResidualComparison S z q (k + 1) ε c₀ s₁ → Real.log ↑q / Real.log z ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m h) → (∀ p ∈ P, Real.log ↑p / Real.log z ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m (upperRosserFixedDepthMeshCell c m (Real.log ↑p / Real.log z))) (upperRosserFixedDepthMeshRight c m (upperRosserFixedDepthMeshCell c m (Real.log ↑p / Real.log z)))) → (∀ (i j : Fin (m + 1)), LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - upperRosserFixedDepthMeshRight c m i) (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m i) + ε ≤ BInner) → (∀ (i : Fin (m + 1)), 0 ≤ M i) → (∀ p₀ ∈ P, ∑ i : Fin (m + 1), (if upperRosserFixedDepthMeshLeft c m i < upperRosserFixedDepthMeshRight c m (upperRosserFixedDepthMeshCell c m (Real.log ↑p₀ / Real.log z)) then LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m (upperRosserFixedDepthMeshCell c m (Real.log ↑p₀ / Real.log z)) - 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) ≤ M (upperRosserFixedDepthMeshCell c m (Real.log ↑p₀ / Real.log z))) → (∀ p ∈ P, M (upperRosserFixedDepthMeshCell c m (Real.log ↑p / Real.log z)) ≤ BOuter) → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 2) ≤ ∑ i : Fin (m + 1), M i * (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i * (1 + K / (upperRosserFixedDepthMeshLeft c m i * Real.log z)) - 1) + ρ + ρ * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

The two-prime Stieltjes successor on a fixed logarithmic mesh. The inner corner majorants are the recursive continuous boundary masses themselves; the remaining outer majorant is therefore a finite Darboux upper sum for those explicit corner values.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChainsFixedDepthDensity_succ_le_fixedDepthMesh_add (k : ℕ) {s₀ s₁ c ε ρ BInner BOuter : ℝ} (hc : 0 < c) (hc1 : c < 1) (hε : 0 < ε) (hρ : 0 < ρ) (hBInner : 0 ≤ BInner) (hBOuter : 0 ≤ BOuter) : ∃ (N : ℕ), ∀ (K : ℝ), 1 ≤ K → ∀ (m : ℕ), N ≤ m → ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z Δ s : ℝ) (q : ℕ) (P : Finset ℕ) (h : Fin (m + 1)) (M : Fin (m + 1) → ℝ), z₀ ≤ z → 0 < Δ → HasDimensionOneLocalProductBound S K → s = Real.log Δ / Real.log z → s ∈ Set.Icc s₀ s₁ → Nat.Prime q → q ∉ P → P ⊆ S.prodPrimes.primeFactors → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, ↑p ≤ z) → 2 ≤ z ^ c → (∀ p ∈ P, c ≤ Real.log ↑p / Real.log z) → UpperRosserBoundaryResidualComparison S z q (k + 1) ε → Real.log ↑q / Real.log z ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m h) → (∀ p ∈ P, Real.log ↑p / Real.log z ∈ Set.Icc (upperRosserFixedDepthMeshLeft c m (upperRosserFixedDepthMeshCell c m (Real.log ↑p / Real.log z))) (upperRosserFixedDepthMeshRight c m (upperRosserFixedDepthMeshCell c m (Real.log ↑p / Real.log z)))) → (∀ (i j : Fin (m + 1)), LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - upperRosserFixedDepthMeshRight c m i) (upperRosserFixedDepthMeshLeft c m h) (upperRosserFixedDepthMeshRight c m i) + ε ≤ BInner) → (∀ (i : Fin (m + 1)), 0 ≤ M i) → (∀ p₀ ∈ P, ∑ i : Fin (m + 1), (if upperRosserFixedDepthMeshLeft c m i < upperRosserFixedDepthMeshRight c m (upperRosserFixedDepthMeshCell c m (Real.log ↑p₀ / Real.log z)) then LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m (upperRosserFixedDepthMeshCell c m (Real.log ↑p₀ / Real.log z)) - 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) ≤ M (upperRosserFixedDepthMeshCell c m (Real.log ↑p₀ / Real.log z))) → (∀ p ∈ P, M (upperRosserFixedDepthMeshCell c m (Real.log ↑p / Real.log z)) ≤ BOuter) → LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P (k + 2) ≤ ∑ i : Fin (m + 1), M i * (upperRosserFixedDepthMeshRight c m i / upperRosserFixedDepthMeshLeft c m i * (1 + K / (upperRosserFixedDepthMeshLeft c m i * Real.log z)) - 1) + ρ + ρ * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) + ε * (Real.log (z + 1) / Real.log (z ^ c) * (1 + K / Real.log (z ^ c)) - 1) ^ 2

The unrestricted compatibility form of the fixed-mesh successor.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserFixedDepthMesh_screenedInnerDarboux_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)), ∑ 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 c 1, x⁻¹ * if x < upperRosserFixedDepthMeshRight c m j + upperRosserFixedDepthMeshWidth c m then LinearSieve.upperRosserBoundaryMassAux (k + 1) (s - upperRosserFixedDepthMeshRight c m j - x) (upperRosserFixedDepthMeshLeft c m h) x else 0) + (η + ε) / c + (c⁻¹ * c⁻¹) ^ (k + 1) * upperRosserFixedDepthMeshWidth c m / c ^ 2

On a sufficiently fine fixed-depth mesh, the explicitly screened inner corner sum is a Darboux upper sum for the continuous residual mass. The screen extends the triangular face by one mesh width, so every cell which can contain an ordered inner prime is retained.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_upperRosserDepthTwoMesh (m : ℕ) (K ρ B : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (T : Finset ℕ) (w : ℕ → ℝ) (M : Fin (m + 1) → ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc (1 / 6) 1) → (∀ (i : Fin (m + 1)), 0 ≤ M i) → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M (upperRosserDepthTwoMeshCell m (Real.log ↑p / Real.log z))) → (∀ p ∈ T, w p ≤ B) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ ∑ i : Fin (m + 1), M i * (upperRosserDepthTwoMeshRight m i / upperRosserDepthTwoMeshLeft m i * (1 + K / (upperRosserDepthTwoMeshLeft m i * Real.log z)) - 1) + ρ

Uniform weighted Stieltjes comparison on the fixed screened mesh. The cutoff absorbs all closed right-face atoms at once; its dependence is only on the mesh, the local-product constant, the weight bound, and the requested error.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_upperRosserDepthTwoMeshMain (m : ℕ) (K ρ B : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (T : Finset ℕ) (w : ℕ → ℝ) (M : Fin (m + 1) → ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc (1 / 6) 1) → (∀ (i : Fin (m + 1)), 0 ≤ M i ∧ M i ≤ B) → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ M (upperRosserDepthTwoMeshCell m (Real.log ↑p / Real.log z))) → (∀ p ∈ T, w p ≤ B) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ ∑ i : Fin (m + 1), M i * (upperRosserDepthTwoMeshRight m i / upperRosserDepthTwoMeshLeft m i - 1) + ρ

The same fixed-mesh comparison with both the closed-face loss and every K / log z correction absorbed into one prescribed error. Its main term is the genuine logarithmic Darboux sum Mᵢ (vᵢ / uᵢ - 1).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_integral_add_of_depthTwoMesh (m : ℕ) (K ρ B L : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hL : 0 ≤ L) (hmesh : (12 * L + 36 * B) * upperRosserDepthTwoMeshWidth m ≤ ρ / 2) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (T : Finset ℕ) (w : ℕ → ℝ) (f : ℝ → ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc (1 / 6) 1) → (∀ x ∈ Set.Icc (1 / 6) 1, 0 ≤ f x) → (∀ x ∈ Set.Icc (1 / 6) 1, f x ≤ B) → (∀ x ∈ Set.Icc (1 / 6) 1, ∀ y ∈ Set.Icc (1 / 6) 1, |f x - f y| ≤ L * |x - y|) → MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo (1 / 6) 1) MeasureTheory.volume → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ f (Real.log ↑p / Real.log z)) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ (∫ (x : ℝ) in Set.Ioo (1 / 6) 1, x⁻¹ * f x) + ρ

A fixed screened mesh compares every uniformly bounded Lipschitz prime weight with its logarithmic integral. All dimension-one product errors and closed right-face atoms are absorbed in the cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_weighted_sum_nu_div_one_sub_le_integral_add (K ρ B L : ℝ) (hK : 1 ≤ K) (hρ : 0 < ρ) (hB : 0 ≤ B) (hL : 0 ≤ L) : ∃ (z₀ : ℝ), 2 ≤ z₀ ∧ ∀ (S : BoundingSieve) (z : ℝ) (T : Finset ℕ) (w : ℕ → ℝ) (f : ℝ → ℝ), z₀ ≤ z → HasDimensionOneLocalProductBound S K → T ⊆ S.prodPrimes.primeFactors → (∀ p ∈ T, Real.log ↑p / Real.log z ∈ Set.Icc (1 / 6) 1) → (∀ x ∈ Set.Icc (1 / 6) 1, 0 ≤ f x) → (∀ x ∈ Set.Icc (1 / 6) 1, f x ≤ B) → (∀ x ∈ Set.Icc (1 / 6) 1, ∀ y ∈ Set.Icc (1 / 6) 1, |f x - f y| ≤ L * |x - y|) → MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ * f x) (Set.Ioo (1 / 6) 1) MeasureTheory.volume → (∀ p ∈ T, 0 ≤ w p ∧ w p ≤ f (Real.log ↑p / Real.log z)) → ∑ p ∈ T, w p * (S.nu p / (1 - S.nu p)) ≤ (∫ (x : ℝ) in Set.Ioo (1 / 6) 1, x⁻¹ * f x) + ρ

Uniform screened Stieltjes comparison for bounded nonnegative Lipschitz weights. The mesh and the local-product cutoff depend only on the displayed uniform constants and the requested error.