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) #
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)
Instances For
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
Instances For
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
Instances For
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) #
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
Instances For
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
Instances For
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.
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) #
Indicator f(a): a = p₁p₂ with N^(1/10) < p₁ ≤ N^(1/3) < p₂ ≤ (N/p₁)^(1/2).
Equations
Instances For
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
Instances For
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
Instances For
Package the existing pointwise remainder interfaces into an explicit error
budget. No uniformity in N is claimed here.
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.
The two analytic estimates required for Chen's theorem, uniform over all sufficiently large N.
Equations
Instances For
The key inequality #
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.
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)}
Instances For
The historical W-candidates whose complementary integer is not a P₂.
Equations
Instances For
The unit boundary fibre of the W-candidates.
Equations
Instances For
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.
The unit fibre inside the named W-candidate set also has cardinality at most one.
Corrected lower sieve cutoff. The max 2 removes the small-N
degeneracy of the historical floor cutoff.
Instances For
The local compatibility copy and the imported analytic truncation are definitionally the same finite Euler product.
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·𝔖 #
z = max 2 ⌊N^{1/10}⌋ lies above N^{1/10}/2 for N > 2^110.
z = max 2 ⌊N^{1/10}⌋ ≥ 3 for N > 2^110.
z = max 2 ⌊N^{1/10}⌋ ≤ N + 1 for 2 ≤ 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.
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).
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.