Chen weights and representation counts

Exact divisibility, prime-power and triple-factor weights, historical representation counts, corrected lower cutoffs, and uniform control of the singular-series tail.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

Weight function w(n)

def MathlibNt.SieveTheory.SwitchingPrinciple.exactDiv (q k n : ℕ) : Prop

Exact prime-power divisibility: q^k ∥ n means q^k | n but q^(k+1) ∤ n.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.exactDiv q k n = (q ^ k ∣ n ∧ ¬q ^ (k + 1) ∣ n)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.primePowerSum (n z y : ℕ) : ℝ

Sum of the multiplicities of prime powers exactly dividing n, with primes in [z, y): Σ_{z ≤ q < y, q prime, q^k ∥ n} k.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.primePowerSum n z y = ∑ q ∈ Finset.range y with Nat.Prime q ∧ z ≤ q ∧ ∃ (k : ℕ), 1 ≤ k ∧ MathlibNt.SieveTheory.SwitchingPrinciple.exactDiv q k n, ↑(n.factorization q)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.tripleFactorCount (n z y : ℕ) : ℝ

Triple-factorization count: Σ_{p₁p₂p₃ = n, z ≤ p₁ < y ≤ p₂ ≤ p₃} 1.

Note: the non-strict inequality p₂ ≤ p₃ correctly counts n = q * r² (the case p₂ = p₃ = r). The original condition p₂ < p₃ would omit these factorizations.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.tripleFactorCount n z y = ↑{p₁ ∈ Finset.range (n + 1) | Nat.Prime p₁ ∧ z ≤ p₁ ∧ p₁ < y ∧ ∃ (p₂ : ℕ) (p₃ : ℕ), Nat.Prime p₂ ∧ Nat.Prime p₃ ∧ y ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₁ * p₂ * p₃ = n ∧ p₁ < p₂ ∧ p₂ ≤ p₃}.card

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenWeight (n z y : ℕ) : ℝ

Weight function w(n) (Chen's switching weight):

w(n) = 1 - (1/2) Σ_{z ≤ q < y, q^k ∥ n} k - (1/2) Σ_{p₁p₂p₃=n, z ≤ p₁ < y ≤ p₂ ≤ p₃} 1

If w(n) > 0 and n has no prime factor ≤ z, then n ∈ {1, p, p₁p₂ : p, p₁, p₂ ≥ z}.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenWeight n z y = 1 - 1 / 2 * MathlibNt.SieveTheory.SwitchingPrinciple.primePowerSum n z y - 1 / 2 * MathlibNt.SieveTheory.SwitchingPrinciple.tripleFactorCount n z y

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenWeight_pos_implies_semiprime (n z y : ℕ) (hz : 2 ≤ z) (hy : z < y) (hn : 1 ≤ n) (hn_lt : ↑n < ↑y ^ 3) (h_coprime : ∀ (p : ℕ), Nat.Prime p → p < z → ¬p ∣ n) (hw : 0 < chenWeight n z y) : n = 1 ∨ Nat.Prime n ∨ ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ z ≤ p₁ ∧ z ≤ p₂ ∧ n = p₁ * p₂

w(n) > 0 implies that n is 1, a prime, or a product of two primes, provided n has no prime factor ≤ z and n < y³.

The extra hypothesis n < y³ is needed: if all prime factors of n are ≥ y, then w(n) = 1 > 0, but n ≥ y³ can have three or more prime factors, each ≥ y. The hypothesis n < y³ excludes this case and ensures that n has at most two prime factors.

Definition of W(N)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenWCandidates (N : ℕ) : Finset ℕ

The finite candidate set underlying the working W-count. It is named so that a corrected switching argument can partition its good, bad, and boundary fibres without changing the analytic-facing count all at once.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenWCandidates N = {p ∈ Finset.range N | Nat.Prime p ∧ (∀ (q : ℕ), Nat.Prime q → q ≤ ⌊↑N ^ (1 / 10)⌋₊ → ¬q ∣ N - p) ∧ {q ∈ Finset.range (⌊↑N ^ (1 / 3)⌋₊ + 1) | Nat.Prime q ∧ ⌊↑N ^ (1 / 10)⌋₊ < q ∧ q ≤ ⌊↑N ^ (1 / 3)⌋₊ ∧ q ∣ N - p}.card ≤ 1}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenW (N : ℕ) : ℝ

W(N): the count of primes p satisfying the sieve conditions.

W(N) = |{p prime : N-p has no prime factor ≤ N^(1/10), and at most one prime factor in (N^(1/10), N^(1/3)]}|.

The Jurkat-Richert lower bound gives W(N) ≥ 2.6408 𝔖(N) N/log²N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenW N = ↑(MathlibNt.SieveTheory.SwitchingPrinciple.chenWCandidates N).card

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenW_lower_bound (N : ℕ) (_hN : Even N) (hN_large : 1000 ≤ N) : ∃ (C : ℝ), 2.6408 * chenW N ≥ 2.6408 * 2.6408 * 1 * ↑N / Real.log ↑N ^ 2 - C * ↑N / Real.log ↑N ^ 10

Pointwise remainder interface for the W(N) lower bound.

The error constant in the current linear-sieve interface may depend on the fixed N, so the remainder cannot be removed without a uniformity hypothesis. The genuinely uniform Jurkat--Richert lower bound is included in ChenAnalyticBounds below.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenW_le_primeCount (N : ℕ) : chenW N ≤ ↑(Finset.filter Nat.Prime (Finset.range N)).card

The working chenW is bounded by the number of primes below N.

This is only the filter-inclusion chenW ≤ π(N - 1). It is not a lower bound for Chen representations and is not used by the conditional Chen chain.

Definition of Ω (the switched sum)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenF (N a : ℕ) : ℝ

Indicator f(a): a = p₁p₂ with N^(1/10) < p₁ ≤ N^(1/3) < p₂ ≤ (N/p₁)^(1/2).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenF N a = if ∃ (p₁ : ℕ) (p₂ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ ↑N ^ (1 / 10) < ↑p₁ ∧ ↑p₁ ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) < ↑p₂ ∧ ↑p₂ ≤ (↑N / ↑p₁) ^ (1 / 2) ∧ a = p₁ * p₂ then 1 else 0

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega (N : ℕ) : ℝ

Switched sum Ω:

Ω = Σ_a Σ_{ap₃ ≤ N, N-ap₃ prime} f(a),

where f(a) is the indicator of a = p₁p₂ satisfying the range conditions. For a strict ordered triple, this counts the smaller large-prime pairing once and counts the larger pairing only when it independently satisfies the square cutoff. It therefore has local multiplicity one or two, not uniformly two.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega N = ∑ a ∈ Finset.range (N + 1), MathlibNt.SieveTheory.SwitchingPrinciple.chenF N a * ∑ p₃ ∈ Finset.range (N + 1), if Nat.Prime p₃ ∧ a * p₃ ≤ N ∧ Nat.Prime (N - a * p₃) then 1 else 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega_upper_bound (N : ℕ) (hN : Even N) (hN_large : 1000 ≤ N) : ∃ (C : ℝ), chenOmega N ≤ 3.9404 * 1 * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ 10

Pointwise remainder interface for the Ω upper bound.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenPointwiseAnalyticBoundsAt (N : ℕ) : Prop

The two analytic estimates currently available at one fixed N, with their remainders made explicit. This is deliberately weaker than the uniform Jurkat--Richert/Selberg input needed for Chen's theorem: the errors may still depend on N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenPointwiseAnalyticBoundsAt N = ∃ (errorW : ℝ) (errorOmega : ℝ), 2.6408 * MathlibNt.SieveTheory.SwitchingPrinciple.chenW N ≥ 2.6408 * 2.6408 * 1 * ↑N / Real.log ↑N ^ 2 - errorW ∧ MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega N ≤ 3.9404 * 1 * ↑N / Real.log ↑N ^ 2 + errorOmega

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chen_pointwise_analytic_bounds_at (N : ℕ) (hN : Even N) (hN_large : 1000 ≤ N) : ChenPointwiseAnalyticBoundsAt N

Package the existing pointwise remainder interfaces into an explicit error budget. No uniformity in N is claimed here.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chen_key_inequality_of_error_budget {N : ℕ} {errorW errorOmega : ℝ} (hW : 2.6408 * chenW N ≥ 2.6408 * 2.6408 * 1 * ↑N / Real.log ↑N ^ 2 - errorW) (hO : chenOmega N ≤ 3.9404 * 1 * ↑N / Real.log ↑N ^ 2 + errorOmega) (hbudget : 0 < (2.6408 * 2.6408 - 2.6408 * 3.9404 / 2) * (↑N / Real.log ↑N ^ 2) - errorW - 2.6408 * errorOmega / 2) : chenW N - chenOmega N / 2 > 0

A closed pointwise error budget forces Chen's numerical key inequality.

This isolates the precise analytic work still needed for a uniform theorem: prove that the two remainders fit this strict budget uniformly for all sufficiently large even N.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenAnalyticBounds : Prop

The two analytic estimates required for Chen's theorem, uniform over all sufficiently large N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenAnalyticBounds = ∀ (N : ℕ), Even N → 1000 ≤ N → 2.6408 * MathlibNt.SieveTheory.SwitchingPrinciple.chenW N ≥ 2.6408 * 2.6408 * 1 * ↑N / Real.log ↑N ^ 2 ∧ MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega N ≤ 3.9404 * 1 * ↑N / Real.log ↑N ^ 2

The key inequality

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chen_key_inequality (h_analytic : ChenAnalyticBounds) (N : ℕ) (hN : Even N) (hN_large : 1000 ≤ N) : chenW N - chenOmega N / 2 > 0

Key inequality for Chen's theorem: W(N) - Ω/2 > 0.

W(N) - Ω/2 ≥ (2.6408 - 3.9404/2) 𝔖(N) N/log²N = 0.6706 𝔖(N) N/log²N > 0

Since 𝔖(N) > 0 by positivity of the singular series, W(N) - Ω/2 > 0.

This theorem is only the numerical consequence of the two historical analytic bounds. Turning it into a Chen representation additionally requires a valid counting theorem; the old symmetry argument for chenOmega / 2 is false.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenGoodRepresentations (N : ℕ) : Finset ℕ

Prime candidates already satisfying the conclusion of Chen's theorem.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenGoodRepresentations N = {p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ Nat.IsAtMostAlmostPrime 2 (N - p)}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenWBadCandidates (N : ℕ) : Finset ℕ

The historical W-candidates whose complementary integer is not a P₂.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenWBadCandidates N = {p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.chenWCandidates N | ¬Nat.IsAtMostAlmostPrime 2 (N - p)}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenUnitCandidates (N : ℕ) : Finset ℕ

The unit boundary fibre of the W-candidates.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenUnitCandidates N = {p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.chenWCandidates N | N - p = 1}

theorem MathlibNt.SieveTheory.SwitchingPrinciple.range_sub_eq_one_card_le_one (N : ℕ) : {p ∈ Finset.range N | N - p = 1}.card ≤ 1

The exceptional candidate with N - p = 1 occurs at most once. A corrected switching count must either remove this fibre from chenW or carry this explicit boundary term.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenUnitCandidates_card_le_one (N : ℕ) : (chenUnitCandidates N).card ≤ 1

The unit fibre inside the named W-candidate set also has cardinality at most one.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ (N : ℕ) : ℕ

Corrected lower sieve cutoff. The max 2 removes the small-N degeneracy of the historical floor cutoff.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N = max 2 ⌊↑N ^ (1 / 10)⌋₊

theorem MathlibNt.SieveTheory.SwitchingPrinciple.singularSeriesTruncated_eq_ant (N z : ℕ) : SingularSeries.singularSeriesTruncated N z = AnalyticNumberTheory.Sieve.singularSeriesTruncated N z

The local compatibility copy and the imported analytic truncation are definitionally the same finite Euler product.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenLogZ_upper_bound : ∃ (Clog : ℝ), 0 < Clog ∧ ∀ (N : ℕ), 2 ≤ N → Real.log (↑(correctedChenZ N) - 1) ≤ Clog * Real.log ↑N

Sieve-level logarithmic parameter estimate: there exists Clog > 0 such that for all N ≥ 2, log (z(N) − 1) ≤ Clog · log N, where z(N) = max 2 ⌊N^{1/10}⌋.

One can take Clog = 1/10: z(N) − 1 ≤ N^{1/10} follows from the floor and max bounds, then use monotonicity of log and log(N^{1/10}) = (1/10)·log N.

Uniform lower bound for the truncated singular series: 𝔖_trunc ≥ c·𝔖

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.chenZ_root_large (N : ℕ) (hNbig : 2 ^ 110 < N) : 2 ^ 11 < ↑N ^ (1 / 10)

For N > 2^110, the corrected cutoff z = max 2 ⌊N^{1/10}⌋ satisfies 2^11 < N^{1/10} (real exponent).

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

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

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.chenZ_ge_three (N : ℕ) (hNbig : 2 ^ 110 < N) : 3 ≤ correctedChenZ N

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

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.chenZ_le_N_add_one (N : ℕ) (hN2 : 2 ≤ N) : correctedChenZ N ≤ N + 1

z = max 2 ⌊N^{1/10}⌋ ≤ N + 1 for 2 ≤ N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.chenZ_tail_prime_count_le (N n : ℕ) (hNbig : 2 ^ 110 < N) (hnpos : 0 < n) (hnle : n ≤ N) : {p ∈ Finset.Ico (correctedChenZ N) (N + 1) | Nat.Prime p ∧ p ∣ n}.card ≤ 10

Every positive n ≤ N has at most ten prime divisors in [correctedChenZ N, N] when N > 2^110.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.singularSeries_eq_trunc_mul_tail (N : ℕ) (_hN2 : 2 ≤ N) (hz1 : 1 ≤ correctedChenZ N) (hzleN : correctedChenZ N ≤ N + 1) : SingularSeries.singularSeries N = SingularSeries.singularSeriesTruncated N (correctedChenZ N - 1) * ∏ p ∈ Finset.Ico (correctedChenZ N) (N + 1) with Nat.Prime p, SingularSeries.localFactor p N

𝔖(N) = 𝔖_trunc(N, z−1) · ∏_{z ≤ p ≤ N} localFactor(p, N), the exact tail split used to compare the truncated and full singular series.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.chenZ_tail_prod_le_vanishing (N : ℕ) (hz3 : 3 ≤ correctedChenZ N) : ∏ p ∈ Finset.Ico (correctedChenZ N) (N + 1) with Nat.Prime p, SingularSeries.localFactor p N ≤ (1 + 1 / ↑(correctedChenZ N - 1)) ^ {p ∈ Finset.Ico (correctedChenZ N) (N + 1) | Nat.Prime p ∧ p ∣ N}.card

The same tail product has a bound tending to one: only prime divisors of N enlarge it, and each such factor is at most 1 + 1 / (correctedChenZ N - 1).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.singularSeriesTruncated_lower_bound : ∃ (c : ℝ), 0 < c ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → c * SingularSeries.singularSeries N ≤ SingularSeries.singularSeriesTruncated N (correctedChenZ N - 1)

Uniform lower bound for the truncated singular series: there exist c > 0, N₀ such that for all even N ≥ N₀, c·𝔖(N) ≤ 𝔖_trunc(N, z−1), where z = correctedChenZ N = max 2 ⌊N^{1/10}⌋. This is one of the standard inputs to the main-term lower bound CorrectedChenMainTermLower. The key point is that the tail ∏_{z ≤ p ≤ N} localFactor(p,N) is at most (3/2)^10, since N has at most ten prime factors greater than z.