The triple main-term estimate (hTripleMain) #
This file proves the structural reduction for the triple main-term estimate
Σ_{p₁ ∈ [z,y)} Σ_{p₂ ∈ [y,N]} switchingCount N (p₁·p₂) ≤ cₘ·𝔖_trunc·N/log²N
from an explicit prime-pair hypothesis.
Here switchingCount N a = #{p ∈ C(N) : a·p₃ = N−p, p₃ prime} is a
twin-prime-type count requiring both p₃ and p = N−a·p₃ to be prime.
The required analytic upper bound, of the type arising in Chen's method and
Bombieri-Vinogradov distribution estimates, is stated as the proposition
ChenPrimePairInput. The remaining steps are proved here:
- Region reduction: p ∈ C(N) implies that N−p has no prime factor < z, so p₃ ≥ z and the effective region is p₁p₂ ≤ N/z, not merely 2p₁p₂ ≤ N. This gives log(N/(p₁p₂)) ≥ log z, a lower bound proportional to log N that is essential for the correct triple main-term scale.
- Apply the input pairwise: switchingCount ≤ C·(N/φ(p₁p₂))/(log N·log(N/(p₁p₂))).
- Use φ(p₁p₂) ≥ p₁p₂/4 for primes p₁,p₂ ≥ 2 and 1/log(N/(p₁p₂)) ≤ 1/log z.
- Bound the double prime-reciprocal sum by a constant using
AnalyticNumberTheory.Sieve.primeReciprocal_doubleSum_le. - Estimate the parameters: log z ≥ (1/20)log N, log y ≤ log 2 + (1/3)log N, and related bounds.
- Absorb constants using 𝔖_trunc ≥ 1/2
(
singularSeriesTruncated_ge_half).
Thus ChenPrimePairInput implies the existence of cₘ and N₀ₘ satisfying
hTripleMain. This supplies the triple main-term hypothesis of
corrected_chens_theorem_of_q1Count_and_triple; the Pan, q¹, and numerical
hypotheses remain explicit in the final conditional theorem.
1. Analytic input: a prime-pair bound (Chen's method / BV scale) #
Prime-pair input: the analytic core of hTripleMain.
For positive a, switchingCount N a = #{p ∈ C(N) : ∃p₃ prime, a·p₃ = N−p} counts p₃ for which p₃ and p = N−a·p₃ are prime (membership in C(N) implies that p is prime). This is a count of prime pairs in two linear forms. The input requires a uniform upper bound of the form used in Chen's method, Bombieri-Vinogradov estimates, and the linear sieve for two linear forms, with the singular series and local factors absorbed into the constant C:
switchingCount N a ≤ C · (N/φ(a)) · 1/(log N · log(N/a)), (1 ≤ a, 2a ≤ N)
The motivating classical estimate has the shape #{p₃ ≤ X : p₃, N−ap₃ prime} ≤ C·(a/φ(a))·X/(log X·log N), with X = N/a. This is the only additional analytic input to the triple main-term reduction; a Pan-distribution or prime-pair argument must supply it separately. Prime-counting upper bounds and Mertens estimates alone give only the N/log N scale: they lack the extra 1/log N factor from the primality of p and do not reach N/log²N. See the module introduction.
Equations
Instances For
2. Region reduction: p₃ ≥ z and p₁p₂ ≤ N/z #
If a·z > N (equivalently, N < z·a), then switchingCount N a = 0.
Proof: suppose p ∈ C(N), a·p₃ = N−p, and p₃ is prime. The condition defining C(N) says that N−p = a·p₃ has no prime factor < z. If p₃ < z, it would be such a factor, a contradiction. Hence p₃ ≥ z, so a·p₃ ≥ a·z > N ≥ N−p, contradicting a·p₃ = N−p.
Reduction of the triple main term to the z-region: contributing pairs
satisfy z·(p₁p₂) ≤ N; all other pairs contribute zero by
switchingCount_eq_zero_of_N_lt_z_mul.
This region gives N/(p₁p₂) ≥ z and hence log(N/(p₁p₂)) ≥ log z,
the lower bound needed for the N/log²N scale of the triple main term.
3. φ(p₁p₂) ≥ p₁p₂/4 #
Totient lower bound for a product of two primes (each ≥ 2): φ(p₁p₂) ≥ p₁p₂/4.
If p₁ = p₂, then φ(p²) = p(p−1) ≥ p²/2 ≥ p²/4. If p₁ ≠ p₂, they are coprime, and φ(p₁p₂) = (p₁−1)(p₂−1) ≥ (p₁/2)(p₂/2) = p₁p₂/4.
4. Parameter estimates (logarithmic bounds) #
z = max 2 ⌊N^{1/10}⌋ ≥ N^{1/10}/2 for N > 2^110.
log z ≥ (1/20)·log N for N > 2^110.
y ≤ 2·N^{1/3}, using the ceiling upper bound.
log y ≥ (1/3)·log N, from y³ ≥ N.
y ≤ N for N ≥ 8.
Parameter bound: z ≥ 3 for N ≥ 59049.
Parameter bound: z < y for N ≥ 9.
5. Logarithmic parameter bounds for hTripleMain #
log y/log z ≤ 7 for N > 2^110.
log N/log y ≤ 3 for N ≥ 8.
6. Main theorem: hTripleMain #
Pairwise bound: in the z-region, the input implies the upper bound C·(4/a)·(N/(log N·log z)), where a = p₁p₂.
The prime-pair input implies hTripleMain, in existential form.
ChenPrimePairInput gives a pairwise upper bound on switchingCount.
Combining the region reduction (switchingCount_sum_eq_z_region),
the totient bound, the double reciprocal-sum bound from
AnalyticNumberTheory.Sieve, and the logarithmic parameter bounds gives
cₘ = 160·C·(log 7+E)(log 3+E) and N₀ₘ = 2^220.
Here C comes from the input and E from primeReciprocal_doubleSum_le.
The bound 𝔖_trunc ≥ 1/2 absorbs a factor of 2.
Conditional endpoint with all analytic inputs explicit #
chensTheorem_fully_instantiated supplies the three inputs of
corrected_chens_theorem_of_q1Count_and_triple from explicit analytic hypotheses:
hPan←chenPanInput_of_sourceFaithfulSignedInputs(hI/hII/hM/htrunc); the exact signed pointwise decomposition is provided byAnalyticNumberTheory, whilePanSourceFaithfulSignedMainBoundremains an explicit hypothesis;hTripleMain←hTripleMain_of_primePairInput(hPP :ChenPrimePairInput);hq1←hq1_of_q1AnalyticInputs(hMain + hErr).
hnum is a numerical condition applied to the constants (cₘ, Cq) obtained
from hPP and hMain. As stated, it quantifies over every cₘ and every Cq > 0
for which the corresponding eventual bounds hold:
the double switchingCount sum ≤ cₘ·𝔖·N/log²N and q¹ ≤ Cq·𝔖·N/log²N.
It requires (10/3) > (cₘ + (Cq + 1/2))/2.
This final numerical condition is an explicit hypothesis alongside hPP and
hMain, not a numerical estimate established by this theorem. The structural
implication from all these hypotheses is proved below.