Residual boundary comparisons and support screens #
Recursive residual-comparison predicates, ceil-division identities, and lower logarithmic screens reduce boundary densities to continuous residual masses. Partition faces and paired residual errors retain quantitative bounds.
All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.
A pointwise comparison interface for a residual upper Rosser chain inside a fixed bounding sieve. Besides the altered real level, it retains both invariants created by pair removal: the residual carrier stays in the ambient prime carrier and all of its logarithmic coordinates lie strictly below the inherited upper endpoint.
Equations
- MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserBoundaryResidualComparison S z q k ε = ∀ ⦃Δ s b : ℝ⦄ ⦃P : Finset ℕ⦄, 1 < Δ → s = Real.log Δ / Real.log z → P ⊆ S.prodPrimes.primeFactors → q ∉ P → Nat.Prime q → (∀ p ∈ P, Nat.Prime p) → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, Real.log ↑p / Real.log z < b) → MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P k ≤ MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux k s (Real.log ↑q / Real.log z) b + ε
Instances For
The residual comparison restricted to the screen and bounded level range
that are preserved by pair removal. Unlike
UpperRosserBoundaryResidualComparison, this is closed under the fixed-depth
induction: a residual level is positive and no larger than its parent level,
while its inherited upper face remains at most one.
Equations
- MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserBoundaryScreenedResidualComparison S z q k ε c s₁ = ∀ ⦃Δ s b : ℝ⦄ ⦃P : Finset ℕ⦄, 1 < Δ → s = Real.log Δ / Real.log z → s ≤ s₁ → P ⊆ S.prodPrimes.primeFactors → q ∉ P → Nat.Prime q → (∀ p ∈ P, Nat.Prime p) → (∀ p ∈ P, q ≤ p) → (∀ p ∈ P, Real.log ↑p / Real.log z < b) → c ≤ Real.log ↑q / Real.log z → b ≤ 1 → MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q P k ≤ MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux k s (Real.log ↑q / Real.log z) b + ε
Instances For
A global residual comparison restricts to every screened bounded range.
Increasing the lower-screen requirement only restricts the instances of a screened residual comparison.
The residual comparison interface holds at depth zero with no error, for every altered real level and every ambiently supported carrier below its inherited upper endpoint.
The exact depth-zero comparison is induction-ready on every bounded screened range.
The outer prime exposed by one Buchstab pair lies in the exact inherited
screen. The cubic Rosser condition gives the closed s / 3 face, while the
residual carrier gives the strict inherited face b.
A residual comparison can be instantiated at the exact altered level left
by peeling two primes. The ceiling-divided level and residual coordinate agree
after the elementary logarithm identities; ambient support is inherited, and
the strict carrier bound p < p₁ supplies the logarithmic upper face.
A screened bounded residual comparison applies after peeling an admissible prime pair. The residual level decreases, and the second prime supplies an inherited face at most one whenever it lies below the ambient cutoff.
After peeling the first two selected primes, the ceiling-divided discrete depth-zero mass is bounded by the continuous mass at the exact residual logarithmic parameter. In particular, there is no rounding loss in the residual Rosser level.
Pointwise depth-one Buchstab majorant. Peeling the unique prime pair and using the exact depth-zero shell comparison leaves precisely the residual continuous indicator, with no local-product or rounding error.
The pointwise depth-one majorant can be restricted to the exact inherited
outer screen. The upper endpoint is closed because the cubic condition only
implies x₀ ≤ s / 3; primes on that face must not be discarded.
The lower support exposed after peeling a Rosser pair is uniform at every fixed residual depth. The inherited upper bound is retained in the residual mass, while the lower bound depends only on that depth.
Every nonzero term in the continuous depth-zero majorant left after peeling
the first Rosser pair has its distinguished-prime coordinate above 1 / 6.
Unlike fixed-chain support, this applies after the discrete residual has already
been enlarged to the continuous indicator.
The recursive support screen gives a uniform bound for every residual mass at a fixed depth. This supplies the boundedness input for finite Darboux majorants independently of the sieve and of all prime coordinates.
All three exposed logarithmic coordinates of a nonzero fixed-depth residual lie above the same depth-dependent screen.
A nonzero residual after the first Rosser pair confines all three prime
coordinates away from zero. The distinguished-prime inequality is the recursive
cubic support; the other two follow from the ordering above q. This supplies a
common lower cutoff for every depth-two logarithmic mesh.
The complete discrete depth-two contribution is bounded by the two peeled prime sums weighted by the continuous residual depth-zero mass. This is the exact finite majorant to which the two logarithmic partition estimates are applied.
Induction step for a fixed-depth boundary comparison. After screening the
distinguished prime at the exact depth-dependent support, any pointwise
majorant for the residual depth lifts through the exact two-prime recursion.
The function E records the residual induction error without hiding how it is
weighted by the two newly peeled coordinates.
Error-free specialization of the fixed-depth recursion lift. It isolates
the exact induction obligation: dominate every inherited residual carrier by
upperRosserBoundaryMassAux k with its actual upper endpoint.
The exact depth-two residual majorant may be restricted to the compact
box where all three logarithmic coordinates exceed 1 / 6. This is the
screened finite sum to which the nested Darboux partitions are applied.
One logarithmic cell of the inner p₁-sum in the depth-two residual
majorant. The residual depth-zero mass is an indicator and hence is bounded by
one. A possible prime on the closed right face is retained and paid for by the
fixed-depth atom bound η.
Partitioned form of the inner p₁ residual estimate. It is the finite
upper Darboux sum used for the inner integral in
upperRosserBoundaryMass 1; every closed cell contributes its local-product
increment and one fixed-depth atom error.
Partitioned inner residual estimate with one global budget for every closed
right-face atom. Since the depth-zero residual mass is an indicator, the
weighted endpoint contribution is bounded by the unweighted normalized atom
mass appearing in hatom.
The union of all closed right faces of a logarithmic partition contains at most one natural number for each cell. This is the combinatorial reason that endpoint errors cost the size of the fixed mesh, rather than the number of primes being sieved.
A pointwise atom bound yields one global budget for all right faces of a fixed logarithmic partition. In particular, the loss is controlled by the number of cells and is independent of the number of primes in the sieve.
For a fixed logarithmic mesh, all closed-face atoms are uniformly negligible under the dimension-one local-product hypothesis. The cutoff is independent of the sieve, the partition assignment, and the face locations.
Uniform weighted Stieltjes comparison on an arbitrary fixed positive
logarithmic screen and an arbitrary finite closed partition. This is the
depth-independent form of the screened comparison: the lower screen c, the
cell geometry, and the weight majorants are all parameters.
The normalized prime mass above a fixed positive logarithmic screen is bounded by one dimension-one local-product interval.
A uniform pointwise residual error remains quantitative after both peeled prime sums. On a fixed positive logarithmic screen it costs at most the square of the one-dimensional normalized prime mass bound.