Honest terminal split for the upper Rosser carrier tail

The terminal carrier is split once, before any estimate is applied. On the large-terminal lane, sqrt (z + 1) ≤ q + 1 gives the initialization power bound with exponent 2. On the complementary lane we sum the already proved absolute discrete-tail estimate, retaining the exact cardinality payment.

The small-terminal scale conversion is proved below rather than postulated. Its fixed-depth proof expands each boundary path exactly, retains the inverse Euler product over omitted primes, and pays that product by the dimension-one local product estimate. The resulting common factor is log (z+1) / log (Q+1) * (1 + K / log (Q+1)); hence the final aggregate keeps both this z,Q growth and the exact filtered-terminal cardinality. No continuous tail estimate or carrier-uniform absorption is asserted.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.add_one_le_sq_of_sqrt_le_nat_add_one {z : ℝ} {q : ℕ} (hz : 0 ≤ z + 1) (hq : √(z + 1) ≤ ↑q + 1) : z + 1 ≤ (↑q + 1) ^ 2

The square-root terminal cutoff gives the exponent-two initialization bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.sum_terminal_sqrt_split (P : Finset ℕ) (z : ℝ) (f : ℕ → ℝ) : ∑ q ∈ P, f q = ∑ q ∈ P with √(z + 1) ≤ ↑q + 1, f q + ∑ q ∈ P with ¬√(z + 1) ≤ ↑q + 1, f q

Exact carrier partition. This identity is the bookkeeping boundary used below; estimates are applied only after this split.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosser_largeTerminal_relativeBlock_sum_le_card (K : ℝ) (hK : 1 ≤ K) : ∃ (Q : ℝ), 2 ≤ Q ∧ ∀ (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 ∈ {q ∈ S.prodPrimes.primeFactors | √(z + 1) ≤ ↑q + 1}, Q ≤ ↑q) → ∑ q ∈ S.prodPrimes.primeFactors with √(z + 1) ≤ ↑q + 1, ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j) ≤ ↑{q ∈ S.prodPrimes.primeFactors | √(z + 1) ≤ ↑q + 1}.card * (180 * (101 / 100) * (9 / 10) ^ L)

Aggregate large-terminal relative block estimate. The power-bound theorem is invoked inside one Finset.sum_le_sum, and the common geometric envelope is then counted exactly by the filtered carrier cardinality.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosser_smallTerminal_absoluteBlock_sum_le_card_mul_tail (K : ℝ) (hK : 1 ≤ K) : ∃ (N : ℕ) (τ : ℕ → ℝ), Filter.Tendsto τ Filter.atTop (nhds 0) ∧ ∀ (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 with ¬√(z + 1) ≤ ↑q + 1, ∑ 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) ≤ ↑{q ∈ S.prodPrimes.primeFactors | ¬√(z + 1) ≤ ↑q + 1}.card * τ L

The complementary small-terminal lane is controlled by the existing absolute discrete tail. Summing is done before simplification, so the cost is exactly card small * τ L, not an untracked per-terminal error.

def MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserSmallTerminalAggregateConversion (B : ℝ) (S : BoundingSieve) (L n N : ℕ) (z Δ : ℝ) : Prop

The remaining scale-conversion interface after the honest split: an aggregate conversion on the small-terminal lane from the proved absolute density to the relative Euler-product scale. It is intentionally not stated pointwise in q; the separate filtered-cardinality payment remains explicit in the assembly theorem.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.UpperRosserSmallTerminalAggregateConversion B S L n N z Δ = (∑ q ∈ S.prodPrimes.primeFactors with ¬√(z + 1) ≤ ↑q + 1, ∑ j ∈ Finset.range n, MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N) ≤ B * ∑ q ∈ S.prodPrimes.primeFactors with ¬√(z + 1) ≤ ↑q + 1, ∑ j ∈ Finset.range n, MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N))

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserTerminalEulerConversionFactor (K z Q : ℝ) : ℝ

The exact Euler-product payment available once every terminal is at least Q. Its growth in z is retained: for fixed Q this is of order log z, so it is not a carrier-uniform constant.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserTerminalEulerConversionFactor K z Q = Real.log (z + 1) / Real.log (Q + 1) * (1 + K / Real.log (Q + 1))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserBoundaryChainsFixedDepthRelativeDensity_le_eulerConversionFactor {S : BoundingSieve} {K z Q : ℝ} {D q k : ℕ} (hQ : 2 ≤ Q) (hQq : Q ≤ ↑q) (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hq : q ∈ S.prodPrimes.primeFactors) : LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) D q ({p ∈ S.prodPrimes.primeFactors | q < p}) k ≤ upperRosserTerminalEulerConversionFactor K z Q * LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (fun (p : ℕ) => S.nu p / (1 - S.nu p)) D q ({p ∈ S.prodPrimes.primeFactors | q < p}) k

Fixed-depth conversion from the absolute density with normalized atoms ν(p)/(1-ν(p)) to the relative density. The proof expands each boundary path exactly: selected primes become normalized atoms, while the genuinely omitted primes retain their inverse Euler factors. The dimension-one product estimate then pays that whole omitted product once at the common terminal floor Q.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserSmallTerminalAggregateConversion_of_terminalFloor {K Q : ℝ} (hQ : 2 ≤ Q) {S : BoundingSieve} {L n N : ℕ} {z Δ : ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) (hQsmall : ∀ q ∈ {q ∈ S.prodPrimes.primeFactors | ¬√(z + 1) ≤ ↑q + 1}, Q ≤ ↑q) : UpperRosserSmallTerminalAggregateConversion (upperRosserTerminalEulerConversionFactor K z Q) S L n N z Δ

Genuine aggregate producer for the frozen small-terminal conversion interface. Unlike a postulated uniform B, the factor keeps the initialization Euler denominator visible through B(z,Q). The square-root condition identifies the lane but is not used to erase this growth.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosserSmallTerminalAggregateConversion_two {K : ℝ} {S : BoundingSieve} {L n N : ℕ} {z Δ : ℝ} (hlocal : HasDimensionOneLocalProductBound S K) (hcut : ∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) : UpperRosserSmallTerminalAggregateConversion (upperRosserTerminalEulerConversionFactor K z 2) S L n N z Δ

Every terminal in the prime carrier is at least two. Consequently the small-terminal aggregate always has the explicit factor B(z,2), with no extra terminal-floor premise.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.upperRosser_terminalSplit_unifiedRelativeCarrierTail {B : ℝ} (hB : 0 ≤ B) {S : BoundingSieve} {L n N : ℕ} {z Δ τ : ℝ} (hlarge : ∑ q ∈ S.prodPrimes.primeFactors with √(z + 1) ≤ ↑q + 1, ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N) ≤ ↑{q ∈ S.prodPrimes.primeFactors | √(z + 1) ≤ ↑q + 1}.card * (180 * (101 / 100) * (9 / 10) ^ (L + N))) (hsmallAbs : ∑ q ∈ S.prodPrimes.primeFactors with ¬√(z + 1) ≤ ↑q + 1, ∑ 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) ≤ ↑{q ∈ S.prodPrimes.primeFactors | ¬√(z + 1) ≤ ↑q + 1}.card * τ) (hconvert : UpperRosserSmallTerminalAggregateConversion B S L n N z Δ) : ∑ q ∈ S.prodPrimes.primeFactors, ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N) ≤ ↑{q ∈ S.prodPrimes.primeFactors | √(z + 1) ≤ ↑q + 1}.card * (180 * (101 / 100) * (9 / 10) ^ (L + N)) + B * (↑{q ∈ S.prodPrimes.primeFactors | ¬√(z + 1) ≤ ↑q + 1}.card * τ)

Conditional unified relative carrier-tail inequality. The proof first rewrites the whole carrier sum by the exact terminal partition, then inserts the aggregate large- and small-lane bounds. The scale mismatch is isolated in UpperRosserSmallTerminalAggregateConversion; the cardinality factors are not silently discarded.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.exists_upperRosser_terminalSplit_relativeCarrierTail_explicit (K : ℝ) (hK : 1 ≤ K) : ∃ (Q : ℝ) (N : ℕ) (τ : ℕ → ℝ), 2 ≤ Q ∧ Filter.Tendsto τ Filter.atTop (nhds 0) ∧ ∀ (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 ∈ {q ∈ S.prodPrimes.primeFactors | √(z + 1) ≤ ↑q + 1}, Q ≤ ↑q) → ∑ q ∈ S.prodPrimes.primeFactors, ∑ j ∈ Finset.range n, LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (⇑S.nu) (⌊Δ⌋₊ + 1) q ({p ∈ S.prodPrimes.primeFactors | q < p}) (L + j + N) ≤ ↑{q ∈ S.prodPrimes.primeFactors | √(z + 1) ≤ ↑q + 1}.card * (180 * (101 / 100) * (9 / 10) ^ (L + N)) + upperRosserTerminalEulerConversionFactor K z 2 * (↑{q ∈ S.prodPrimes.primeFactors | ¬√(z + 1) ≤ ↑q + 1}.card * τ L)

Strongest unconditional terminal-split consumer currently available. The small lane is geometric in L, but its exact coefficient is

B(z,2) * card(small terminals).

Thus the Euler denominator and terminal cardinality are both paid explicitly; this statement deliberately does not promote the result to a cutoff uniform in the varying sieve and endpoint.