Upper Rosser boundary integrals and alternating pairs

Screened integrands, support restrictions, finite boundary factors, alternating-pair transforms, and summable prefix-volume majorants.

theorem MathlibNt.SieveTheory.LinearSieve.inv_sq_mul_upperRosserBoundaryMass_one_le {s a : ℝ} (ha : 1 / 6 ≤ a) : a⁻¹ * a⁻¹ * upperRosserBoundaryMass 1 s a ≤ 180 * Real.log 6

Uniform bound for the full screened depth-two outer integrand, including both reciprocal factors in the future outer a-integral.

theorem MathlibNt.SieveTheory.LinearSieve.abs_inv_sq_mul_upperRosserBoundaryMass_one_sub_le {s t a b : ℝ} (ha : 1 / 6 ≤ a) (hb : 1 / 6 ≤ b) : |a⁻¹ * a⁻¹ * upperRosserBoundaryMass 1 s a - b⁻¹ * b⁻¹ * upperRosserBoundaryMass 1 t b| ≤ 36 * ((36 + 2 * Real.log 6) * |s - t| + (144 + 6 * Real.log 6) * |a - b|) + 2160 * Real.log 6 * |a - b|

The complete depth-two outer density is jointly Lipschitz on the screened box. This is the uniform-continuity input for the final outer Darboux sum.

theorem MathlibNt.SieveTheory.LinearSieve.lipschitzOn_inv_sq_mul_upperRosserBoundaryMass_one (s : ℝ) : LipschitzOnWith ⟨36 * (144 + 6 * Real.log 6) + 2160 * Real.log 6, ⋯⟩ (fun (a : ℝ) => a⁻¹ * a⁻¹ * upperRosserBoundaryMass 1 s a) (Set.Ici (1 / 6))

For fixed s, the complete screened depth-two outer density is Lipschitz in the outer logarithmic coordinate.

theorem MathlibNt.SieveTheory.LinearSieve.integrableOn_inv_sq_mul_upperRosserBoundaryMass_one (s : ℝ) : MeasureTheory.IntegrableOn (fun (a : ℝ) => a⁻¹ * a⁻¹ * upperRosserBoundaryMass 1 s a) (Set.Ioo (1 / 6) 1) MeasureTheory.volume

The screened depth-two outer density is integrable. Together with integral_upperRosserBoundaryMass_one_eq_integral_one_sixth, this places the entire depth-two continuous contribution on a compact Lipschitz interval.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_eq_zero_of_terminal_le (k : ℕ) {s a b : ℝ} (hs : 0 ≤ s) (ha : a ≤ s / 3 ^ (k + 1)) : upperRosserBoundaryMassAux k s a b = 0

The recursive continuous mass has the same depth-dependent lower support as the exact Rosser region: at depth 2k it vanishes unless s / 3^(k+1) < a.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_ne_zero_terminal_lt (k : ℕ) {s a b : ℝ} (hs : 0 ≤ s) (h : upperRosserBoundaryMassAux k s a b ≠ 0) : s / 3 ^ (k + 1) < a

Nonvanishing of the depth-2k continuous residual forces its terminal coordinate past the exact recursive support threshold.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_ne_zero_outer_lower (k : ℕ) {s a x₀ x₁ : ℝ} (hs : 3 / 2 ≤ s) (hx₀ : x₀ ≤ s / 3) (hx₁ : x₁ < x₀) (h : upperRosserBoundaryMassAux k (s - x₀ - x₁) a x₁ ≠ 0) : 1 / (2 * 3 ^ (k + 1)) < a

After one Rosser pair has been peeled, every nonzero depth-2k residual has a terminal coordinate bounded below solely in terms of the original fundamental-lemma range and the remaining depth.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_succ_eq_zero_of_div_three_le (k : ℕ) {s a b : ℝ} (h : s / 3 ≤ a) : upperRosserBoundaryMassAux (k + 1) s a b = 0

A positive-depth boundary mass vanishes unless the terminal coordinate lies strictly below the cubic outer cutoff.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_succ_eq_zero_of_upper_le (k : ℕ) {s a b : ℝ} (h : b ≤ a) : upperRosserBoundaryMassAux (k + 1) s a b = 0

A positive-depth mass also vanishes when its inherited upper interval is empty.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMassAux_succ_ne_zero_support (k : ℕ) {s a b : ℝ} (h : upperRosserBoundaryMassAux (k + 1) s a b ≠ 0) : a < b ∧ a < s / 3

Nonzero positive-depth mass forces both geometric support inequalities for the first peeled coordinate.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass_succ_eq_zero_of_div_three_le (k : ℕ) {s a : ℝ} (h : s / 3 ≤ a) : upperRosserBoundaryMass (k + 1) s a = 0

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserBoundaryMass_eq_integral_support (k : ℕ) {s : ℝ} (hs : 0 ≤ s) : ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass k s a = ∫ (a : ℝ) in Set.Ioo (s / 3 ^ (k + 1)) 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass k s a

The outer boundary integral may be restricted to the exact lower support cutoff supplied by the recursive Rosser inequalities.

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserBoundaryMass_eq_integral_fixedDepthSupport (k : ℕ) {s : ℝ} (hs : 3 / 2 ≤ s) : ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass k s a = ∫ (a : ℝ) in Set.Ioo (1 / (2 * 3 ^ k)) 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass k s a

On the fundamental-lemma range, every fixed-depth outer boundary integral is supported in a compact interval bounded away from zero. The lower endpoint depends only on the depth, so this is the uniform domain for the fixed-depth Darboux induction.

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserBoundaryMass_one_eq_integral_one_sixth {s : ℝ} (hs : 3 / 2 ≤ s) : ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass 1 s a = ∫ (a : ℝ) in Set.Ioo (1 / 6) 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass 1 s a

On the upper-sieve range s ≥ 3/2, the complete depth-two outer integral is already supported in the common screened interval (1/6, 1).

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserBoundaryMass_eq_zero_of_pow_le (k : ℕ) {s : ℝ} (hs : 3 ^ (k + 1) ≤ s) : ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass k s a = 0

At depth 2k, the outer boundary contribution vanishes once the normalized level is at least 3^(k+1).

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserBoundaryMass_zero {s : ℝ} (hs : 0 < s) (hs3 : s < 3) : ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass 0 s a = 3 / s - 1

The first continuous boundary contribution is the reciprocal cubic-shell integral. This is the initial term of the finite Buchstab expansion.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserFiniteBoundaryFactor (L : ℕ) (s : ℝ) : ℝ

The finite continuous upper Rosser factor obtained by summing boundary depths below L and then integrating the distinguished outer coordinate.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserFiniteBoundaryFactor L s = 1 + ∑ k ∈ Finset.range L, ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryMass k s a

@[simp]

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserFiniteBoundaryFactor_zero (s : ℝ) : upperRosserFiniteBoundaryFactor 0 s = 1

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserFiniteBoundaryFactor_succ (L : ℕ) (s : ℝ) : upperRosserFiniteBoundaryFactor (L + 1) s = upperRosserFiniteBoundaryFactor L s + ∫ (a : ℝ) in Set.Ioo 0 1, a⁻¹ * a⁻¹ * upperRosserBoundaryMass L s a

Adding one admissible depth adds exactly its outer-coordinate boundary integral.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserFiniteBoundaryFactor_nonneg (L : ℕ) (s : ℝ) : 0 ≤ upperRosserFiniteBoundaryFactor L s

Every finite truncation of the continuous upper Rosser factor is nonnegative.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserFiniteBoundaryFactor_mono_succ (L : ℕ) (s : ℝ) : upperRosserFiniteBoundaryFactor L s ≤ upperRosserFiniteBoundaryFactor (L + 1) s

The finite continuous factors increase with the depth cutoff.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserFiniteBoundaryFactor_succ_eq_self_of_pow_le (L : ℕ) {s : ℝ} (hs : 3 ^ (L + 1) ≤ s) : upperRosserFiniteBoundaryFactor (L + 1) s = upperRosserFiniteBoundaryFactor L s

A depth contributes nothing to the finite factor once its geometric support cutoff lies beyond the normalized sieve level.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserFiniteBoundaryFactor_one {s : ℝ} (hs : 0 < s) (hs3 : s < 3) : upperRosserFiniteBoundaryFactor 1 s = 3 / s

The first finite Buchstab truncation is 3 / s on the nonempty range of the cubic shell.

theorem MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegion.even_coordinate_lt_suffix_add_terminal {s a : ℝ} {x : List ℝ} (hregion : UpperRosserLogRegion s a x) {i : ℕ} (hi : i < x.length) (heven : Even i) : 2 * x[i] < (List.drop (i + 1) x).sum + 3 * a

Combining an even Rosser prefix inequality with the terminal boundary inequality gives a constraint from that coordinate towards the remaining suffix. Unlike the unrestricted factorial estimate, this retains every alternating-prefix condition.

theorem MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegion.last_pair_lt_terminal {s a : ℝ} {x : List ℝ} {k : ℕ} (hregion : UpperRosserLogRegion s a x) (hlen : x.length = 2 * (k + 1)) : 2 * x[2 * k] < x[2 * k + 1] + 3 * a

At the innermost pair of a nonempty even Rosser chain, the larger coordinate is less than half the smaller coordinate plus the terminal budget.

theorem MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegionBelow.last_pair_ratios_mem {s a b : ℝ} {x : List ℝ} {k : ℕ} (hregion : UpperRosserLogRegionBelow s a b x) (hlen : x.length = 2 * (k + 1)) (ha : 0 < a) : x[2 * k + 1] / a ∈ Set.Ioo 1 3 ∧ x[2 * k] / a ∈ Set.Ioo (x[2 * k + 1] / a) ((x[2 * k + 1] / a + 3) / 2)

After division by the terminal coordinate, the innermost Rosser pair lies in the scale-free triangular region 1 < y < 3, y < x < (y + 3) / 2. This is the first cell of the reverse-chain geometric contraction below.

theorem MathlibNt.SieveTheory.LinearSieve.sum_add_geometric_le_of_sortedGT_even_prefix {s : ℝ} {x : List ℝ} {k : ℕ} (hs : 0 ≤ s) (hlen : x.length = 2 * k) (hsorted : x.SortedGT) (hprefix : ∀ (i : ℕ) (hi : i < x.length), Even i → (List.take i x).sum + 3 * x[i] ≤ s) : x.sum + s / 3 ^ k ≤ s

Alternating cubic-prefix inequalities contract the unused logarithmic budget by a factor of three after each pair of decreasing coordinates.

theorem MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegion.sum_add_geometric_le {s a : ℝ} {x : List ℝ} {k : ℕ} (hregion : UpperRosserLogRegion s a x) (hs : 0 ≤ s) (hlen : x.length = 2 * k) : x.sum + s / 3 ^ k ≤ s

A depth-2k upper Rosser region leaves at least s / 3^k of the logarithmic budget unused by its selected coordinates.

theorem MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegion.outer_lower {s a : ℝ} {x : List ℝ} {k : ℕ} (hregion : UpperRosserLogRegion s a x) (hs : 0 ≤ s) (hlen : x.length = 2 * k) : s / 3 ^ (k + 1) < a

The terminal boundary coordinate of a depth-2k Rosser region stays uniformly away from zero.

theorem MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegion.outer_lower_of_three_halves_le {s a : ℝ} {x : List ℝ} {k : ℕ} (hregion : UpperRosserLogRegion s a x) (hs : 3 / 2 ≤ s) (hlen : x.length = 2 * k) : 1 / (2 * 3 ^ k) < a

On the fundamental-lemma range, the depth-2k outer coordinate is bounded below by a constant depending only on the fixed depth.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairTransform (F : ℝ → ℝ) (r : ℝ) : ℝ

The reverse-chain integral operator obtained by adjoining one ordered pair. Here r is the suffix-plus-terminal budget divided by the current terminal coordinate, y is the smaller new coordinate, and x the larger one. The upper face 2x < y + r is exactly an even-prefix Rosser inequality.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairTransform F r = ∫ (y : ℝ) in Set.Ioo 1 r, y⁻¹ * ∫ (x : ℝ) in Set.Ioo y ((y + r) / 2), x⁻¹ * F ((r + y + x) / x)

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairNormalizedKernel (r y x : ℝ) : ℝ

The quadratic reverse-pair kernel normalized by the current state.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairNormalizedKernel r y x = ((r + y + x) / x) ^ 2 / r ^ 2

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairNormalizedKernel_nonneg (r y x : ℝ) : 0 ≤ upperRosserAlternatingPairNormalizedKernel r y x

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairNormalizedKernel_le_sq {r y x R : ℝ} (hr : 3 ≤ r) (hR : 3 ≤ R) (hx : x ∈ Set.Icc 1 R) (hy : y ∈ Set.Icc 1 R) : upperRosserAlternatingPairNormalizedKernel r y x ≤ R ^ 2

On a fixed ratio window, the normalized reverse-pair kernel has a bound independent of the current state.

theorem MathlibNt.SieveTheory.LinearSieve.abs_upperRosserAlternatingPairNormalizedKernel_sub_le {r y u v R : ℝ} (hr : 3 ≤ r) (hR : 3 ≤ R) (hu : u ∈ Set.Icc 1 R) (hv : v ∈ Set.Icc 1 R) (hy : y ∈ Set.Icc 1 R) : |upperRosserAlternatingPairNormalizedKernel r y u - upperRosserAlternatingPairNormalizedKernel r y v| ≤ 3 * R ^ 2 * |u - v|

The normalized reverse-pair kernel is uniformly Lipschitz in its larger coordinate on a fixed ratio window.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPair_nextRatio_gt_three {r y x : ℝ} (hy : y ∈ Set.Ioo 1 r) (hx : x ∈ Set.Ioo y ((y + r) / 2)) : 3 < (r + y + x) / x

The reverse-chain state remains in the invariant range r > 3 after one pair is adjoined.

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserAlternatingPair_quadratic_inner {r y : ℝ} (hy : 0 < y) (hyr : y ≤ r) : ∫ (x : ℝ) in Set.Ioo y ((y + r) / 2), x⁻¹ * ((r + y + x) / x) ^ 2 = r ^ 2 / (2 * y ^ 2) + 3 * r / y - 7 / 2 + Real.log ((y + r) / (2 * y))

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairTransform_const_mul (c r : ℝ) (F : ℝ → ℝ) : upperRosserAlternatingPairTransform (fun (t : ℝ) => c * F t) r = c * upperRosserAlternatingPairTransform F r

The reverse-pair operator is linear in a constant coefficient.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairTransform_quadratic_le {r : ℝ} (hr : 3 ≤ r) : upperRosserAlternatingPairTransform (fun (t : ℝ) => t ^ 2) r ≤ 4 / 5 * r ^ 2

One reverse Rosser pair contracts the quadratic suffix envelope by a fixed factor. The estimate is genuinely geometric: its triangular integration face is 2x < y + r, the inequality contributed by the corresponding even prefix.

theorem MathlibNt.SieveTheory.LinearSieve.integral_upperRosserAlternatingPairNormalizedKernel_le {r : ℝ} (hr : 3 ≤ r) : ∫ (y : ℝ) in Set.Ioo 1 r, y⁻¹ * ∫ (x : ℝ) in Set.Ioo y ((y + r) / 2), x⁻¹ * upperRosserAlternatingPairNormalizedKernel r y x ≤ 4 / 5

The normalized quadratic kernel has total reverse-pair mass at most 4 / 5. This is the scale-free form used in the discrete contraction argument.

theorem MathlibNt.SieveTheory.LinearSieve.stronglyMeasurable_upperRosserAlternatingPair_inner (F : ℝ → ℝ) (hF : MeasureTheory.StronglyMeasurable F) (r : ℝ) : MeasureTheory.StronglyMeasurable fun (y : ℝ) => ∫ (x : ℝ) in Set.Ioo y ((y + r) / 2), x⁻¹ * F ((r + y + x) / x)

Measurability of the inner integral in the reverse-pair operator.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairTransform_le_const_mul_quadratic (F : ℝ → ℝ) {C r : ℝ} (hr : 3 ≤ r) (hFmeas : MeasureTheory.StronglyMeasurable F) (hFnonneg : ∀ (t : ℝ), 3 ≤ t → 0 ≤ F t) (hFle : ∀ (t : ℝ), 3 ≤ t → F t ≤ C * t ^ 2) : upperRosserAlternatingPairTransform F r ≤ upperRosserAlternatingPairTransform (fun (t : ℝ) => C * t ^ 2) r

Monotonicity of one reverse-pair step against a quadratic envelope. The hypotheses are pointwise only on the invariant range t ≥ 3; measurability is enough to recover all required integrability from the quadratic majorant.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPrefixMajorant (k : ℕ) (r : ℝ) : ℝ

The explicit geometric envelope for k reverse Rosser pairs.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPrefixMajorant k r = (4 / 5) ^ k * r ^ 2

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairTransform_majorant_le (k : ℕ) {r : ℝ} (hr : 3 ≤ r) : upperRosserAlternatingPairTransform (upperRosserAlternatingPrefixMajorant k) r ≤ upperRosserAlternatingPrefixMajorant (k + 1) r

Applying one constrained reverse-pair integral to the depth-k envelope lands below the depth-k+1 envelope.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPrefixVolume : ℕ → ℝ → ℝ

Scale-free volume of k reverse-built Rosser pairs. Starting from terminal state r = 3, each recursion imposes decreasing order and the next even-prefix constraint instead of integrating over all unordered coordinates.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPrefixVolume 0 x✝ = 1
• MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPrefixVolume k.succ x✝ = MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPairTransform (MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPrefixVolume k) x✝

theorem MathlibNt.SieveTheory.LinearSieve.stronglyMeasurable_upperRosserAlternatingPrefixVolume (k : ℕ) : MeasureTheory.StronglyMeasurable (upperRosserAlternatingPrefixVolume k)

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPrefixVolume_nonneg (k : ℕ) {r : ℝ} (hr : 3 ≤ r) : 0 ≤ upperRosserAlternatingPrefixVolume k r

The constrained reverse-chain volume is nonnegative throughout its invariant range.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAlternatingPrefixVolume_le_majorant (k : ℕ) {r : ℝ} (hr : 3 ≤ r) : upperRosserAlternatingPrefixVolume k r ≤ upperRosserAlternatingPrefixMajorant k r

Every constrained reverse-chain volume is bounded by the explicit geometric envelope.

theorem MathlibNt.SieveTheory.LinearSieve.summable_upperRosserAlternatingPrefixMajorant_three : Summable fun (k : ℕ) => upperRosserAlternatingPrefixMajorant k 3

At the terminal state r = 3, the constrained reverse-chain envelopes form a summable geometric series.

theorem MathlibNt.SieveTheory.LinearSieve.summable_upperRosserAlternatingPrefixVolume_three : Summable fun (k : ℕ) => upperRosserAlternatingPrefixVolume k 3

The actual constrained reverse-chain volumes are summable at the terminal state because they are termwise dominated by the geometric envelope.

theorem MathlibNt.SieveTheory.LinearSieve.tsum_upperRosserAlternatingPrefixMajorant_three_natAdd (L : ℕ) : ∑' (j : ℕ), upperRosserAlternatingPrefixMajorant (L + j) 3 = 45 * (4 / 5) ^ L

Exact tail sum of the scale-free alternating-prefix majorant.

theorem MathlibNt.SieveTheory.LinearSieve.sum_range_upperRosserAlternatingPrefixMajorant_three_natAdd_le (L n : ℕ) : ∑ j ∈ Finset.range n, upperRosserAlternatingPrefixMajorant (L + j) 3 ≤ 45 * (4 / 5) ^ L

Every finite aggregate beyond depth L is bounded by the same explicit geometric tail, independently of its terminal depth.

theorem MathlibNt.SieveTheory.LinearSieve.sum_range_upperRosserAlternatingPrefixVolume_three_natAdd_le (L n : ℕ) : ∑ j ∈ Finset.range n, upperRosserAlternatingPrefixVolume (L + j) 3 ≤ 45 * (4 / 5) ^ L

The volume of any finite block of constrained depths beyond L is at most the explicit geometric tail 45 (4/5)^L.

theorem MathlibNt.SieveTheory.LinearSieve.exists_sum_range_upperRosserAlternatingPrefixMajorant_three_natAdd_lt {ρ : ℝ} (hρ : 0 < ρ) : ∃ (L : ℕ), ∀ (n : ℕ), ∑ j ∈ Finset.range n, upperRosserAlternatingPrefixMajorant (L + j) 3 < ρ

The aggregate alternating-prefix majorant has a uniform tail cutoff.

theorem MathlibNt.SieveTheory.LinearSieve.exists_sum_range_upperRosserAlternatingPrefixVolume_three_natAdd_lt {ρ : ℝ} (hρ : 0 < ρ) : ∃ (L : ℕ), ∀ (n : ℕ), ∑ j ∈ Finset.range n, upperRosserAlternatingPrefixVolume (L + j) 3 < ρ

Consequently, one depth cutoff makes every finite tail of the constrained reverse-chain volumes smaller than a prescribed positive error.