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:

1. 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.
2. Apply the input pairwise: switchingCount ≤ C·(N/φ(p₁p₂))/(log N·log(N/(p₁p₂))).
3. Use φ(p₁p₂) ≥ p₁p₂/4 for primes p₁,p₂ ≥ 2 and 1/log(N/(p₁p₂)) ≤ 1/log z.
4. Bound the double prime-reciprocal sum by a constant using AnalyticNumberTheory.Sieve.primeReciprocal_doubleSum_le.
5. Estimate the parameters: log z ≥ (1/20)log N, log y ≤ log 2 + (1/3)log N, and related bounds.
6. 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)

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenPrimePairInput : Prop

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

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenPrimePairInput = ∃ (C : ℝ), 0 < C ∧ ∀ (N a : ℕ), 1 ≤ a → 2 * a ≤ N → MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount N a ≤ C * ↑N / ↑a.totient / (Real.log ↑N * Real.log (↑N / ↑a))

2. Region reduction: p₃ ≥ z and p₁p₂ ≤ N/z

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount_eq_zero_of_N_lt_z_mul (N a : ℕ) (haz : N < correctedChenZ N * a) : switchingCount N a = 0

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.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount_sum_eq_z_region (N : ℕ) : ∑ p₁ ∈ Finset.range (correctedChenY N) with Nat.Prime p₁ ∧ correctedChenZ N ≤ p₁, ∑ p₂ ∈ Finset.range (N + 1) with Nat.Prime p₂ ∧ correctedChenY N ≤ p₂, switchingCount N (p₁ * p₂) = ∑ p₁ ∈ Finset.range (correctedChenY N) with Nat.Prime p₁ ∧ correctedChenZ N ≤ p₁, ∑ p₂ ∈ {p₂ ∈ Finset.range (N + 1) | Nat.Prime p₂ ∧ correctedChenY N ≤ p₂} with correctedChenZ N * (p₁ * p₂) ≤ N, switchingCount N (p₁ * 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

theorem MathlibNt.SieveTheory.SwitchingPrinciple.totient_mul_prime_ge_quarter {p₁ p₂ : ℕ} (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) : ↑p₁ * ↑p₂ / 4 ≤ ↑(p₁ * p₂).totient

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.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.one_div_totient_mul_prime_le (p₁ p₂ : ℕ) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) : 1 / ↑(p₁ * p₂).totient ≤ 4 / (↑p₁ * ↑p₂)

Real-valued reciprocal form: 1/φ(p₁p₂) ≤ 4/(p₁p₂).

4. Parameter estimates (logarithmic bounds)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ_ge_root_half (N : ℕ) (hNbig : 2 ^ 110 < N) : ↑N ^ (1 / 10) / 2 ≤ ↑(correctedChenZ N)

z = max 2 ⌊N^{1/10}⌋ ≥ N^{1/10}/2 for N > 2^110.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.log_ge_110_log_two {N : ℕ} (hNbig : 2 ^ 110 < N) : 110 * Real.log 2 ≤ Real.log ↑N

log N ≥ 110·log 2 for N > 2^110.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ_log_ge_logN_div_twenty (N : ℕ) (hNbig : 2 ^ 110 < N) : 1 / 20 * Real.log ↑N ≤ Real.log ↑(correctedChenZ N)

log z ≥ (1/20)·log N for N > 2^110.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY_le_two_mul_root (N : ℕ) (hN : 1 ≤ N) : ↑(correctedChenY N) ≤ 2 * ↑N ^ (1 / 3)

y ≤ 2·N^{1/3}, using the ceiling upper bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY_log_le (N : ℕ) (hN : 1 ≤ N) : Real.log ↑(correctedChenY N) ≤ Real.log 2 + 1 / 3 * Real.log ↑N

log y ≤ log 2 + (1/3)·log N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY_log_ge (N : ℕ) (hN : 1 ≤ N) : 1 / 3 * Real.log ↑N ≤ Real.log ↑(correctedChenY N)

log y ≥ (1/3)·log N, from y³ ≥ N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY_le_N {N : ℕ} (hN : 8 ≤ N) : correctedChenY N ≤ N

y ≤ N for N ≥ 8.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ_ge_three {N : ℕ} (hN : 59049 ≤ N) : 3 ≤ correctedChenZ N

Parameter bound: z ≥ 3 for N ≥ 59049.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ_lt_Y {N : ℕ} (hN : 9 ≤ N) : correctedChenZ N < correctedChenY N

Parameter bound: z < y for N ≥ 9.

5. Logarithmic parameter bounds for hTripleMain

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hTripleMain_one_div_log_z_le (N : ℕ) (hNbig : 2 ^ 110 < N) : 1 / Real.log ↑(correctedChenZ N) ≤ 20 / Real.log ↑N

1/log z ≤ 20/log N for N > 2^110.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hTripleMain_log_y_div_log_z_le (N : ℕ) (hNbig : 2 ^ 110 < N) : Real.log ↑(correctedChenY N) / Real.log ↑(correctedChenZ N) ≤ 7

log y/log z ≤ 7 for N > 2^110.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hTripleMain_log_N_div_log_y_le (N : ℕ) (hN : 8 ≤ N) : Real.log ↑N / Real.log ↑(correctedChenY N) ≤ 3

log N/log y ≤ 3 for N ≥ 8.

6. Main theorem: hTripleMain

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hTripleMain_pair_bound {C : ℝ} {N p₁ p₂ : ℕ} (hC : 0 ≤ C) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hza : correctedChenZ N * (p₁ * p₂) ≤ N) (hin : switchingCount N (p₁ * p₂) ≤ C * ↑N / ↑(p₁ * p₂).totient / (Real.log ↑N * Real.log (↑N / (↑p₁ * ↑p₂)))) : switchingCount N (p₁ * p₂) ≤ C * (4 / (↑p₁ * ↑p₂)) * (↑N / (Real.log ↑N * Real.log ↑(correctedChenZ N)))

Pairwise bound: in the z-region, the input implies the upper bound C·(4/a)·(N/(log N·log z)), where a = p₁p₂.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hTripleMain_of_primePairInput (hPP : ChenPrimePairInput) : ∃ (cₘ : ℝ) (N₀ₘ : ℕ), ∀ (N : ℕ), N₀ₘ ≤ N → Even N → ∑ p₁ ∈ Finset.range (correctedChenY N) with Nat.Prime p₁ ∧ correctedChenZ N ≤ p₁, ∑ p₂ ∈ Finset.range (N + 1) with Nat.Prime p₂ ∧ correctedChenY N ≤ p₂, switchingCount N (p₁ * p₂) ≤ cₘ * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

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 by AnalyticNumberTheory, while PanSourceFaithfulSignedMainBound remains 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.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chensTheorem_fully_instantiated {u v : ℕ} (hI : AnalyticNumberTheory.Sieve.PanTypeICharacterMeanValue (fun (N : ℕ) => ↑N) chenPanWeightOne u) (hII : AnalyticNumberTheory.Sieve.PanTypeIICharacterMeanValue (fun (N : ℕ) => ↑N) chenPanWeightOne u v) (hM : AnalyticNumberTheory.Sieve.PanSourceFaithfulSignedMainBound (fun (N : ℕ) => ↑N) chenPanWeightOne u v) (htrunc : CorrectedChenPanTruncationInput) (hPP : ChenPrimePairInput) (hMain : q1MainTermAbsorption) (hErr : q1APErrorUniformBound) (hnum : ∀ (cₘ Cq : ℝ), 0 < Cq → (∃ (N₀ₘ : ℕ), ∀ (N : ℕ), N₀ₘ ≤ N → Even N → ∑ p₁ ∈ Finset.range (correctedChenY N) with Nat.Prime p₁ ∧ correctedChenZ N ≤ p₁, ∑ p₂ ∈ Finset.range (N + 1) with Nat.Prime p₂ ∧ correctedChenY N ≤ p₂, switchingCount N (p₁ * p₂) ≤ cₘ * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) → (∃ (Nq : ℕ), ∀ (N : ℕ), Nq ≤ N → Even N → correctedChenQ1Count N ≤ Cq * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) → 10 / 3 > (cₘ + (Cq + 1 / 2)) / 2) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q