Weighted aggregate tail for the upper Rosser boundary

The production prefix carries the normalized outer atom S.nu q / (1 - S.nu q). Keeping this atom and restoring the complete Euler product cancels the terminal-dependent suffix denominator. The remaining ordered terminal masses telescope to at most one, so no terminal cardinality appears.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChains_weightedAggregate_geometric (K : ℝ) (hK : 1 ≤ K) : ∃ (N : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (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.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N)) * ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p) ≤ 90 * C * (9 / 10) ^ L

Literal geometric form of the weighted aggregate tail. The constants are selected before every sieve and source parameter. This is the form intended to compose with a fixed-depth prefix producer.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChains_weightedSubaggregate_geometric (K : ℝ) (hK : 1 ≤ K) : ∃ (N : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (S : BoundingSieve) (T : Finset ℕ) (L n : ℕ) (z Δ s : ℝ), T ⊆ S.prodPrimes.primeFactors → 2 ≤ z → 0 < Δ → s = Real.log Δ / Real.log z → HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → (∑ q ∈ T, S.nu q / (1 - S.nu q) * ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N)) * ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p) ≤ 90 * C * (9 / 10) ^ L

Geometric weighted tail on any terminal subcarrier, with no cardinality factor. Taking T to be a filtered terminal lane gives the exact aggregate replacement for the old pointwise-then-cardinality estimate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosserBoundaryChains_weightedAggregate_uniform_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.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N)) * ∏ p ∈ S.prodPrimes.primeFactors, (1 - S.nu p) ≤ τ L

The existing ordered-mass telescoping estimate, rewritten in the literal fixed-depth prefix coordinates: normalized outer atom times relative boundary density. The cutoff N and tail τ are selected before the sieve, depth block, and source parameters.

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

The same weighted tail over an arbitrary terminal subcarrier. In particular this applies directly to either side of the square-root terminal split. It is strictly stronger than paying card T * τ L: after Euler restoration the bound is just τ L, independently of T.card.