A generic paper-Q-style modulus for Liu's finite weight

This module first develops the generic non-strict integer convention Q(N, w) = ∏ {r prime | r ≤ w and r ∤ N}. It then identifies the specialization at w = ⌊N^(1/4 - ε/2)⌋ with Liu's source definition, whose membership condition is the real inequality r ≤ N^(1/4 - ε/2).

The exact finite outer divisor sum from Liu's eqn-r0 is also assembled, with its cutoff retained. No asymptotic estimate or subsequent maximum bound is asserted.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 (N : ℕ) : ℕ

Liu's source lower cutoff for the first prime in eqn-adef. This is independent of the modulus-prime cutoff paperQSourceCutoff.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N = ⌊↑N ^ (1 / 10)⌋₊

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceY3 (N : ℕ) : ℕ

Liu's source split point between the two primes in eqn-adef.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N = ⌊↑N ^ (1 / 3)⌋₊

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_source_basic_range {N : ℕ} {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) : ↑N ^ (1 / 10) < ↑p.1 ∧ ↑p.1 ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p.2

The floor cutoffs recover the three strict/non-strict real source inequalities in eqn-adef.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_source_p₂_le_rpow_nine_twentieth {N : ℕ} {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) : ↑p.2 ≤ ↑N ^ (9 / 20)

The support condition and the strict N^(1/10) lower bound on p₁ imply the corrected upper exponent p₂ ≤ N^(9/20).

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_source_range {N : ℕ} {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)) : ↑N ^ (1 / 10) < ↑p.1 ∧ ↑p.1 ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p.2 ∧ ↑p.2 ≤ ↑N ^ (9 / 20)

All source-facing real consequences of an admissible pair at Liu's N^(1/10) and N^(1/3) cutoffs. The final exponent is 9/20, not the unsupported 4/10 printed in main.tex line 312.

def MathlibNt.SieveTheory.LiuWeight.paperQStylePrimes (N w : ℕ) : Finset ℕ

The finite set of primes at most w which do not divide N.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStylePrimes N w = {r ∈ Finset.range (w + 1) | Nat.Prime r ∧ ¬r ∣ N}

def MathlibNt.SieveTheory.LiuWeight.paperQStyleModulus (N w : ℕ) : ℕ

A generic paper-Q-style modulus with the non-strict integer convention r ≤ w.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleModulus N w = (MathlibNt.SieveTheory.LiuWeight.paperQStylePrimes N w).prod id

theorem MathlibNt.SieveTheory.LiuWeight.primeFactors_prod_eq_self_paperQ {S : Finset ℕ} (hS : ∀ p ∈ S, Nat.Prime p) : (S.prod id).primeFactors = S

The prime factors of a product over a finite prime set recover that set.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleModulus_ne_zero (N w : ℕ) : paperQStyleModulus N w ≠ 0

The generic modulus is nonzero because every factor is prime.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleModulus_primeFactors (N w : ℕ) : (paperQStyleModulus N w).primeFactors = paperQStylePrimes N w

The prime-factor finset of the generic modulus is exactly its defining set.

theorem MathlibNt.SieveTheory.LiuWeight.prime_dvd_paperQStyleModulus {N w r : ℕ} (hr : Nat.Prime r) : r ∣ paperQStyleModulus N w ↔ r ≤ w ∧ ¬r ∣ N

Exact prime-divisor characterization for the non-strict cutoff convention.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleModulus_squarefree (N w : ℕ) : Squarefree (paperQStyleModulus N w)

The generic prime product is squarefree.

theorem MathlibNt.SieveTheory.LiuWeight.prime_le_and_not_dvd_of_dvd_paperQStyleModulus {N w d r : ℕ} (hd : d ∣ paperQStyleModulus N w) (hr : Nat.Prime r) (hrd : r ∣ d) : r ≤ w ∧ ¬r ∣ N

Every prime factor of a divisor of the generic modulus respects both its cutoff and its exclusion from N.

theorem MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeMajorant_liuWeight_mod_eq_abs_main_sum_of_dvd_paperQStyleModulus (main : ℝ → ℝ) (N z w y Y X d : ℕ) (hwy : w ≤ y) (hd : d ∣ paperQStyleModulus N w) : liuMainNoncoprimeMajorant main Y X d (N % d) (liuWeight N z y) = ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |main (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Exact finite arbitrary-model R₁ majorant for a divisor of the generic modulus. The weight cutoff z remains independent of the modulus cutoff w.

theorem MathlibNt.SieveTheory.LiuWeight.abs_liuMainNoncoprimeSum_liuWeight_mod_le_abs_main_sum_of_dvd_paperQStyleModulus (main : ℝ → ℝ) (N z w y Y X d : ℕ) (hwy : w ≤ y) (hd : d ∣ paperQStyleModulus N w) : |liuMainNoncoprimeSum main Y X d (N % d) (liuWeight N z y)| ≤ ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |main (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Signed finite arbitrary-model R₁ bound for a divisor of the generic modulus.

theorem MathlibNt.SieveTheory.LiuWeight.panDistributionNoncoprimeMajorant_liuWeight_mod_eq_abs_li_sum_of_dvd_paperQStyleModulus (N z w y Y X d : ℕ) (hwy : w ≤ y) (hd : d ∣ paperQStyleModulus N w) : AnalyticNumberTheory.Sieve.panDistributionNoncoprimeMajorant Y X d (N % d) (liuWeight N z y) = ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Proxy specialization. Exact finite R₁ majorant using ANT's historical x / log x model. This is not a theorem about the paper's true li.

theorem MathlibNt.SieveTheory.LiuWeight.abs_panDistributionNoncoprimeSum_liuWeight_mod_le_abs_li_sum_of_dvd_paperQStyleModulus (N z w y Y X d : ℕ) (hwy : w ≤ y) (hd : d ∣ paperQStyleModulus N w) : |AnalyticNumberTheory.Sieve.panDistributionNoncoprimeSum Y X d (N % d) (liuWeight N z y)| ≤ ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |AnalyticNumberTheory.Sieve.logarithmicIntegral (↑Y / (↑p.1 * ↑p.2))| / ↑d.totient

Proxy specialization. Signed finite R₁ bound using ANT's historical x / log x model. Its type exhibits N, independent z,w,y, and the hypothesis d ∣ Q(N,w).

def MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors (N w D : ℕ) : Finset ℕ

The exact divisor index in Liu 2022, main.tex lines 296--300 (eqn-r0), using the explicit non-strict paperQStyleModulus convention. In particular, d = 1 is not removed.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors N w D = {d ∈ (MathlibNt.SieveTheory.LiuWeight.paperQStyleModulus N w).divisors | d ≤ D}

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1Majorant (main : ℝ → ℝ) (N z w y D X : ℕ) : ℝ

The finite outer non-coprime majorant with an arbitrary main-term model, generic support cutoff X, and exact index d ∣ Q(N,w), d ≤ D.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1Majorant main N z w y D X = ∑ d ∈ MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeMajorant main N X d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N z y)

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1SignedSum (main : ℝ → ℝ) (N z w y D X : ℕ) : ℝ

The corresponding finite outer signed sum for an arbitrary main-term model.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1SignedSum main N z w y D X = ∑ d ∈ MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeSum main N X d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N z y)

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1Majorant_eq_abs_main_sum (main : ℝ → ℝ) (N z w y D X : ℕ) (hwy : w ≤ y) : paperQStyleMainR1Majorant main N z w y D X = ∑ d ∈ paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card * ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |main (↑N / (↑p.1 * ↑p.2))| / ↑d.totient

Exact outer arbitrary-model rewrite before every analytic estimate in Liu 2022 main.tex line 304.

theorem MathlibNt.SieveTheory.LiuWeight.abs_paperQStyleMainR1SignedSum_le_majorant (main : ℝ → ℝ) (N z w y D X : ℕ) : |paperQStyleMainR1SignedSum main N z w y D X| ≤ paperQStyleMainR1Majorant main N z w y D X

Outer triangle bound for the arbitrary-model signed finite sum.

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1Majorant (main : ℝ → ℝ) (N z w y D : ℕ) : ℝ

Source-facing Liu R₁ majorant with the paper scale fixed as X = N. The function main remains abstract, so this definition does not identify the paper's li with ANT's proxy.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1Majorant main N z w y D = MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1Majorant main N z w y D N

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1SignedSum (main : ℝ → ℝ) (N z w y D : ℕ) : ℝ

Source-facing signed Liu R₁ sum with X = N.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1SignedSum main N z w y D = MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1SignedSum main N z w y D N

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1Majorant_eq_abs_main_sum (main : ℝ → ℝ) (N z w y D : ℕ) (hwy : w ≤ y) : paperQStyleSourceR1Majorant main N z w y D = ∑ d ∈ paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card * ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ N ∧ p.1 ∣ d, |main (↑N / (↑p.1 * ↑p.2))| / ↑d.totient

Source-facing outer rewrite with X = N, matching the N in Liu's eqn-delta-def and eqn-r0.

theorem MathlibNt.SieveTheory.LiuWeight.abs_paperQStyleSourceR1SignedSum_le_majorant (main : ℝ → ℝ) (N z w y D : ℕ) : |paperQStyleSourceR1SignedSum main N z w y D| ≤ paperQStyleSourceR1Majorant main N z w y D

Source-facing outer triangle bound with X = N.

Reduction under a paper-li upper model

def MathlibNt.SieveTheory.LiuWeight.PaperLiUpperModel (main : ℝ → ℝ) (C : ℝ) : Prop

An explicit upper model for a candidate paper logarithmic integral. No identification with ANT's historical x / log x proxy is made.

Equations

• MathlibNt.SieveTheory.LiuWeight.PaperLiUpperModel main C = (0 ≤ C ∧ ∀ (x : ℝ), 2 ≤ x → |main x| ≤ C * x / Real.log x)

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_product_pos {N z y : ℕ} {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N z y) : 0 < p.1 * p.2

An admissible Liu pair has positive product.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_rpow_one_third_le_div {N z y : ℕ} {p : ℕ × ℕ} (hp : p ∈ liuWeightPairs N z y) : ↑N ^ (1 / 3) ≤ ↑N / (↑p.1 * ↑p.2)

The root-free cube support bound gives the real cube-root lower bound for the quotient appearing in the main term.

theorem MathlibNt.SieveTheory.LiuWeight.two_le_div_of_mem_liuWeightPairs {N z y : ℕ} {p : ℕ × ℕ} (hN : 8 ≤ N) (hp : p ∈ liuWeightPairs N z y) : 2 ≤ ↑N / (↑p.1 * ↑p.2)

The threshold N ≥ 8 makes the source main-term argument at least 2.

theorem MathlibNt.SieveTheory.LiuWeight.one_third_mul_log_le_log_div_of_mem_liuWeightPairs {N z y : ℕ} {p : ℕ × ℕ} (hN : 8 ≤ N) (hp : p ∈ liuWeightPairs N z y) : 1 / 3 * Real.log ↑N ≤ Real.log (↑N / (↑p.1 * ↑p.2))

Logarithmic consequence of the cube-root lower bound.

theorem MathlibNt.SieveTheory.LiuWeight.PaperLiUpperModel.abs_main_div_le {main : ℝ → ℝ} {C : ℝ} {N z y : ℕ} {p : ℕ × ℕ} (hmain : PaperLiUpperModel main C) (hN : 8 ≤ N) (hp : p ∈ liuWeightPairs N z y) : |main (↑N / (↑p.1 * ↑p.2))| ≤ 3 * C * ↑N / (↑p.1 * ↑p.2 * Real.log ↑N)

Pointwise Liu-pair estimate under an explicit paper-li upper model.

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1ReciprocalSum (N z w y D : ℕ) : ℝ

The exact finite double reciprocal sum left after applying the paper-li upper model. No maximum, Euler product, or Mertens estimate is built into it.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1ReciprocalSum N z w y D = ∑ d ∈ MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card * ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N z y with p.1 * p.2 ≤ N ∧ p.1 ∣ d, 1 / (↑p.1 * ↑p.2 * ↑d.totient)

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleR1PairReciprocalSum (N z y d : ℕ) : ℝ

The reciprocal sum over admissible Liu pairs whose first prime divides d. The parameters z and y retain their independent source roles.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleR1PairReciprocalSum N z y d = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N z y with p.1 * p.2 ≤ N ∧ p.1 ∣ d, 1 / (↑p.1 * ↑p.2)

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₁Range (N d : ℕ) : Finset ℕ

The exact outer p₁ index in Liu's nested source sum, including primality and p₁ ∣ d.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₁Range N d = {p₁ ∈ Finset.range (N + 1) | Nat.Prime p₁ ∧ MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N < p₁ ∧ p₁ ≤ MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N ∧ p₁ ∣ d}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂Range (N p₁ : ℕ) : Finset ℕ

The exact inner p₂ index in Liu's nested source sum. The root-free size condition is exactly the square-root cutoff from eqn-adef.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂Range N p₁ = {p₂ ∈ Finset.range (N + 1) | Nat.Prime p₂ ∧ MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N < p₂ ∧ p₁ * p₂ ^ 2 ≤ N}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1NestedPairReciprocalSum (N d : ℕ) : ℝ

Liu's pair reciprocal sum written as an exact nested p₁,p₂ finite sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1NestedPairReciprocalSum N d = ∑ p₁ ∈ MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₁Range N d, ∑ p₂ ∈ MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂Range N p₁, 1 / (↑p₁ * ↑p₂)

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleR1PairReciprocalSum_source_eq_nested (N d : ℕ) : paperQStyleR1PairReciprocalSum N (liuSourceZ10 N) (liuSourceY3 N) d = liuSourceR1NestedPairReciprocalSum N d

Exact reindexing of the retained pair sum into Liu's nested source ranges. The redundant p₁*p₂ ≤ N filter follows from the exact square-root condition.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularPairs (N d : ℕ) : Finset (ℕ × ℕ)

The corrected rectangular source range: p₁ > N^(1/10) and N^(1/3) < p₂ ≤ N^(9/20), with primality and p₁ ∣ d retained.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularPairs N d = {p ∈ (Finset.range (N + 1)).product (Finset.range (N + 1)) | Nat.Prime p.1 ∧ ↑N ^ (1 / 10) < ↑p.1 ∧ p.1 ∣ d ∧ Nat.Prime p.2 ∧ ↑N ^ (1 / 3) < ↑p.2 ∧ ↑p.2 ≤ ↑N ^ (9 / 20)}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularPairReciprocalSum (N d : ℕ) : ℝ

The reciprocal sum over the corrected rectangular source range.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularPairReciprocalSum N d = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularPairs N d, 1 / (↑p.1 * ↑p.2)

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleR1PairReciprocalSum_source_le_rectangular (N d : ℕ) : paperQStyleR1PairReciprocalSum N (liuSourceZ10 N) (liuSourceY3 N) d ≤ liuSourceR1RectangularPairReciprocalSum N d

Monotonicity from the exact nested source range to the corrected rectangle. No prime-reciprocal estimate or Mertens theorem is used.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularP₁Range (N d : ℕ) : Finset ℕ

The first-coordinate index in the corrected rectangular majorant.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularP₁Range N d = {p ∈ Finset.range (N + 1) | Nat.Prime p ∧ ↑N ^ (1 / 10) < ↑p ∧ p ∣ d}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularP₂Range (N : ℕ) : Finset ℕ

The corrected [1/3, 9/20] prime interval in the second coordinate.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularP₂Range N = {p ∈ Finset.range (N + 1) | Nat.Prime p ∧ ↑N ^ (1 / 3) < ↑p ∧ ↑p ≤ ↑N ^ (9 / 20)}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₁DivisorReciprocalSum (N d : ℕ) : ℝ

The reciprocal divisor-prime factor in the corrected rectangle.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₁DivisorReciprocalSum N d = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularP₁Range N d, 1 / ↑p

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂IntervalReciprocalSum (N : ℕ) : ℝ

The reciprocal prime sum on the corrected [1/3, 9/20] interval.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂IntervalReciprocalSum N = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularP₂Range N, 1 / ↑p

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularPairs_eq_product (N d : ℕ) : liuSourceR1RectangularPairs N d = (liuSourceR1RectangularP₁Range N d).product (liuSourceR1RectangularP₂Range N)

The finite corrected rectangle is exactly the product of its two coordinate indices.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1RectangularPairReciprocalSum_eq_mul (N d : ℕ) : liuSourceR1RectangularPairReciprocalSum N d = liuSourceR1P₁DivisorReciprocalSum N d * liuSourceR1P₂IntervalReciprocalSum N

Exact factorization of the corrected rectangular pair reciprocal sum.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂IntervalReciprocalSum_nonneg (N : ℕ) : 0 ≤ liuSourceR1P₂IntervalReciprocalSum N

The second-coordinate reciprocal interval sum is nonnegative.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂ReciprocalBound : ℝ

A fixed global bound for the corrected [1/3, 9/20] reciprocal prime interval, chosen from the verified Mertens theorem.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂ReciprocalBound = Classical.choose MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂ReciprocalBound._proof_1

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂ReciprocalBound_spec (N : ℕ) (hN : 2 ≤ N) : |liuSourceR1P₂IntervalReciprocalSum N| ≤ liuSourceR1P₂ReciprocalBound

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂ReciprocalBound_nonneg : 0 ≤ liuSourceR1P₂ReciprocalBound

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₂IntervalReciprocalSum_le (N : ℕ) (hN : 2 ≤ N) : liuSourceR1P₂IntervalReciprocalSum N ≤ liuSourceR1P₂ReciprocalBound

theorem MathlibNt.SieveTheory.LiuWeight.one_div_le_ten_mul_rpow_neg_one_tenth_mul_log_div_log (N p : ℕ) (hN : 2 ≤ N) (hp : ↑N ^ (1 / 10) < ↑p) : 1 / ↑p ≤ 10 * ↑N ^ (-1 / 10) * Real.log ↑p / Real.log ↑N

The pointwise logarithmic gain from p > N^(1/10). The threshold N ≥ 2 is sufficient for every positivity and logarithmic division used here.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₁_log_sum_le_log (N d : ℕ) (hd : 0 < d) : ∑ p ∈ liuSourceR1RectangularP₁Range N d, Real.log ↑p ≤ Real.log ↑d

The logarithms of the selected distinct prime divisors sum to at most log d. This uses their product dividing d, not a cardinality estimate.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSourceD2 (N : ℕ) : ℕ

Liu's source divisor cutoff D₂ = floor(N^(1/2)).

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSourceD2 N = ⌊↑N ^ (1 / 2)⌋₊

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceR1P₁DivisorReciprocalSum_le (N d : ℕ) (hN : 2 ≤ N) (hd : 0 < d) (hdD : d ≤ liuSourceD2 N) : liuSourceR1P₁DivisorReciprocalSum N d ≤ 5 * ↑N ^ (-1 / 10)

The first-coordinate reciprocal divisor sum has the concrete uniform 5 N^(-1/10) bound up to the source cutoff D₂.

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleR1DivisorWeightSum (N w D : ℕ) : ℝ

The truncated divisor-weight sum from the exact R₁ index, including d = 1 whenever 1 ≤ D.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleR1DivisorWeightSum N w D = ∑ d ∈ MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card / ↑d.totient

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleFullDivisorWeightSum (N w : ℕ) : ℝ

The full divisor-weight sum over all divisors of the generic paper-Q-style modulus.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleFullDivisorWeightSum N w = ∑ d ∈ (MathlibNt.SieveTheory.LiuWeight.paperQStyleModulus N w).divisors, 3 ^ d.primeFactors.card / ↑d.totient

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1ReciprocalSum_eq_weighted_pair_sums (N z w y D : ℕ) : paperQStyleSourceR1ReciprocalSum N z w y D = ∑ d ∈ paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card / ↑d.totient * paperQStyleR1PairReciprocalSum N z y d

Exact factorization of the retained reciprocal sum into the divisor weight and the per-modulus pair reciprocal sum.

def MathlibNt.SieveTheory.LiuWeight.PaperQStyleR1PairUniformBound (N z w y D : ℕ) (M : ℝ) : Prop

A transparent uniform upper bound for every per-modulus pair reciprocal sum in the exact truncated divisor index.

Equations

• MathlibNt.SieveTheory.LiuWeight.PaperQStyleR1PairUniformBound N z w y D M = (0 ≤ M ∧ ∀ d ∈ MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors N w D, MathlibNt.SieveTheory.LiuWeight.paperQStyleR1PairReciprocalSum N z y d ≤ M)

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleR1PairReciprocalSum_nonneg (N z y d : ℕ) : 0 ≤ paperQStyleR1PairReciprocalSum N z y d

Every per-modulus pair reciprocal sum is nonnegative.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleR1PairUniformBound_source (N w : ℕ) (hN : 2 ≤ N) : PaperQStyleR1PairUniformBound N (liuSourceZ10 N) w (liuSourceY3 N) (liuSourceD2 N) (5 * liuSourceR1P₂ReciprocalBound * ↑N ^ (-1 / 10))

At the frozen source cutoffs and D₂, every per-modulus pair sum is bounded by 5 C₂ N^(-1/10).

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleSourceR1ReciprocalSum_le_divisorWeight_mul (N z w y D : ℕ) (M : ℝ) (hM : PaperQStyleR1PairUniformBound N z w y D M) : paperQStyleSourceR1ReciprocalSum N z w y D ≤ paperQStyleR1DivisorWeightSum N w D * M

A uniform per-modulus pair bound factors out of the exact reciprocal sum.

theorem MathlibNt.SieveTheory.LiuWeight.PaperLiUpperModel.paperQStyleSourceR1Majorant_le {main : ℝ → ℝ} {C : ℝ} (N z w y D : ℕ) (hmain : PaperLiUpperModel main C) (hN : 8 ≤ N) (hwy : w ≤ y) : paperQStyleSourceR1Majorant main N z w y D ≤ 3 * C * ↑N / Real.log ↑N * paperQStyleSourceR1ReciprocalSum N z w y D

Source-facing Liu R₁ reduction under an explicit paper-li upper model. The right side retains the exact finite divisor and pair sums.

theorem MathlibNt.SieveTheory.LiuWeight.PaperLiUpperModel.paperQStyleSourceR1Majorant_le_divisorWeight_mul {main : ℝ → ℝ} {C M : ℝ} (N z w y D : ℕ) (hmain : PaperLiUpperModel main C) (hN : 8 ≤ N) (hwy : w ≤ y) (hM : PaperQStyleR1PairUniformBound N z w y D M) : paperQStyleSourceR1Majorant main N z w y D ≤ 3 * C * ↑N / Real.log ↑N * (paperQStyleR1DivisorWeightSum N w D * M)

The paper-li upper-model reduction combined with a transparent uniform bound for the exact per-modulus pair sums.

theorem MathlibNt.SieveTheory.LiuWeight.PaperLiUpperModel.paperQStyleSourceR1Majorant_le_source_pair_bound {main : ℝ → ℝ} {C : ℝ} (N w : ℕ) (hmain : PaperLiUpperModel main C) (hN : 8 ≤ N) (hwy : w ≤ liuSourceY3 N) : paperQStyleSourceR1Majorant main N (liuSourceZ10 N) w (liuSourceY3 N) (liuSourceD2 N) ≤ 3 * C * ↑N / Real.log ↑N * (paperQStyleR1DivisorWeightSum N w (liuSourceD2 N) * (5 * liuSourceR1P₂ReciprocalBound * ↑N ^ (-1 / 10)))

The paper-li majorant specialized to the verified source pair bound at z = floor(N^(1/10)), y = floor(N^(1/3)), and D₂ = floor(N^(1/2)).

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleR1DivisorWeightSum_le_full (N w D : ℕ) : paperQStyleR1DivisorWeightSum N w D ≤ paperQStyleFullDivisorWeightSum N w

Dropping the cutoff d ≤ D only enlarges the nonnegative divisor-weight sum.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleFullDivisorWeightSum_eq_eulerProduct (N w : ℕ) : paperQStyleFullDivisorWeightSum N w = ∏ p ∈ paperQStylePrimes N w, (1 + 3 / (↑p - 1))

Exact squarefree Euler product for the full divisor-weight sum.

Liu 2022 main.tex line 194 prints p - 2 in this local factor. That is a source typo: because Nat.totient p = p - 1 for prime p, the exact factor is 1 + 3 / (p - 1). No Mertens or asymptotic estimate is used here.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleEulerFactor_le_mertensFactor_inv_cube {p : ℕ} (hp : Nat.Prime p) : 1 + 3 / (↑p - 1) ≤ (1 - 1 / ↑p)⁻¹ ^ 3

The corrected local divisor factor is bounded by the reciprocal cube of the corresponding Mertens factor. This includes p = 2; primality supplies all denominator positivity used in the proof.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleFullDivisorWeightSum_le_primeProduct_inv_cube (N w : ℕ) (hw : w ≤ N) : paperQStyleFullDivisorWeightSum N w ≤ (MertensTheorem.primeProduct N)⁻¹ ^ 3

For w ≤ N, enlarging from the primes defining the paper-Q-style modulus to every prime at most N bounds the full divisor sum by the reciprocal cube of the Mertens product.

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleMertensLowerConstant : ℝ

A fixed positive choice of lower-bound constant for the Mertens product.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleMertensLowerConstant = Classical.choose MathlibNt.SieveTheory.MertensTheorem.primeProduct_lower_bound_exists

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleMertensLowerConstant_pos : 0 < paperQStyleMertensLowerConstant

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleMertensLowerConstant_spec (N : ℕ) (hN : 3 ≤ N) : paperQStyleMertensLowerConstant / Real.log ↑N ≤ MertensTheorem.primeProduct N

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleDivisorWeightLogConstant : ℝ

The fixed divisor-weight constant obtained by cubing the reciprocal of the chosen Mertens lower-bound constant.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleDivisorWeightLogConstant = MathlibNt.SieveTheory.LiuWeight.paperQStyleMertensLowerConstant⁻¹ ^ 3

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleDivisorWeightLogConstant_pos : 0 < paperQStyleDivisorWeightLogConstant

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleDivisorWeightLogConstant_nonneg : 0 ≤ paperQStyleDivisorWeightLogConstant

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleFullDivisorWeightSum_le_log_cube (N w : ℕ) (hN : 3 ≤ N) (hw : w ≤ N) : paperQStyleFullDivisorWeightSum N w ≤ paperQStyleDivisorWeightLogConstant * Real.log ↑N ^ 3

The corrected full divisor weight is O((log N)^3), uniformly for w ≤ N, with an explicit choice-defined constant and threshold N ≥ 3.

theorem MathlibNt.SieveTheory.LiuWeight.PaperLiUpperModel.paperQStyleSourceR1Majorant_le_log_square {main : ℝ → ℝ} {C : ℝ} (N w : ℕ) (hmain : PaperLiUpperModel main C) (hN : 8 ≤ N) (hwy : w ≤ liuSourceY3 N) (hwN : w ≤ N) : paperQStyleSourceR1Majorant main N (liuSourceZ10 N) w (liuSourceY3 N) (liuSourceD2 N) ≤ 15 * C * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Conditional source endpoint. Assuming the supplied main satisfies the explicit PaperLiUpperModel true-li boundary, the verified R1 layers give the source majorant bound with the exact harmless constant 15 = 3 * 5. This theorem does not instantiate main or identify it with ANT's proxy.

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleOuterR1Majorant (N z w y D X : ℕ) : ℝ

The finite outer non-coprime majorant from Liu 2022, main.tex lines 296--300, with Y = N, canonical residue N % d, and a generic support cutoff X. This legacy declaration is the ANT x / log x proxy specialization, not the paper's true-li layer.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleOuterR1Majorant N z w y D X = ∑ d ∈ MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card * AnalyticNumberTheory.Sieve.panDistributionNoncoprimeMajorant N X d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N z y)

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQStyleOuterR1SignedSum (N z w y D X : ℕ) : ℝ

The corresponding finite outer signed non-coprime sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQStyleOuterR1SignedSum N z w y D X = ∑ d ∈ MathlibNt.SieveTheory.LiuWeight.paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card * AnalyticNumberTheory.Sieve.panDistributionNoncoprimeSum N X d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N z y)

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1Majorant_proxy (N z w y D X : ℕ) : paperQStyleMainR1Majorant AnalyticNumberTheory.Sieve.logarithmicIntegral N z w y D X = paperQStyleOuterR1Majorant N z w y D X

The legacy outer majorant is exactly the ANT proxy specialization.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleMainR1SignedSum_proxy (N z w y D X : ℕ) : paperQStyleMainR1SignedSum AnalyticNumberTheory.Sieve.logarithmicIntegral N z w y D X = paperQStyleOuterR1SignedSum N z w y D X

The legacy outer signed sum is exactly the ANT proxy specialization.

theorem MathlibNt.SieveTheory.LiuWeight.paperQStyleOuterR1Majorant_eq_abs_li_sum (N z w y D X : ℕ) (hwy : w ≤ y) : paperQStyleOuterR1Majorant N z w y D X = ∑ d ∈ paperQStyleR1Divisors N w D, 3 ^ d.primeFactors.card * ∑ p ∈ liuWeightPairs N z y with p.1 * p.2 ≤ X ∧ p.1 ∣ d, |AnalyticNumberTheory.Sieve.logarithmicIntegral (↑N / (↑p.1 * ↑p.2))| / ↑d.totient

Proxy specialization. Exact outer rewrite with ANT's x / log x compatibility model. It is not an identification with the paper's true li.

theorem MathlibNt.SieveTheory.LiuWeight.abs_paperQStyleOuterR1SignedSum_le_majorant (N z w y D X : ℕ) (_hwy : w ≤ y) : |paperQStyleOuterR1SignedSum N z w y D X| ≤ paperQStyleOuterR1Majorant N z w y D X

Proxy specialization. Outer triangle bound for the legacy signed finite sum. This does not assert a true-li model or any estimate from lines 304--319.

noncomputable def MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff (N : ℕ) (ε : ℝ) : ℕ

The natural cutoff obtained by flooring the paper's real exponent N^(1/4 - ε/2).

Equations

• MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff N ε = ⌊↑N ^ (1 / 4 - ε / 2)⌋₊

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQPrimes (N : ℕ) (ε : ℝ) : Finset ℕ

The source-facing finite set in Liu main.tex line 219: primes satisfying the real, non-strict cutoff p ≤ N^(1/4 - ε/2) and not dividing N. The range bound is only a finite carrier; mem_liuPaperQPrimes exposes the source formula.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPaperQPrimes N ε = {p ∈ Finset.range (MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff N ε + 1) | Nat.Prime p ∧ ¬p ∣ N ∧ ↑p ≤ ↑N ^ (1 / 4 - ε / 2)}

theorem MathlibNt.SieveTheory.LiuWeight.mem_liuPaperQPrimes {N p : ℕ} {ε : ℝ} : p ∈ liuPaperQPrimes N ε ↔ Nat.Prime p ∧ ¬p ∣ N ∧ ↑p ≤ ↑N ^ (1 / 4 - ε / 2)

Membership in Liu's source-facing prime set is exactly the real inequality printed in main.tex line 219, together with primality and p ∤ N.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQPrimes_eq_paperQStylePrimes (N : ℕ) (ε : ℝ) : liuPaperQPrimes N ε = paperQStylePrimes N (paperQSourceCutoff N ε)

Flooring the nonnegative real power loses no natural primes at the non-strict source cutoff.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus (N : ℕ) (ε : ℝ) : ℕ

Liu's source modulus Q, defined from the real cutoff in line 219.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N ε = (MathlibNt.SieveTheory.LiuWeight.liuPaperQPrimes N ε).prod id

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus_eq_paperQStyleModulus (N : ℕ) (ε : ℝ) : liuPaperQModulus N ε = paperQStyleModulus N (paperQSourceCutoff N ε)

Liu's real-cutoff modulus is exactly the generic floor-cutoff modulus.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceR1Majorant (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : ℝ

The fully source-specialized finite R₁ majorant, whose outer divisors use the real-cutoff modulus liuPaperQModulus and whose weight lower cutoff remains the distinct liuSourceZ10.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceR1Majorant main N ε = ∑ d ∈ (MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N ε).divisors with d ≤ MathlibNt.SieveTheory.LiuWeight.liuSourceD2 N, 3 ^ d.primeFactors.card * MathlibNt.SieveTheory.LiuWeight.liuMainNoncoprimeMajorant main N N d (N % d) (MathlibNt.SieveTheory.LiuWeight.liuWeight N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N))

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQSourceR1Majorant_eq_paperQStyleSourceR1Majorant (main : ℝ → ℝ) (N : ℕ) (ε : ℝ) : liuPaperQSourceR1Majorant main N ε = paperQStyleSourceR1Majorant main N (liuSourceZ10 N) (paperQSourceCutoff N ε) (liuSourceY3 N) (liuSourceD2 N)

The source-Q majorant is exactly the generic floor-cutoff specialization.

theorem MathlibNt.SieveTheory.LiuWeight.paperQSourceCutoff_le_floor_cuberoot (N : ℕ) (ε : ℝ) (hN : 1 ≤ N) (hε : 0 ≤ ε) : paperQSourceCutoff N ε ≤ ⌊↑N ^ (1 / 3)⌋₊

Under the elementary source assumptions, the exponent cutoff is no larger than the floored cube-root cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceY3_le (N : ℕ) (hN : 1 ≤ N) : liuSourceY3 N ≤ N

The floored source cube-root cutoff is no larger than N for N ≥ 1.

theorem MathlibNt.SieveTheory.LiuWeight.PaperLiUpperModel.paperQStyleSourceR1Majorant_le_log_square_cutoff {main : ℝ → ℝ} {C : ℝ} (N : ℕ) (ε : ℝ) (hmain : PaperLiUpperModel main C) (hN : 8 ≤ N) (hε : 0 ≤ ε) : paperQStyleSourceR1Majorant main N (liuSourceZ10 N) (paperQSourceCutoff N ε) (liuSourceY3 N) (liuSourceD2 N) ≤ 15 * C * liuSourceR1P₂ReciprocalBound * paperQStyleDivisorWeightLogConstant * ↑N ^ (9 / 10) * Real.log ↑N ^ 2

Conditional source-cutoff endpoint. For ε ≥ 0, the natural floored paper cutoff meets both cutoff hypotheses of paperQStyleSourceR1Majorant_le_log_square. The PaperLiUpperModel hypothesis is retained explicitly; no unconditional R1 or true-li identification follows.