Finite upper Rosser density and certificates

Logarithmic realization of discrete chains, fixed-depth density recursions, Euler-normalized boundary identities, and upper weight certificates.

theorem MathlibNt.SieveTheory.LinearSieve.UpperRosserBoundaryChain.logarithmicCoordinates_mem {z Δ s : ℝ} {q : ℕ} {l : List ℕ} (hz : 1 < z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hq : 0 < q) (hl : ∀ p ∈ l, 0 < p) (hchain : UpperRosserBoundaryChain (⌊Δ⌋₊ + 1) q l) : UpperRosserLogRegion s (Real.log ↑q / Real.log z) (logarithmicCoordinates z l)

A discrete Rosser boundary chain lies in its exact logarithmic-coordinate region. The floor in the natural level weakens strict prefix inequalities to closed faces, while making the terminal shell strict.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensitySum (nu : ℕ → ℝ) (D : ℕ) (P : Finset ℕ) : ℝ

The finite upper Rosser density sum over subsets of a prescribed prime set.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensitySum nu D P = ∑ s ∈ P.powerset, MathlibNt.SieveTheory.LinearSieve.upperRosserSetWeight D s * ∏ p ∈ s, nu p

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensitySum_empty (nu : ℕ → ℝ) {D : ℕ} (hD : 1 < D) : upperRosserSetDensitySum nu D ∅ = 1

Initial value for the finite upper Rosser density recursion.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensitySum_insert (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) (hq : q ∉ P) : upperRosserSetDensitySum nu D (insert q P) = ∑ s ∈ P.powerset, (upperRosserSetWeight D s + nu q * upperRosserSetWeight D (insert q s)) * ∏ p ∈ s, nu p

Exact one-prime recursion for the finite upper Rosser density sum. It is the finite combinatorial form of the Buchstab decomposition: subsets not containing q and subsets containing q are paired over P.powerset.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensitySum_min_recursion (nu : ℕ → ℝ) (D : ℕ) {P : Finset ℕ} (hP : P.Nonempty) : upperRosserSetDensitySum nu D P = ∑ s ∈ (P.erase (P.min' hP)).powerset, (upperRosserSetWeight D s + nu (P.min' hP) * upperRosserSetWeight D (insert (P.min' hP) s)) * ∏ p ∈ s, nu p

Cardinality-decreasing form of the finite Buchstab recursion, obtained by peeling off the least prime in a nonempty finite set.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosser_insert_min_active_iff_cube_lt {D q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ s, q ≤ p) (heven : Even s.card) (hs : s.prod id < D ∧ UpperRosserAdmissibleSet D s) : (insert q s).prod id < D ∧ UpperRosserAdmissibleSet D (insert q s) ↔ s.prod id * q ^ 3 < D

For an active even set, adjoining a new least prime remains active exactly until the cubic Rosser cutoff q ^ 3 * ∏ s < D is crossed.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySet_iff_cube_le {D q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ s, q ≤ p) : UpperRosserBoundarySet D q s ↔ Even s.card ∧ s.prod id < D ∧ UpperRosserAdmissibleSet D s ∧ D ≤ s.prod id * q ^ 3

The abstract even Rosser boundary is exactly the cubic shell D ≤ q ^ 3 * ∏ s once q is the new least prime.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySet_iff_sorted_chain {D q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ s, q ≤ p) : UpperRosserBoundarySet D q s ↔ UpperRosserBoundaryChain D q (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)

A boundary subset is equivalently its canonical decreasing Rosser chain. The statement retains all alternating-prefix inequalities, rather than incorrectly truncating boundary tails to cardinality zero or two.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChains (D q : ℕ) (P : Finset ℕ) : Finset (List ℕ)

Canonical decreasing-list representatives of all boundary subsets of P. Unlike a powerset, this carrier exposes the chain length and indexed prefixes used by the Buchstab iteration.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChains D q P = Finset.image (fun (s : Finset ℕ) => s.sort fun (x1 x2 : ℕ) => x1 ≥ x2) (Finset.filter (MathlibNt.SieveTheory.LinearSieve.UpperRosserBoundarySet D q) P.powerset)

theorem MathlibNt.SieveTheory.LinearSieve.mem_upperRosserBoundaryChains_iff {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ P, q ≤ p) {l : List ℕ} : l ∈ upperRosserBoundaryChains D q P ↔ l.Nodup ∧ l.SortedGT ∧ l.toFinset ⊆ P ∧ UpperRosserBoundaryChain D q l

Membership in the canonical boundary-chain carrier is exactly strict decrease, containment in P, and the explicit arbitrary-depth Rosser region.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) (k : ℕ) : ℝ

The selected density mass of upper Rosser boundary chains of exact length 2k. This is the discrete quantity compared depth-by-depth with upperRosserBoundaryMassAux.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity nu D q P k = ∑ l ∈ MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChains D q P with l.length = 2 * k, (List.map nu l).prod

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) (k : ℕ) : ℝ

The exact fixed-depth boundary density on the relative Euler-product scale. Keeping the quotient intact is essential in the depth tail: replacing its denominator by a pointwise local-product majorant loses the full sieve-product factor required by the fundamental lemma.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q P k = MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity nu D q P k / ∏ p ∈ P, (1 - nu p)

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryRelativePairTransition (nu : ℕ → ℝ) (P : Finset ℕ) (p₀ p₁ : ℕ) : ℝ

The exact relative weight for peeling the two largest selected primes. The quotient of Euler products retains all primes skipped before the residual carrier p < p₁; no local-product estimate has yet been applied.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryRelativePairTransition nu P p₀ p₁ = (nu p₀ * nu p₁ * ∏ p ∈ P with p < p₁, (1 - nu p)) / ∏ p ∈ P, (1 - nu p)

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryRelativePairTransition_mul_eulerProduct (nu : ℕ → ℝ) {P : Finset ℕ} {p₀ p₁ : ℕ} (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserBoundaryRelativePairTransition nu P p₀ p₁ * ∏ p ∈ P, (1 - nu p) = nu p₀ * nu p₁ * ∏ p ∈ P with p < p₁, (1 - nu p)

Restoring the ambient Euler product cancels a relative pair transition exactly, leaving the selected pair and the residual Euler product.

theorem MathlibNt.SieveTheory.LinearSieve.mem_upperRosserBoundaryChains_fixedDepth_succ_iff {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hprime : ∀ p ∈ P, Nat.Prime p) (hqmin : ∀ p ∈ P, q ≤ p) {l : List ℕ} (k : ℕ) : l ∈ {l ∈ upperRosserBoundaryChains D q P | l.length = 2 * (k + 1)} ↔ ∃ p₀ ∈ P, ∃ p₁ ∈ P, p₁ < p₀ ∧ p₀ ^ 3 < D ∧ ∃ (xs : List ℕ), l = p₀ :: p₁ :: xs ∧ xs ∈ {xs ∈ upperRosserBoundaryChains (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ P | p < p₁}) | xs.length = 2 * k}

Exact carrier recursion for positive-depth upper Rosser boundary chains. The first two entries determine a residual chain at the ceiling-divided level, with its ambient primes restricted below the second entry.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity_succ (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hprime : ∀ p ∈ P, Nat.Prime p) (hqmin : ∀ p ∈ P, q ≤ p) (k : ℕ) : upperRosserBoundaryChainsFixedDepthDensity nu D q P (k + 1) = ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < D, nu p₀ * nu p₁ * upperRosserBoundaryChainsFixedDepthDensity nu (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ P | p < p₁}) k

Exact finite Buchstab recursion for the selected density mass. A positive depth peels the two largest selected primes and leaves the same boundary mass at the ceiling-divided level, with all remaining primes below the second one.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity_succ (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hprime : ∀ p ∈ P, Nat.Prime p) (hqmin : ∀ p ∈ P, q ≤ p) (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) (k : ℕ) : upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q P (k + 1) = ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < D, upperRosserBoundaryRelativePairTransition nu P p₀ p₁ * upperRosserBoundaryChainsFixedDepthRelativeDensity nu (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ P | p < p₁}) k

Exact finite Buchstab--Rosser recursion on the relative Euler-product scale. The transition keeps the quotient between the residual and ambient Euler products, and therefore retains every skipped-prime inverse factor.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryRelativePairTransition_nonneg (nu : ℕ → ℝ) {P : Finset ℕ} {p₀ p₁ : ℕ} (hp₀ : p₀ ∈ P) (hp₁ : p₁ ∈ P) (hnu : ∀ p ∈ P, 0 ≤ nu p) (hnuOne : ∀ p ∈ P, nu p ≤ 1) : 0 ≤ upperRosserBoundaryRelativePairTransition nu P p₀ p₁

Relative pair transitions are nonnegative under the natural local-density bounds.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity_succ_le (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hprime : ∀ p ∈ P, Nat.Prime p) (hqmin : ∀ p ∈ P, q ≤ p) (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) (hnu : ∀ p ∈ P, 0 ≤ nu p) (hnuOne : ∀ p ∈ P, nu p ≤ 1) (F : ℕ → ℕ → ℝ) (k : ℕ) (hF : ∀ p₀ ∈ P, ∀ p₁ ∈ P, p₁ < p₀ → p₀ ^ 3 < D → upperRosserBoundaryChainsFixedDepthRelativeDensity nu (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ P | p < p₁}) k ≤ F p₀ p₁) : upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q P (k + 1) ≤ ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < D, upperRosserBoundaryRelativePairTransition nu P p₀ p₁ * F p₀ p₁

Monotone interface for the relative Buchstab--Rosser recursion. Any majorant for the residual relative state propagates through the exact, nonnegative skipped-prime transitions.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity_succ_le (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hprime : ∀ p ∈ P, Nat.Prime p) (hqmin : ∀ p ∈ P, q ≤ p) (hnu : ∀ p ∈ P, 0 ≤ nu p) (F : ℕ → ℕ → ℝ) (k : ℕ) (hF : ∀ p₀ ∈ P, ∀ p₁ ∈ P, p₁ < p₀ → p₀ ^ 3 < D → upperRosserBoundaryChainsFixedDepthDensity nu (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ P | p < p₁}) k ≤ F p₀ p₁) : upperRosserBoundaryChainsFixedDepthDensity nu D q P (k + 1) ≤ ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ ^ 3 < D, nu p₀ * nu p₁ * F p₀ p₁

Monotone form of the finite Buchstab recursion. This is the induction interface for replacing every residual discrete mass by a continuous majorant.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity_zero (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hD : 1 < D) (hqs : q ∉ P) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ P, q ≤ p) : upperRosserBoundaryChainsFixedDepthDensity nu D q P 0 = if D ≤ q ^ 3 then 1 else 0

The depth-zero discrete boundary mass is exactly the terminal cubic shell.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity_zero (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hD : 1 < D) (hqs : q ∉ P) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ P, q ≤ p) : upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q P 0 = if D ≤ q ^ 3 then (∏ p ∈ P, (1 - nu p))⁻¹ else 0

At depth zero the relative density is exactly the terminal shell times the inverse ambient Euler product.

theorem MathlibNt.SieveTheory.LinearSieve.sum_mul_upperRosserBoundaryChainsFixedDepthDensity_zero (nu w : ℕ → ℝ) {D : ℕ} {P : Finset ℕ} (hD : 1 < D) (hprime : ∀ p ∈ P, Nat.Prime p) : ∑ q ∈ P, w q * upperRosserBoundaryChainsFixedDepthDensity nu D q ({p ∈ P | q < p}) 0 = ∑ q ∈ P with D ≤ q ^ 3, w q

Summing the depth-zero boundary density over the distinguished prime collapses exactly to the terminal cubic shell.

theorem MathlibNt.SieveTheory.LinearSieve.sum_mul_upperRosserBoundaryChainsFixedDepthDensity_succ (nu w : ℕ → ℝ) {D : ℕ} {P : Finset ℕ} (hprime : ∀ p ∈ P, Nat.Prime p) (k : ℕ) : ∑ q ∈ P, w q * upperRosserBoundaryChainsFixedDepthDensity nu D q ({p ∈ P | q < p}) (k + 1) = ∑ q ∈ P, w q * ∑ p₀ ∈ P with q < p₀, ∑ p₁ ∈ {p ∈ P | q < p} with p₁ < p₀ ∧ p₀ ^ 3 < D, nu p₀ * nu p₁ * upperRosserBoundaryChainsFixedDepthDensity nu (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ {p ∈ P | q < p} | p < p₁}) k

Exact outer form of the finite Buchstab recursion. It simultaneously peels the distinguished prime and the first pair of every positive-depth boundary chain, leaving a residual depth-2k density at the ceiling-divided level.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity_zero_le_boundaryMassAux (nu : ℕ → ℝ) {z Δ s a b : ℝ} {q D : ℕ} {P : Finset ℕ} (hz : 1 < z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (ha : a = Real.log ↑q / Real.log z) (hsnonneg : 0 ≤ s) (hD : D = ⌊Δ⌋₊ + 1) (hDlarge : 1 < D) (hqs : q ∉ P) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ P, q ≤ p) : upperRosserBoundaryChainsFixedDepthDensity nu D q P 0 ≤ upperRosserBoundaryMassAux 0 s a b

The discrete depth-zero shell is bounded by the base continuous boundary mass after passage to logarithmic coordinates.

theorem MathlibNt.SieveTheory.LinearSieve.sum_upperRosserBoundary_eq_sum_chains (D q : ℕ) (P : Finset ℕ) (w : ℕ → ℝ) : ∑ u ∈ P.powerset with (UpperRosserBoundarySet D q) u, ∏ p ∈ u, w p = ∑ l ∈ upperRosserBoundaryChains D q P, (List.map w l).prod

Exact injective reindexing of the boundary powerset sum by canonical decreasing chains.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChains_length_le {D q : ℕ} {P : Finset ℕ} {l : List ℕ} (hl : l ∈ upperRosserBoundaryChains D q P) : l.length ≤ P.card

A canonical boundary chain cannot be longer than its ambient finite prime set.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChains_length_even {D q : ℕ} {P : Finset ℕ} {l : List ℕ} (hl : l ∈ upperRosserBoundaryChains D q P) : Even l.length

Every upper Rosser boundary chain has even length.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity_nonneg (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hnu : ∀ p ∈ P, 0 ≤ nu p) (k : ℕ) : 0 ≤ upperRosserBoundaryChainsFixedDepthDensity nu D q P k

A fixed-depth selected boundary density is nonnegative when all ambient prime weights are nonnegative.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthRelativeDensity_nonneg (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hnu : ∀ p ∈ P, 0 ≤ nu p) (hnuOne : ∀ p ∈ P, nu p ≤ 1) (k : ℕ) : 0 ≤ upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q P k

Relative fixed-depth boundary densities are nonnegative under the natural local-density bounds.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity_mono {f g : ℕ → ℝ} {D q k : ℕ} {P : Finset ℕ} (hf : ∀ p ∈ P, 0 ≤ f p) (hfg : ∀ p ∈ P, f p ≤ g p) : upperRosserBoundaryChainsFixedDepthDensity f D q P k ≤ upperRosserBoundaryChainsFixedDepthDensity g D q P k

Fixed-depth boundary-chain density is monotone in every nonnegative prime weight on its ambient carrier.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChainsFixedDepthDensity_eq_zero_of_card_lt (nu : ℕ → ℝ) {D q k : ℕ} {P : Finset ℕ} (hk : P.card < 2 * k) : upperRosserBoundaryChainsFixedDepthDensity nu D q P k = 0

A fixed-depth selected boundary density vanishes once twice the depth exceeds the number of available ambient primes.

theorem MathlibNt.SieveTheory.LinearSieve.sum_upperRosserBoundaryChains_by_length (D q : ℕ) (P : Finset ℕ) (f : List ℕ → ℝ) : ∑ l ∈ upperRosserBoundaryChains D q P, f l = ∑ ell ∈ Finset.range (P.card + 1), ∑ l ∈ upperRosserBoundaryChains D q P with l.length = ell, f l

The canonical chain sum decomposes as a finite sigma over chain length. This is the exact finite starting point for estimating each nested Rosser region and then controlling the tail uniformly in the length.

theorem MathlibNt.SieveTheory.LinearSieve.sum_upperRosserBoundaryChains_by_even_length (D q : ℕ) (P : Finset ℕ) (f : List ℕ → ℝ) : ∑ l ∈ upperRosserBoundaryChains D q P, f l = ∑ ell ∈ Finset.range (P.card + 1) with Even ell, ∑ l ∈ upperRosserBoundaryChains D q P with l.length = ell, f l

Since boundary chains have even cardinality, the depth sigma may be restricted exactly to even lengths.

theorem MathlibNt.SieveTheory.LinearSieve.sum_upperRosserBoundaryChains_by_depth (D q : ℕ) (P : Finset ℕ) (f : List ℕ → ℝ) : ∑ l ∈ upperRosserBoundaryChains D q P, f l = ∑ k ∈ Finset.range (P.card + 1), ∑ l ∈ upperRosserBoundaryChains D q P with l.length = 2 * k, f l

The canonical boundary-chain sum decomposes exactly by pair depth. This reindexes the even chain length 2k directly by the recursion parameter k.

theorem MathlibNt.SieveTheory.LinearSieve.sum_upperRosserBoundary_eq_sum_fixedDepthDensity (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) : ∑ u ∈ P.powerset with (UpperRosserBoundarySet D q) u, ∏ p ∈ u, nu p = ∑ k ∈ Finset.range (P.card + 1), upperRosserBoundaryChainsFixedDepthDensity nu D q P k

The complete selected boundary density is the finite sum of its exact pair-depth slices.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryDensity_div_eulerProduct_eq_sum_fixedDepthRelativeDensity (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) : (∑ u ∈ P.powerset with (UpperRosserBoundarySet D q) u, ∏ p ∈ u, nu p) / ∏ p ∈ P, (1 - nu p) = ∑ k ∈ Finset.range (P.card + 1), upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q P k

Exact decomposition of a normalized boundary density into its finite relative pair-depth slices.

theorem MathlibNt.SieveTheory.LinearSieve.sum_upperRosserBoundaryChains_fixed_length (D q : ℕ) (P : Finset ℕ) (w : ℕ → ℝ) (ell : ℕ) : ∑ l ∈ upperRosserBoundaryChains D q P with l.length = ell, (List.map w l).prod = ∑ u ∈ Finset.filter (UpperRosserBoundarySet D q) P.powerset with u.card = ell, ∏ p ∈ u, w p

At a fixed depth, the canonical decreasing-chain sum is exactly the corresponding cardinality slice of the boundary powerset.

theorem MathlibNt.SieveTheory.LinearSieve.sum_upperRosserBoundaryChains_fixed_length_le_powersetCard (D q : ℕ) (P : Finset ℕ) (w : ℕ → ℝ) (hw : ∀ p ∈ P, 0 ≤ w p) (ell : ℕ) : ∑ l ∈ upperRosserBoundaryChains D q P with l.length = ell, (List.map w l).prod ≤ ∑ u ∈ Finset.powersetCard ell P, ∏ p ∈ u, w p

Dropping the Rosser inequalities at a fixed depth leaves the full elementary symmetric sum. This is the finite domination needed before applying a factorial/geometric tail estimate.

theorem MathlibNt.SieveTheory.LinearSieve.factorial_mul_sum_powersetCard_prod_le_pow_sum {α : Type u_1} [DecidableEq α] (P : Finset α) (w : α → ℝ) (hw : ∀ p ∈ P, 0 ≤ w p) (ell : ℕ) : ↑ell.factorial * ∑ u ∈ Finset.powersetCard ell P, ∏ p ∈ u, w p ≤ (∑ p ∈ P, w p) ^ ell

The elementary symmetric sum of fixed degree is bounded by the corresponding power sum, with the factorial accounting for all orderings of each subset.

theorem MathlibNt.SieveTheory.LinearSieve.factorial_mul_sum_upperRosserBoundaryChains_fixed_length_le_pow_sum (D q : ℕ) (P : Finset ℕ) (w : ℕ → ℝ) (hw : ∀ p ∈ P, 0 ≤ w p) (ell : ℕ) : ↑ell.factorial * ∑ l ∈ upperRosserBoundaryChains D q P with l.length = ell, (List.map w l).prod ≤ (∑ p ∈ P, w p) ^ ell

A fixed-depth upper Rosser boundary sum has factorial decay in its depth, uniformly in the Rosser parameters.

theorem MathlibNt.SieveTheory.LinearSieve.sum_upperRosserBoundaryChains_fixed_length_le_pow_sum_div_factorial (D q : ℕ) (P : Finset ℕ) (w : ℕ → ℝ) (hw : ∀ p ∈ P, 0 ≤ w p) (ell : ℕ) : ∑ l ∈ upperRosserBoundaryChains D q P with l.length = ell, (List.map w l).prod ≤ (∑ p ∈ P, w p) ^ ell / ↑ell.factorial

Division form of the fixed-depth factorial estimate.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySet_empty_iff {D q : ℕ} (hD : 1 < D) (hqprime : Nat.Prime q) : UpperRosserBoundarySet D q ∅ ↔ D ≤ q ^ 3

The depth-zero upper Rosser boundary is the elementary cubic cutoff.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySet_max_cube_lt {D q : ℕ} {s : Finset ℕ} (hs : s.Nonempty) (hboundary : UpperRosserBoundarySet D q s) : s.max' hs ^ 3 < D

The largest prime in any nonempty upper Rosser boundary tail is below the cubic level. This is the outer support inequality for arbitrary-depth boundary chains, independent of the distinguished prime q.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySet_mem_cube_lt {D q p : ℕ} {s : Finset ℕ} (hp : p ∈ s) (hboundary : UpperRosserBoundarySet D q s) : p ^ 3 < D

Every selected prime in an upper Rosser boundary tail lies below D^(1/3) in the integral form p³ < D.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySet_mem_log_div_le_third {z Δ s : ℝ} {q p : ℕ} {t : Finset ℕ} (hz : 2 ≤ z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log z) (hpPrime : Nat.Prime p) (hp : p ∈ t) (hboundary : UpperRosserBoundarySet (⌊Δ⌋₊ + 1) q t) : Real.log ↑p / Real.log z ≤ s / 3

At real level Δ = z^s, every prime in a boundary tail has logarithmic coordinate at most s / 3. The natural level ⌊Δ⌋ + 1 introduces no loss in this upper support bound.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAdmissibleSet_pair_iff {D r t : ℕ} (hrt : r < t) : UpperRosserAdmissibleSet D {r, t} ↔ t ^ 3 < D

For an increasing two-prime tail, upper Rosser admissibility is exactly the cubic restriction on its larger prime.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundarySet_pair_iff {D q r t : ℕ} (hqprime : Nat.Prime q) (htprime : Nat.Prime t) (hqr : q < r) (hrt : r < t) : UpperRosserBoundarySet D q {r, t} ↔ t ^ 3 < D ∧ D ≤ r * t * q ^ 3

The two-prime boundary is the first nontrivial Rosser chain: if q < r < t, then t³ < D ≤ q³rt.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetWeight_pair_eq_euler_add_boundary {D q : ℕ} {s : Finset ℕ} (hqs : q ∉ s) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ s, q ≤ p) (nuq : ℝ) : upperRosserSetWeight D s + nuq * upperRosserSetWeight D (insert q s) = (1 - nuq) * upperRosserSetWeight D s + if UpperRosserBoundarySet D q s then nuq else 0

Pairing a set with the set obtained by adjoining a new least prime produces the Euler factor 1 - nuq, apart from the explicit even Rosser boundary.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensitySum_insert_eq_euler_add_boundary (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hq : q ∉ P) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ P, q ≤ p) : upperRosserSetDensitySum nu D (insert q P) = (1 - nu q) * upperRosserSetDensitySum nu D P + nu q * ∑ s ∈ P.powerset with (UpperRosserBoundarySet D q) s, ∏ p ∈ s, nu p

Finite Buchstab--Rosser recursion in Euler-factor form. Removing the least prime contributes the expected factor 1 - nu q; the only correction is the explicit even Rosser boundary where adjoining q first violates the cutoff.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensityRatio_insert (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hq : q ∉ P) (hqprime : Nat.Prime q) (hqD : q < D) (hqmin : ∀ p ∈ P, q ≤ p) (hqFactor : 1 - nu q ≠ 0) (hPFactor : ∏ p ∈ P, (1 - nu p) ≠ 0) : upperRosserSetDensitySum nu D (insert q P) / ∏ p ∈ insert q P, (1 - nu p) = upperRosserSetDensitySum nu D P / ∏ p ∈ P, (1 - nu p) + nu q / (1 - nu q) * ((∑ s ∈ P.powerset with (UpperRosserBoundarySet D q) s, ∏ p ∈ s, nu p) / ∏ p ∈ P, (1 - nu p))

Normalized one-prime Rosser recursion. After division by the finite sieve product, each peeled prime contributes its boundary mass with coefficient nu q / (1 - nu q).

theorem MathlibNt.SieveTheory.LinearSieve.prod_nu_div_eulerProduct_eq (nu : ℕ → ℝ) {P s : Finset ℕ} (hs : s ⊆ P) : (∏ p ∈ s, nu p) / ∏ p ∈ P, (1 - nu p) = (∏ p ∈ s, nu p / (1 - nu p)) * ∏ p ∈ P \ s, (1 - nu p)⁻¹

Splitting an Euler denominator over a subset and its complement turns a density monomial into selected prime ratios and unselected inverse factors.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryDensity_div_eulerProduct (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) : (∑ s ∈ P.powerset with (UpperRosserBoundarySet D q) s, ∏ p ∈ s, nu p) / ∏ p ∈ P, (1 - nu p) = ∑ s ∈ P.powerset with (UpperRosserBoundarySet D q) s, (∏ p ∈ s, nu p / (1 - nu p)) * ∏ p ∈ P \ s, (1 - nu p)⁻¹

The normalized boundary sum is a sum of path monomials: selected primes contribute nu p / (1 - nu p), while unselected tail primes contribute the inverse Euler factor.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensityRatio_eq_one_add_sum_boundary (nu : ℕ → ℝ) {D : ℕ} (P : Finset ℕ) (hD : 1 < D) (hprime : ∀ p ∈ P, Nat.Prime p) (hpD : ∀ p ∈ P, p < D) (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserSetDensitySum nu D P / ∏ p ∈ P, (1 - nu p) = 1 + ∑ q ∈ P, nu q / (1 - nu q) * ((∑ s ∈ {p ∈ P | q < p}.powerset with (UpperRosserBoundarySet D q) s, ∏ p ∈ s, nu p) / ∏ p ∈ P with q < p, (1 - nu p))

Exact path expansion of the normalized upper Rosser density. The primes are peeled in increasing order; the tail after q is therefore precisely the set of primes larger than q. Each term is the normalized mass of the cubic boundary first encountered at that prime.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensityRatio_eq_one_add_sum_relativeBoundaryDepths (nu : ℕ → ℝ) {D : ℕ} (P : Finset ℕ) (hD : 1 < D) (hprime : ∀ p ∈ P, Nat.Prime p) (hpD : ∀ p ∈ P, p < D) (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserSetDensitySum nu D P / ∏ p ∈ P, (1 - nu p) = 1 + ∑ q ∈ P, nu q / (1 - nu q) * ∑ k ∈ Finset.range ({p ∈ P | q < p}.card + 1), upperRosserBoundaryChainsFixedDepthRelativeDensity nu D q ({p ∈ P | q < p}) k

The exact normalized upper Rosser density grouped by relative Buchstab pair depth. In contrast to a selected-chain majorant, each depth slice still carries the complete Euler denominator above its distinguished prime.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensityRatio_eq_one_add_sum_boundaryPaths (nu : ℕ → ℝ) {D : ℕ} (P : Finset ℕ) (hD : 1 < D) (hprime : ∀ p ∈ P, Nat.Prime p) (hpD : ∀ p ∈ P, p < D) (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserSetDensitySum nu D P / ∏ p ∈ P, (1 - nu p) = 1 + ∑ q ∈ P, nu q / (1 - nu q) * ∑ s ∈ {p ∈ P | q < p}.powerset with (UpperRosserBoundarySet D q) s, (∏ p ∈ s, nu p / (1 - nu p)) * ∏ p ∈ {p ∈ P | q < p} \ s, (1 - nu p)⁻¹

Fully factorized Rosser path expansion. After choosing the first boundary prime q, every selected tail prime contributes its normalized density and every skipped tail prime contributes its inverse Euler factor.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensityRatio_eq_one_add_sum_cubicBoundary (nu : ℕ → ℝ) {D : ℕ} (P : Finset ℕ) (hD : 1 < D) (hprime : ∀ p ∈ P, Nat.Prime p) (hpD : ∀ p ∈ P, p < D) (hfactor : ∀ p ∈ P, 1 - nu p ≠ 0) : upperRosserSetDensitySum nu D P / ∏ p ∈ P, (1 - nu p) = 1 + ∑ q ∈ P, nu q / (1 - nu q) * ((∑ u ∈ {p ∈ P | q < p}.powerset with Even u.card ∧ u.prod id < D ∧ UpperRosserAdmissibleSet D u ∧ D ≤ u.prod id * q ^ 3, ∏ p ∈ u, nu p) / ∏ p ∈ P with q < p, (1 - nu p))

The path expansion with the abstract boundary predicate eliminated. Thus the entire excess over the Euler product is a sum over even admissible tails in the explicit cubic shell D ≤ (∏ s) q ^ 3.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserSetDensitySum_min_eq_euler_add_boundary (nu : ℕ → ℝ) {D : ℕ} {P : Finset ℕ} (hP : P.Nonempty) (hprime : ∀ p ∈ P, Nat.Prime p) (hD : ∀ p ∈ P, p < D) : upperRosserSetDensitySum nu D P = (1 - nu (P.min' hP)) * upperRosserSetDensitySum nu D (P.erase (P.min' hP)) + nu (P.min' hP) * ∑ s ∈ (P.erase (P.min' hP)).powerset with (UpperRosserBoundarySet D (P.min' hP)) s, ∏ p ∈ s, nu p

Cardinality-decreasing Euler-factor recursion at the least prime.

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserWeight (P D d : ℕ) : ℝ

The explicit finite upper Rosser coefficient, with the standard odd-position Rosser admissibility test and strict level support built into its definition.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserWeight P D d = if d ∈ P.divisors ∧ d < D ∧ MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissible D d then if Even d.primeFactors.card then 1 else -1 else 0

theorem MathlibNt.SieveTheory.LinearSieve.mainSum_upperRosserWeight_eq_setDensitySum (S : BoundingSieve) (D : ℕ) : BoundingSieve.mainSum (upperRosserWeight S.prodPrimes D) = upperRosserSetDensitySum (⇑S.nu) D S.prodPrimes.primeFactors

The BoundingSieve.mainSum of the explicit upper Rosser coefficient is exactly its finite subset density sum. This removes divisor arithmetic from the analytic fundamental-lemma problem and exposes the prime-by-prime Buchstab recursion upperRosserSetDensitySum_insert.

theorem MathlibNt.SieveTheory.LinearSieve.abs_upperRosserWeight_le_one (P D d : ℕ) : |upperRosserWeight P D d| ≤ 1

theorem MathlibNt.SieveTheory.LinearSieve.abs_upperRosserWeight_le_threePow (P D d : ℕ) : |upperRosserWeight P D d| ≤ 3 ^ d.primeFactors.card

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserWeight_dvd {P D d : ℕ} (h : upperRosserWeight P D d ≠ 0) : d ∣ P

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserWeight_lt_level {P D d : ℕ} (h : upperRosserWeight P D d ≠ 0) : d < D

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserWeight_hasUpperLevelSupport (P D : ℕ) : HasUpperLevelSupport P D (upperRosserWeight P D)

def MathlibNt.SieveTheory.LinearSieve.IsUpperRosserCertificate (P D : ℕ) : Prop

The finite upper Rosser certificate is precisely the upper-Möbius condition on divisors of the chosen squarefree prime product.

Equations

• MathlibNt.SieveTheory.LinearSieve.IsUpperRosserCertificate P D = MathlibNt.SieveTheory.LinearSieve.IsUpperMoebiusOn P (MathlibNt.SieveTheory.LinearSieve.upperRosserWeight P D)

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserWeight_certificate {P D : ℕ} (hP : Squarefree P) (hP0 : P ≠ 0) (hD1 : 1 < D) (hD : ∀ p ∈ P.primeFactors, p < D) : IsUpperRosserCertificate P D

The explicit upper Rosser weight is a finite upper-Möbius certificate. The condition 1 < D is necessary for any strictly level-supported upper coefficient, since its coefficient at 1 must be at least one.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserWeight_divisor_sum {P D n : ℕ} (hcert : IsUpperRosserCertificate P D) (hn : n ∣ P) : (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, upperRosserWeight P D d

theorem MathlibNt.SieveTheory.LinearSieve.siftedSum_le_mainSum_add_upperErrSum_upperRosser {S : BoundingSieve} (D : ℕ) (hcert : IsUpperRosserCertificate S.prodPrimes D) : BoundingSieve.siftedSum ≤ S.totalMass * BoundingSieve.mainSum (upperRosserWeight S.prodPrimes D) + upperErrSum S D (upperRosserWeight S.prodPrimes D)

The explicit upper Rosser coefficient gives the finite upper-sieve inequality with the exact level-restricted remainder sum.