Q1 main-term absorption #

Scope #

This file proves the q¹ main-term bound q1MainTermAbsorption from SwitchingPrinciple.lean:

∃ C₁ > 0, ∃ N₁, ∀ N ≥ N₁ Even N:
  q1MainTermSum N ≤ C₁·𝔖_trunc(N, z−1)·N/log²N

Here z = correctedChenZ N, y = correctedChenY N, P(N) = correctedChenSiftingProduct N (odd primes r < z with r ∤ N), F(N) = correctedChenForbiddenProduct N (primes r < z with r ≤ 2 or r | N), and Fodd(N) = F(N)/2 (the product of the odd prime factors of F when z ≥ 3).

Mathematical structure (sieve main terms in Halberstam--Richert Ch. 10; Chen 1973) #

For a fixed prime q ∈ [z, y), d | P, and e | F:

q1APMainValue N (lcm(lcm q d) e) = if Even (lcm(lcm q d) e) then [lcm(lcm q d) e | N−2] else li(N)/φ(lcm(lcm q d) e).

The numbers q, d, e are pairwise coprime: q ≥ z, all prime factors of P·F are < z, and P and F have disjoint prime-factor sets. In the odd part, q and d are odd, and e is odd exactly when e | Fodd. Thus lcm(lcm q d) e = q·d·e, and

q1CandidateAPMain N q = li(N)·Σ_{d|P} Σ_{e|Fodd} μ(d)μ(e)/φ(q·d·e) + (even-modulus correction, ≤ 0).

The odd part factors through the Möbius Euler-product identity (Mathlib's prodPrimeFactors_one_sub_of_squarefree):

Σ_{d|P} μ(d)/φ(d) = ∏{p|P} (1 − 1/(p−1)) =: q1SieveProduct N, Σ{e|Fodd} μ(e)/φ(e) = ∏_{p|Fodd} (1 − 1/(p−1)) =: q1ForbiddenOddProduct N,

The even part is exactly zero or negative, by Möbius inversion Σ_{d|m} μ(d) = [m = 1]:

EvenPart = −[q | N−2]·[gcd(P, N−2) = 1]·[gcd(Fodd, (N−2)/2) = 1] ≤ 0.

Consequently, for even N (where p ∤ N automatically excludes p = 2),

q1MainTermSum N ≤ li(N)·goldbachSieveProduct(N, z)·Σ_{q∈[z,y)} 1/φ(q).

goldbachSieveProduct(N, z) = primeProduct(z−1)·𝔖_trunc(N, z−1) (MertensTheorem.sieveProduct_identity);
primeProduct(z−1) ≤ a₂/log(z−1), log(z−1) ≥ (1/20)·log N (Mertens' theorem and an elementary estimate);
Σ_{q∈[z,y)} 1/φ(q) ≤ 2·Σ 1/q ≤ 2·(primeReciprocalSum y − primeReciprocalSum (z−1)) ≤ 2·(log(log y/log z) + E) ≤ 2·(log 7 + E) (AnalyticNumberTheory.Sieve.primeReciprocalSum_range_le and log y/log z ≤ 7 from hTripleMain_log_y_div_log_z_le in TripleMain.lean).

Combining these estimates gives q1MainTermAbsorption, with C₁ = 20·a₂·(2·(log 7 + E)).

The analytic ingredients are the proved prime-reciprocal range bound and the goldbachNu / singularSeriesTruncated definitions in AnalyticNumberTheory.Sieve, the theorems MertensTheorem.primeProduct_asymptotic_order and sieveProduct_identity, and the logarithmic parameter bounds from TripleMain.lean.

Q1 main-term absorption #

Scope #

Mathematical structure (sieve main terms in Halberstam--Richert Ch. 10; Chen 1973) #

Notation and definitions #

1. Möbius sums: Σ_{d|n} μ(d) = [n = 1], Σ_{d|n, d|m} μ(d) = [gcd(m,n) = 1] #

2. Parity and coprimality lemmas #

3. Odd-even decomposition of the q¹ main term #

4. Exact evaluation of the even-modulus contribution (Möbius inversion) #

5. Möbius Euler-product factorization: Σ_{d|P} μ(d)/φ(d) = ∏_{p|P} (1 − 1/(p−1)) #

6. Bounds for each q and decomposition of the main-term sum #

7. Combining analytic estimates: prime reciprocals, log(z−1), and absorption #

The finite delta-one Pan bridge for the q¹ error #