Rosser boundary chains and logarithmic regions

Upper admissibility, sorted prime chains, lower fixed-depth recursions, pair removal, and logarithmic-coordinate regions.

0.3. Finite upper Rosser weights

def MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissibleSet (D : ℕ) (s : Finset ℕ) : Prop

The standard upper Rosser test on a finite set of distinct primes. The test is imposed at odd positions in the decreasing list: at p = p_{2l+1} it says p₁⋯p_{2l} * p_{2l+1}^3 < D.

Equations

• MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissibleSet D s = ∀ p ∈ s, ¬Even {q ∈ s | p ≤ q}.card → {q ∈ s | p ≤ q}.prod id * p ^ 2 < D

def MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissible (D d : ℕ) : Prop

The upper Rosser test for the prime factors of a natural number.

Equations

• MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissible D d = MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissibleSet D d.primeFactors

noncomputable def MathlibNt.SieveTheory.LinearSieve.upperRosserSetWeight (D : ℕ) (s : Finset ℕ) : ℝ

The upper Rosser coefficient attached to a finite set of distinct primes.

Equations

• MathlibNt.SieveTheory.LinearSieve.upperRosserSetWeight D s = if s.prod id < D ∧ MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissibleSet D s then if Even s.card then 1 else -1 else 0

def MathlibNt.SieveTheory.LinearSieve.UpperRosserBoundarySet (D q : ℕ) (s : Finset ℕ) : Prop

The even Rosser boundary exposed when a new least prime is inserted: the old set is active, but adjoining q crosses either the level or an odd-position Rosser constraint.

Equations

• MathlibNt.SieveTheory.LinearSieve.UpperRosserBoundarySet D q s = (Even s.card ∧ s.prod id < D ∧ MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissibleSet D s ∧ ¬((insert q s).prod id < D ∧ MathlibNt.SieveTheory.LinearSieve.UpperRosserAdmissibleSet D (insert q s)))

theorem MathlibNt.SieveTheory.LinearSieve.sorted_prefix_toFinset_eq_filter_ge (s : Finset ℕ) (i : ℕ) (hi : i < (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) : (List.take (i + 1) (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).toFinset = {q ∈ s | (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ≤ q}

The first i + 1 entries of the decreasing enumeration of a finite set are exactly the entries greater than or equal to its entry at index i.

theorem MathlibNt.SieveTheory.LinearSieve.sorted_prefix_prod_eq_filter_ge (s : Finset ℕ) (i : ℕ) (hi : i < (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length) : {q ∈ s | (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ≤ q}.prod id = (List.take i (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).prod * (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i]

Product form of sorted_prefix_toFinset_eq_filter_ge: the filtered Rosser prefix is the product of the preceding entries and the entry at i.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserAdmissibleSet_iff_sorted_prefix_cube_lt {D : ℕ} {s : Finset ℕ} : UpperRosserAdmissibleSet D s ↔ ∀ (i : ℕ) (hi : i < (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length), Even i → (List.take i (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).prod * (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ^ 3 < D

The upper Rosser admissibility test in canonical chain coordinates. In the decreasing enumeration p₀ > p₁ > ..., precisely the even zero-based indices are tested, and their inequalities are p₀ ... pᵢ₋₁ * pᵢ³ < D.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserAdmissibleSet_iff_sorted_prefix_cube_lt {D : ℕ} {s : Finset ℕ} : LowerRosserAdmissibleSet D s ↔ ∀ (i : ℕ) (hi : i < (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2).length), ¬Even i → (List.take i (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).prod * (s.sort fun (x1 x2 : ℕ) => x1 ≥ x2)[i] ^ 3 < D

The lower Rosser admissibility test in canonical chain coordinates. In the strictly decreasing enumeration, precisely the odd zero-based indices are tested by the cubic prefix inequalities.

def MathlibNt.SieveTheory.LinearSieve.LowerRosserBoundaryChain (D q : ℕ) (l : List ℕ) : Prop

The ordered odd-chain region underlying one lower Rosser boundary term.

Equations

• MathlibNt.SieveTheory.LinearSieve.LowerRosserBoundaryChain D q l = (l.SortedGT ∧ ¬Even l.length ∧ l.prod < D ∧ (∀ (i : Fin l.length), ¬Even ↑i → (List.take (↑i) l).prod * l.get i ^ 3 < D) ∧ D ≤ l.prod * q ^ 3)

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

A lower boundary subset is equivalent to its canonical strictly decreasing, odd-length boundary chain.

def MathlibNt.SieveTheory.LinearSieve.UpperRosserBoundaryChain (D q : ℕ) (l : List ℕ) : Prop

The explicit ordered-chain region underlying one upper Rosser boundary term. This is the finite region that is later reindexed and compared with the Buchstab nested integrals.

Equations

• MathlibNt.SieveTheory.LinearSieve.UpperRosserBoundaryChain D q l = (l.SortedGT ∧ Even l.length ∧ l.prod < D ∧ (∀ (i : Fin l.length), Even ↑i → (List.take (↑i) l).prod * l.get i ^ 3 < D) ∧ D ≤ l.prod * q ^ 3)

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChain_singleton_iff {D q p : ℕ} : LowerRosserBoundaryChain D q [p] ↔ p < D ∧ D ≤ p * q ^ 3

A singleton lower Rosser boundary chain has no internal cubic test; only level activity and the terminal boundary remain.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChain_cons_cons_iff {D q p₀ p₁ : ℕ} {xs : List ℕ} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) : LowerRosserBoundaryChain D q (p₀ :: p₁ :: xs) ↔ p₁ < p₀ ∧ (∀ p ∈ xs, p < p₁) ∧ p₀ * p₁ ^ 3 < D ∧ LowerRosserBoundaryChain (D ⌈/⌉ (p₀ * p₁)) q xs

Removing the first two entries of a positive lower Rosser boundary chain produces the exact residual lower chain at the ceiling-divided level. The peeled pair contributes the first odd-index test p₀ * p₁^3 < D.

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

Canonical decreasing-list representatives of all lower boundary subsets of P; every represented list has odd length.

Equations

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

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

Exact membership characterization for the finite lower-boundary chain carrier.

theorem MathlibNt.SieveTheory.LinearSieve.mem_lowerRosserBoundaryChains_fixedPairDepth0_iff {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ P, q ≤ p) {l : List ℕ} (k : ℕ) : l ∈ {l ∈ lowerRosserBoundaryChains D q P | l.length = 2 * k + 1} ↔ l.Nodup ∧ l.SortedGT ∧ l.toFinset ⊆ P ∧ LowerRosserBoundaryChain D q l ∧ l.length = 2 * k + 1

The zero-based pair-depth slice consists of chains of length 2*k+1. It corresponds to Suzuki's full-chain source index 2*k+2 and Iwaniec's lower depth k+1.

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

Lower boundary chains at Suzuki's full-chain source index n. The terminal least prime is external to the stored list, hence l.length + 1 = n.

Equations

• MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChainsAtSourceIndex D q P n = {l ∈ MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChains D q P | l.length + 1 = n}

theorem MathlibNt.SieveTheory.LinearSieve.mem_lowerRosserBoundaryChainsAtSourceIndex_iff {D q n : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ P, q ≤ p) {l : List ℕ} : l ∈ lowerRosserBoundaryChainsAtSourceIndex D q P n ↔ l.Nodup ∧ l.SortedGT ∧ l.toFinset ⊆ P ∧ LowerRosserBoundaryChain D q l ∧ l.length + 1 = n

Exact source-index membership characterization.

theorem MathlibNt.SieveTheory.LinearSieve.even_sourceIndex_of_mem_lowerRosserBoundaryChainsAtSourceIndex {D q n : ℕ} {P : Finset ℕ} {l : List ℕ} (hl : l ∈ lowerRosserBoundaryChainsAtSourceIndex D q P n) : Even n

Every inhabited lower source-index slice has even Suzuki index.

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

Exact injective finite reindexing of the lower-boundary powerset sum by canonical odd decreasing chains.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChains_exists_unique_depth {D q : ℕ} {P : Finset ℕ} {l : List ℕ} (hl : l ∈ lowerRosserBoundaryChains D q P) : ∃! k : ℕ, l.length = 2 * k + 1

Every lower boundary chain belongs to a unique odd-depth slice.

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

The selected density mass of lower Rosser boundary chains at zero-based pair-depth k, i.e. of exact odd length 2*k+1.

Equations

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

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChainsFixedPairDepth0Density_eq_sourceIndex (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) (k : ℕ) : lowerRosserBoundaryChainsFixedPairDepth0Density nu D q P k = ∑ l ∈ lowerRosserBoundaryChainsAtSourceIndex D q P (2 * k + 2), (List.map nu l).prod

Zero-based pair-depth k is Suzuki's full-chain source index 2*k+2.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChainsFixedPairDepth0Density_zero (nu : ℕ → ℝ) {D q : ℕ} {P : Finset ℕ} (hqs : q ∉ P) (hqprime : Nat.Prime q) (hqmin : ∀ p ∈ P, q ≤ p) : lowerRosserBoundaryChainsFixedPairDepth0Density nu D q P 0 = ∑ p ∈ P with p < D ∧ D ≤ p * q ^ 3, nu p

The singleton lower-boundary density is exactly the one-prime terminal cubic shell.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChainsFixedPairDepth0Density_zero_eq_sourceIndex_two (nu : ℕ → ℝ) (D q : ℕ) (P : Finset ℕ) : lowerRosserBoundaryChainsFixedPairDepth0Density nu D q P 0 = ∑ l ∈ lowerRosserBoundaryChainsAtSourceIndex D q P 2, (List.map nu l).prod

Pair-depth zero is precisely source index n = 2.

theorem MathlibNt.SieveTheory.LinearSieve.mem_lowerRosserBoundaryChains_fixedPairDepth0_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 ∈ lowerRosserBoundaryChains D q P | l.length = 2 * (k + 1) + 1} ↔ ∃ p₀ ∈ P, ∃ p₁ ∈ P, p₁ < p₀ ∧ p₀ * p₁ ^ 3 < D ∧ ∃ (xs : List ℕ), l = p₀ :: p₁ :: xs ∧ xs ∈ {xs ∈ lowerRosserBoundaryChains (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ P | p < p₁}) | xs.length = 2 * k + 1}

Exact carrier recursion for positive pair-depth lower Rosser boundary chains. Peeling the two largest selected primes shifts source index by two.

theorem MathlibNt.SieveTheory.LinearSieve.lowerRosserBoundaryChainsFixedPairDepth0Density_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 : ℕ) : lowerRosserBoundaryChainsFixedPairDepth0Density nu D q P (k + 1) = ∑ p₀ ∈ P, ∑ p₁ ∈ P with p₁ < p₀ ∧ p₀ * p₁ ^ 3 < D, nu p₀ * nu p₁ * lowerRosserBoundaryChainsFixedPairDepth0Density nu (D ⌈/⌉ (p₀ * p₁)) q ({p ∈ P | p < p₁}) k

Exact two-prime successor recurrence for lower fixed-pair-depth density.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserBoundaryChain_cons_cons_iff {D q p₀ p₁ : ℕ} {xs : List ℕ} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) : UpperRosserBoundaryChain D q (p₀ :: p₁ :: xs) ↔ p₁ < p₀ ∧ (∀ p ∈ xs, p < p₁) ∧ p₀ ^ 3 < D ∧ UpperRosserBoundaryChain (D ⌈/⌉ (p₀ * p₁)) q xs

Removing the first two entries of a positive upper Rosser boundary chain gives an exact residual chain at the ceiling-divided level.

noncomputable def MathlibNt.SieveTheory.LinearSieve.logarithmicCoordinates (z : ℝ) (l : List ℕ) : List ℝ

Logarithmic coordinates of a finite prime chain, relative to the sifting cutoff z.

Equations

• MathlibNt.SieveTheory.LinearSieve.logarithmicCoordinates z l = List.map (fun (p : ℕ) => Real.log ↑p / Real.log z) l

theorem MathlibNt.SieveTheory.LinearSieve.sum_logarithmicCoordinates_eq_log_prod {z : ℝ} (l : List ℕ) (hl : ∀ p ∈ l, 0 < p) : (logarithmicCoordinates z l).sum = Real.log ↑l.prod / Real.log z

theorem MathlibNt.SieveTheory.LinearSieve.logarithmicCoordinates_sortedGT {z : ℝ} {l : List ℕ} (hz : 1 < z) (hlpos : ∀ p ∈ l, 0 < p) (hl : l.SortedGT) : (logarithmicCoordinates z l).SortedGT

theorem MathlibNt.SieveTheory.LinearSieve.logarithmicCoordinates_mem_Ioc {z : ℝ} (hz : 1 < z) {q : ℕ} {l : List ℕ} (hqpos : 0 < q) (hql : ∀ p ∈ l, q < p) (hlz : ∀ p ∈ l, ↑p ≤ z) (x : ℝ) : x ∈ logarithmicCoordinates z l → Real.log ↑q / Real.log z < x ∧ x ≤ 1

If a chain lies strictly above q and below z, then each logarithmic coordinate lies in (log q / log z, 1].

theorem MathlibNt.SieveTheory.LinearSieve.logarithmicCoordinates_prefix_cube {z : ℝ} {l : List ℕ} (hl : ∀ p ∈ l, 0 < p) (i : Fin l.length) : (logarithmicCoordinates z (List.take (↑i) l)).sum + 3 * (Real.log ↑(l.get i) / Real.log z) = Real.log ↑((List.take (↑i) l).prod * l.get i ^ 3) / Real.log z

theorem MathlibNt.SieveTheory.LinearSieve.log_nat_div_log_le_of_lt_floor_add_one {z Δ : ℝ} {n : ℕ} (hz : 1 < z) (hΔ : 0 < Δ) (hn : 0 < n) (h : n < ⌊Δ⌋₊ + 1) : Real.log ↑n / Real.log z ≤ Real.log Δ / Real.log z

theorem MathlibNt.SieveTheory.LinearSieve.log_div_log_lt_of_floor_add_one_le {z Δ : ℝ} {n : ℕ} (hz : 1 < z) (hΔ : 0 < Δ) (h : ⌊Δ⌋₊ + 1 ≤ n) : Real.log Δ / Real.log z < Real.log ↑n / Real.log z

def MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegion (s a : ℝ) (x : List ℝ) : Prop

The real-coordinate region cut out by the decreasing-order, alternating prefix, and terminal-shell conditions of an upper Rosser boundary chain.

Equations

• MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegion s a x = (x.SortedGT ∧ Even x.length ∧ x.sum ≤ s ∧ (∀ (i : ℕ) (hi : i < x.length), Even i → (List.take i x).sum + 3 * x[i] ≤ s) ∧ s < x.sum + 3 * a)

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserLogRegion_nil_iff {s a : ℝ} : UpperRosserLogRegion s a [] ↔ 0 ≤ s ∧ s < 3 * a

The empty upper Rosser region is exactly its terminal cubic shell.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserLogRegion_cons_cons_iff {s a x₀ x₁ : ℝ} {xs : List ℝ} : UpperRosserLogRegion s a (x₀ :: x₁ :: xs) ↔ (x₀ :: x₁ :: xs).SortedGT ∧ 3 * x₀ ≤ s ∧ UpperRosserLogRegion (s - x₀ - x₁) a xs

Removing the first pair of coordinates gives the exact Buchstab recursion for the real upper Rosser region.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserLogRegion_pair_iff {s a x₀ x₁ : ℝ} : UpperRosserLogRegion s a [x₀, x₁] ↔ x₁ < x₀ ∧ 3 * x₀ ≤ s ∧ x₀ + x₁ ≤ s ∧ s < x₀ + x₁ + 3 * a

The first nonempty upper Rosser region is the explicit two-coordinate shell used by the first Buchstab correction.

def MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegionBelow (s a b : ℝ) (x : List ℝ) : Prop

The upper Rosser region with every selected coordinate strictly between the terminal coordinate a and an inherited upper cutoff b.

Equations

• MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegionBelow s a b x = (MathlibNt.SieveTheory.LinearSieve.UpperRosserLogRegion s a x ∧ ∀ y ∈ x, a < y ∧ y < b)

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserLogRegionBelow_nil_iff {s a b : ℝ} : UpperRosserLogRegionBelow s a b [] ↔ 0 ≤ s ∧ s < 3 * a

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserLogRegionBelow_cons_cons_iff {s a b x₀ x₁ : ℝ} {xs : List ℝ} : UpperRosserLogRegionBelow s a b (x₀ :: x₁ :: xs) ↔ a < x₁ ∧ x₁ < x₀ ∧ x₀ < b ∧ 3 * x₀ ≤ s ∧ UpperRosserLogRegionBelow (s - x₀ - x₁) a x₁ xs

Exact bounded form of pair removal. The second peeled coordinate becomes the strict upper cutoff for every coordinate in the residual region.

theorem MathlibNt.SieveTheory.LinearSieve.upperRosserLogRegionBelow_of_length_succ_iff {s a b : ℝ} {x : List ℝ} {k : ℕ} (hlen : x.length = 2 * (k + 1)) : UpperRosserLogRegionBelow s a b x ↔ ∃ (x₀ : ℝ) (x₁ : ℝ) (xs : List ℝ), x = x₀ :: x₁ :: xs ∧ xs.length = 2 * k ∧ a < x₁ ∧ x₁ < x₀ ∧ x₀ < b ∧ 3 * x₀ ≤ s ∧ UpperRosserLogRegionBelow (s - x₀ - x₁) a x₁ xs

Induction-ready decomposition of every positive even-depth bounded Rosser region into its first ordered pair and a depth-two-shorter residual region.