MathlibNt.SieveTheory.SingularSeries

Sieve-normalized finite Goldbach factor

This file retains the finite factor used by the legacy Chen sieve development. It is not Liu's source singular series: it includes the local factor at p = 2, and singularSeries N is truncated at N rather than an infinite product.

The corresponding odd-prime infinite expression in the literature is

𝔖_odd(N) = Π_{p | N, p > 2} (p-1)/(p-2) · Π_{p > 2} (1 - 1/(p-1)²).

The second product is the twin-prime constant C₂ ≈ 0.66016...

For even N, the local factors used in this file simplify to:

• p = 2: the factor is 2;
• p > 2, p | N: the factor is p/(p-1);
• p > 2, p ∤ N: the factor is p(p-2)/(p-1)².

References:

• Chen, J.R. (1973), Sci. Sinica 16, 157-176
• Liu, Z. (2022), "A Corrected Simplified Proof of Chen's Theorem", arXiv:2203.07871
• Halberstam & Richert, "Sieve Methods" (1974)

1. Local factors

noncomputable def MathlibNt.SieveTheory.SingularSeries.localFactor (p N : ℕ) : ℝ

The local factor of the singular series at a prime p.

For p > 2:

• if p | N: g(p, N) = (p-1)/(p-2) · (1 - 1/(p-1)²) = p/(p-1);
• if p ∤ N: g(p, N) = (1 - 1/(p-1)²) = p(p-2)/(p-1)².

The factor at p = 2 is handled separately (it is 2 for even N).

Equations

• MathlibNt.SieveTheory.SingularSeries.localFactor p N = if p = 2 then if 2 ∣ N then 2 else 1 else if p ∣ N then ↑p / (↑p - 1) else ↑p * (↑p - 2) / (↑p - 1) ^ 2

theorem MathlibNt.SieveTheory.SingularSeries.localFactor_two {N : ℕ} (hN : Even N) : localFactor 2 N = 2

The factor at p = 2 is 2 for even N.

theorem MathlibNt.SieveTheory.SingularSeries.localFactor_two_odd {N : ℕ} (hN : Odd N) : localFactor 2 N = 1

The factor at p = 2 is 1 for odd N.

theorem MathlibNt.SieveTheory.SingularSeries.localFactor_of_dvd {p N : ℕ} (_hp : Nat.Prime p) (hp2 : 2 < p) (hpdvd : p ∣ N) : localFactor p N = ↑p / (↑p - 1)

For a prime p > 2 with p | N, the factor is p/(p-1).

theorem MathlibNt.SieveTheory.SingularSeries.localFactor_of_not_dvd {p N : ℕ} (_hp : Nat.Prime p) (hp2 : 2 < p) (hpn : ¬p ∣ N) : localFactor p N = ↑p * (↑p - 2) / (↑p - 1) ^ 2

For a prime p > 2 with p ∤ N, the factor is p(p-2)/(p-1)².

2. Positivity of local factors

theorem MathlibNt.SieveTheory.SingularSeries.localFactor_pos {p N : ℕ} (hp : Nat.Prime p) : 0 < localFactor p N

All local factors at primes are positive.

3. Truncated singular series

noncomputable def MathlibNt.SieveTheory.SingularSeries.singularSeriesTruncated (N z : ℕ) : ℝ

The truncated singular series is the product of local factors at primes p ≤ z:

𝔖(N, z) = Π_{p ≤ z, p.Prime} localFactor p N.

For fixed positive N, the limit as z → ∞ is the corresponding sieve-normalized infinite product. This is distinct from the finite proxy singularSeries N, which uses z = N; no convergence theorem is asserted by this definition.

Equations

• MathlibNt.SieveTheory.SingularSeries.singularSeriesTruncated N z = ∏ p ∈ Finset.range (z + 1) with Nat.Prime p, MathlibNt.SieveTheory.SingularSeries.localFactor p N

theorem MathlibNt.SieveTheory.SingularSeries.singularSeriesTruncated_pos (N z : ℕ) (_hz : 1 ≤ z) : 0 < singularSeriesTruncated N z

The truncated singular series is positive, since all its factors are positive.

4. The finite singular-series proxy

noncomputable def MathlibNt.SieveTheory.SingularSeries.singularSeries (N : ℕ) : ℝ

Legacy finite sieve-normalized proxy, obtained by truncating at N.

This is deliberately kept for compatibility with the existing Chen APIs. It is not Liu's odd-prime infinite singular series.

Equations

• MathlibNt.SieveTheory.SingularSeries.singularSeries N = MathlibNt.SieveTheory.SingularSeries.singularSeriesTruncated N N

theorem MathlibNt.SieveTheory.SingularSeries.singularSeries_pos (N : ℕ) (hN : 2 ≤ N) : 0 < singularSeries N

The finite singular-series proxy is positive.

5. Explicit formula in the even case

theorem MathlibNt.SieveTheory.SingularSeries.singularSeries_even_factor (N : ℕ) (hN : Even N) (_hN2 : 2 ≤ N) : singularSeriesTruncated N 2 = 2

For even N, the singular series contains the factor 2 at p = 2; the truncation at 2 consists of this factor alone.

6. Upper bounds for local factors

theorem MathlibNt.SieveTheory.SingularSeries.localFactor_dvd_le {p N : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) (hpdvd : p ∣ N) : localFactor p N ≤ 3 / 2

For a prime p > 2 with p | N, the factor p/(p-1) ≤ 3/2, since p ≥ 3.

theorem MathlibNt.SieveTheory.SingularSeries.localFactor_not_dvd_lt_one {p N : ℕ} (hp : Nat.Prime p) (hp2 : 2 < p) (hpn : ¬p ∣ N) : localFactor p N < 1

For a prime p > 2 with p ∤ N, the factor p(p-2)/(p-1)² < 1, since p ≥ 3.

7. Bounds for the singular series (elementary proofs)

theorem MathlibNt.SieveTheory.SingularSeries.singularSeries_bounded_below : ∃ (c : ℝ), 0 < c ∧ ∀ (N : ℕ), 2 ≤ N → Even N → c ≤ singularSeries N

A positive lower bound for the finite singular series: 𝔖(N) ≥ 1 for every even N ≥ 2.

Elementary proof: for even N, with all prime products restricted to p ≤ N, 𝔖(N) = 2 · ∏{p|N, p>2} p/(p-1) · ∏{p∤N, p>2} p(p-2)/(p-1)². Here p/(p-1) ≥ 1, and the prime product ∏{2<p≤N} (1 - 1/(p-1)²) is at least ∏{n=2}^{N-1} (1 - 1/n²) = N/(2(N-1)) ≥ 1/2 by telescoping. Thus 𝔖(N) ≥ 2 · 1 · 1/2 = 1.

theorem MathlibNt.SieveTheory.SingularSeries.singularSeries_bounded_above : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ), 2 ≤ N → singularSeries N ≤ C * ↑N

Upper bound for the truncated definition: 𝔖(N) ≤ 2^ω(N) ≤ 2N.

A bound 𝔖(N) ≤ C with an absolute constant C is false: along primorials (products of all primes up to x, such as 2·3·5·7·...), the factors ∏_{p|N} p/(p-1) grow on the order of log log N, while the remaining product stays bounded away from zero, so 𝔖(N) is unbounded. The elementary bound uses local factors ≤ 2 when p | N and ≤ 1 otherwise. It gives 𝔖(N) ≤ 2^ω(N), and hence also the looser bound 𝔖(N) ≤ 2^{ω(N)+1} ≤ 2N.

8. Mathematical scope