Switching upper bounds and Chen endpoint assembly

Triple-factor counts are bounded by switched prime counts and Selberg sums. The corrected analytic inputs assemble Chen endpoints. Historical numerical heuristics, failed multiplicity premises, and coarse switching errors remain documented without strengthening their conclusions.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.tripleFactorCount_le_switchingWeight {n z y : ℕ} : tripleFactorCount n z y ≤ ∑ p₁ ∈ Finset.range y with Nat.Prime p₁ ∧ z ≤ p₁, ∑ p₂ ∈ Finset.range (n + 1) with Nat.Prime p₂ ∧ y ≤ p₂, if ∃ (p₃ : ℕ), Nat.Prime p₃ ∧ p₁ * p₂ * p₃ = n then 1 else 0

For each candidate, the triple-factor penalty is at most the switching weight counting (p₁,p₂) pairs. Dropping constraints such as p₁ < p₂ and p₂ ≤ p₃ preserves an upper bound; the equation uniquely determines p₃.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenOmega_triple_le_switchingCount (N : ℕ) : ∑ p ∈ correctedChenCandidates N, tripleFactorCount (N - p) (correctedChenZ N) (correctedChenY 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₂, {p ∈ correctedChenCandidates N | ∃ (p₃ : ℕ), Nat.Prime p₃ ∧ p₁ * p₂ * p₃ = N - p}.card)

Uniform finite expansion of the triple-factor part: its sum over candidates is bounded by the switched count, summing over (p₁,p₂) pairs the number of candidates satisfying p₁p₂p₃ = N-p.

Analytic switching upper bound: the Selberg sieve on the switched set

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieveNu : ArithmeticFunction ℝ

Density on the switched set: ν(d) = 1/d, the proportion of p₃ ≤ x with d | p₃.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieveNu = { toFun := fun (d : ℕ) => 1 / ↑d, map_zero' := MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieveNu._proof_1 }

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieveNu_isMultiplicative : switchingSieveNu.IsMultiplicative

Multiplicativity of switchingSieveNu: 1/(mn) = (1/m)(1/n).

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.switchingSiftingProduct (z : ℕ) : ℕ

Sifting product for the switching sieve: the product of all primes below z.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.switchingSiftingProduct z = (Finset.filter Nat.Prime (Finset.range z)).prod id

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingSiftingProduct_ne_zero (z : ℕ) : switchingSiftingProduct z ≠ 0

The switching sifting product is nonzero.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingSiftingProduct_squarefree (z : ℕ) : Squarefree (switchingSiftingProduct z)

The switching sifting product is squarefree, being a product of distinct primes.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieve (N a : ℕ) : BoundingSieve

Sieve problem on the switched set: support {p₃ ≤ x}, where x = N/a; sieve out multiples of primes q < z, with density ν(d) = 1/d and total mass equal to the support cardinality. The sifted sum is #{p₃ ≤ x : p₃ has no prime factor < z}.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieve N a = { support := Finset.range (N / a + 1), prodPrimes := MathlibNt.SieveTheory.SwitchingPrinciple.switchingSiftingProduct (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N), prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 1, weights_nonneg := MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieve._proof_2, totalMass := ↑(N / a + 1), nu := MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieveNu, nu_mult := MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieveNu_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

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

Switched-set count: for fixed a = p₁p₂, count candidates satisfying a·p₃ = N-p.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount N a = ↑{p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N | ∃ (p₃ : ℕ), Nat.Prime p₃ ∧ a * p₃ = N - p}.card

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount_le_pi (N a : ℕ) (ha : 1 ≤ a) : switchingCount N a ≤ ↑(Finset.filter Nat.Prime (Finset.range (N / a + 1))).card

Prime p₃ counting lemma: for fixed a ≥ 1, switchingCount N a = #{p ∈ C(N) : a·p₃ = N-p, p₃ prime} maps by p ↦ (N-p)/a injectively into the primes p₃ ≤ N/a. Hence

switchingCount N a ≤ #{p ≤ N/a : p prime}.

This is the first step in the triple-factor main-term estimate: the count retains primality of p₃, the elementary source of the 1/log(N/a) density, without a PNT in AP. Distribution of candidates in APs can further sharpen it.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount_eq_zero_of_N_lt_two_mul (N a : ℕ) (hN : N < 2 * a) : switchingCount N a = 0

Region restriction: if N < 2a, a·p₃ = N-p ≤ N has no solution with p₃ ≥ 2, so switchingCount N a = 0. Consequently, pairs with a = p₁p₂ > N/2 contribute zero to the triple-factor main-term sum.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount_sum_eq_zero_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 2 * (p₁ * p₂) ≤ N, switchingCount N (p₁ * p₂)

Region restriction for the triple-factor main term: pairs with a = p₁p₂ > N/2 have switchingCount = 0 by switchingCount_eq_zero_of_N_lt_two_mul. Thus the main-term sum contains only pairs with 2·p₁p₂ ≤ N, precisely the region where the π upper bound (N/a ≥ 2) and subsequent distribution inputs apply.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount_sum_le_pi_sum (N : ℕ) : ∑ 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 2 * (p₁ * p₂) ≤ N, 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 2 * (p₁ * p₂) ≤ N, ↑(Finset.filter Nat.Prime (Finset.range (N / (p₁ * p₂) + 1))).card

π reduction of the triple-factor main term: after restricting the region, each pair satisfies switchingCount N a ≤ #{p ≤ N/a : p prime} by switchingCount_le_pi. Summing gives a main term ≤ Σ_{2p₁p₂ ≤ N} π(N/(p₁p₂)), the elementary target for the triple-factor estimate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingCount_le_siftedSum (N a : ℕ) : switchingCount N a ≤ BoundingSieve.siftedSum

Switching count ≤ sifted sum of the switching sieve: for a candidate p, p₃ = (N-p)/a lies in the support and is coprime to the sifting product. The candidate condition gives no prime factor < z in p₃, since all prime factors of a = p₁p₂ are ≥ z.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieve_mainTerm_eq_primeProduct (N a : ℕ) : (∑ l ∈ (switchingSieve N a).prodPrimes.divisors, BoundingSieve.selbergTerms l)⁻¹ = MertensTheorem.primeProduct (correctedChenZ N - 1)

Switching-sieve main term = Mertens product: (Σ selbergTerms)⁻¹ = ∏_{q<z}(1-1/q) = primeProduct(z-1), since the switching-sieve density is ν(q) = 1/q.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieve_upper_bound (N a : ℕ) : ∃ (w : ℕ → ℝ), w 1 = 1 ∧ BoundingSieve.siftedSum ≤ (switchingSieve N a).totalMass * (∑ l ∈ (switchingSieve N a).prodPrimes.divisors, BoundingSieve.selbergTerms l)⁻¹ + BoundingSieve.errSum (BoundingSieve.lambdaSquared w)

Selberg upper bound for the switching sieve, an unconditional instance: the switched-set sifted sum satisfies ≤ totalMass·(Σ selbergTerms)⁻¹ + errSum(Λ²w*).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieve_upper_bound_optimal (N a : ℕ) : BoundingSieve.siftedSum ≤ (switchingSieve N a).totalMass * (∑ l ∈ (switchingSieve N a).prodPrimes.divisors, BoundingSieve.selbergTerms l)⁻¹ + BoundingSieve.errSum (BoundingSieve.lambdaSquared (AnalyticNumberTheory.Sieve.optimalSelbergWeight (switchingSieve N a)))

Selberg upper bound with explicit optimal weights: as above, using optimalSelbergWeight, namely the unit-bounded Möbius weight.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieveMainErr (N p₁ p₂ : ℕ) : ℝ

Main term plus error for each switched pair: totalMass·primeProduct(z-1) + errSum(Λ²w*).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieveMainErr N p₁ p₂ = (MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieve N (p₁ * p₂)).totalMass * MathlibNt.SieveTheory.MertensTheorem.primeProduct (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N - 1) + BoundingSieve.errSum (BoundingSieve.lambdaSquared (AnalyticNumberTheory.Sieve.optimalSelbergWeight (MathlibNt.SieveTheory.SwitchingPrinciple.switchingSieve N (p₁ * p₂))))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenOmega_triple_le_switchingSieveMainErr (N : ℕ) : ∑ p ∈ correctedChenCandidates N, tripleFactorCount (N - p) (correctedChenZ N) (correctedChenY 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₂, switchingSieveMainErr N p₁ p₂

Triple-factor part: main-term/error decomposition, conditional on the stated inputs. The triple-factor penalty sum is at most the main-term sum plus the error sum, where

• main term: Σ_{p₁,p₂} (N/(p₁p₂)+1)·primeProduct(z-1);
• error: Σ_{p₁,p₂} errSum(Λ²w*), with w* the optimal weight.

This is the structural decomposition for a bound of the form 3.9404·𝔖·N/log²N: the intended main-term inputs are Mertens estimates and numerical integration (Liu Lemma 4), and the error input is weighted Pan control. See the scale warning below.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenOmegaUpperBound_of_analytic_inputs {cₘ Cₚ : ℝ} {N₀ₘ N₀ₚ : ℕ} (hTripleMain : ∀ (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) (hPrimePower : ∀ (N : ℕ), N₀ₚ ≤ N → Even N → ∑ p ∈ correctedChenCandidates N, primePowerSum (N - p) (correctedChenZ N) (correctedChenY N) ≤ Cₚ * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) (hnum : 10 / 3 > (cₘ + Cₚ) / 2) : CorrectedChenOmegaUpperBound

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_chens_theorem_of_omega_inputs {cₘ Cₚ : ℝ} {N₀ₘ N₀ₚ : ℕ} (hPan : ChenWeightedPanInput) (hTripleMain : ∀ (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) (hPrimePower : ∀ (N : ℕ), N₀ₚ ≤ N → Even N → ∑ p ∈ correctedChenCandidates N, primePowerSum (N - p) (correctedChenZ N) (correctedChenY N) ≤ Cₚ * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) (hnum : 10 / 3 > (cₘ + Cₚ) / 2) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Assembly with the corrected statement: weighted Pan input and two analytic inputs (the corrected hTripleMain and hPrimePower) imply Chen's theorem: ∃ N₀, ∀ even N ≥ N₀: N = p + q, with q having at most two prime factors.

The chain is corrected_chens_theorem_of_inputs followed by CorrectedChenOmegaUpperBound_of_analytic_inputs. The remaining hypotheses are analytic: the triple-factor switchingCount estimate and the uniform prime-power bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_chens_theorem_of_q1Count_and_triple {cₘ Cq : ℝ} {N₀ₘ Nq : ℕ} (hPan : ChenWeightedPanInput) (hTripleMain : ∀ (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) (hq1 : ∀ (N : ℕ), Nq ≤ N → Even N → correctedChenQ1Count N ≤ Cq * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) (_hCq : 0 < Cq) (hnum : 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

Final assembly of Chen's theorem: weighted Pan input, the corrected hTripleMain, the q¹ distribution bound, and the numerical condition imply Chen's theorem.

hPrimePower_of_q1Count_bound reduces the prime-power input to the q¹ bound, and properPower_negligible_threshold discharges the negligible proper-power term. This leaves only analytic inputs. On the hPan side, ChenWeightedPanInput is supplied by chenPanInput_of_sourceFaithfulSignedInputs, which uses PanTypeICharacterMeanValue, PanTypeIICharacterMeanValue, and PanSourceFaithfulSignedMainBound with explicit u,v. The exact signed pointwise split is proved internally in AnalyticNumberTheory; PanLogEventuallyLarge and δ₁(0)=0 are instantiated. Once these three analytic inputs and the two analytic bounds (hTripleMain and q¹) are supplied, direct instantiation gives the full proof of corrected_chens_theorem.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_chens_theorem (h : CorrectedChenAnalyticPositivity) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Conditional Chen theorem for the corrected-penalty development. Its unique assumption is precisely CorrectedChenAnalyticPositivity; the finite bridge and representation extraction are valid, but the fixed-level q¹ route to this positivity is numerically obstructed.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenGoodRepresentationLowerBound : Prop

Diagnostic direct lower bound for the public good-representation count. This is stronger than the Jurkat--Richert weighted theorem and is not the canonical literature contract.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenGoodRepresentationLowerBound = ∃ (c : ℝ), 0 < c ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → c * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2 ≤ ↑(MathlibNt.SieveTheory.SwitchingPrinciple.chenGoodRepresentations N).card

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chens_theorem_of_good_representation_lower_bound (hSwitch : ChenGoodRepresentationLowerBound) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

The diagnostic direct good-representation lower bound has a finite consumer: positivity of its explicit main term makes the public good fibre nonempty.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenCountingBridge : Prop

Historical conditional counting bridge for the present chenW/Ω.

This proposition is retained so the conditional theorem has a stable, explicit interface, but it is not an open proof obligation: finite evaluation refutes it for the current definitions (see CHEN_PROOF_ATLAS.md). A future unconditional development must replace both this statement and, where needed, the counting objects with a multiplicity-corrected switching bridge.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenCountingBridge = ∀ (N : ℕ), Even N → 1000 ≤ N → MathlibNt.SieveTheory.SwitchingPrinciple.chenW N - MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega N / 2 ≤ ↑(MathlibNt.SieveTheory.SwitchingPrinciple.chenGoodRepresentations N).card

theorem MathlibNt.SieveTheory.SwitchingPrinciple.key_inequality_implies_chen (h_bridge : ChenCountingBridge) (h_key : ∀ (N : ℕ), Even N → N ≥ 1000 → chenW N - chenOmega N / 2 > 0) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

The key inequality implies Chen's theorem given the exact counting bridge.

W(N) - Ω/2 > 0 means that there is at least one representation N = p + q, where p is prime and q = N-p satisfies the sieve conditions, with at most two prime factors.

Numerical constants

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenW_coefficient : ℝ

W(N) lower-bound coefficient: 2.6408.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenW_coefficient = 2.6408

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega_coefficient : ℝ

Ω upper-bound coefficient: 3.9404.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega_coefficient = 3.9404

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.chen_difference_coefficient : ℝ

Key difference: W(N) - Ω/2 ≥ (2.6408 - 3.9404/2) 𝔖(N) N/log²N = 0.6706 𝔖(N) N/log²N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chen_difference_coefficient = MathlibNt.SieveTheory.SwitchingPrinciple.chenW_coefficient - MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega_coefficient / 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chen_difference_pos : 0 < chen_difference_coefficient

The key difference is positive: 0.6706 > 0.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.sieveF_at_5 : ℝ

Working expression for f(5): 2e^γ · log(5/2) / 5 ≈ 0.6528.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.sieveF_at_5 = 2 * Real.exp Real.eulerMascheroniConstant * Real.log (5 / 2) / 5

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenW_coefficient_simplification : sieveF_at_5 * Real.exp (-Real.eulerMascheroniConstant) = 2 * Real.log (5 / 2) / 5

Source of the W(N) coefficient: 10 · e^(-γ) · f(5) = 4 · log(5/2) ≈ 3.665...

Note: the full W(N) coefficient 2.6408 comes from the precise evaluation of the Jurkat-Richert sieve function f(5), which involves explicit formulas for F(s)/f(s), not a simple algebraic simplification. Here only the cancellation e^γ · e^(-γ) = 1 is verified.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenOmega_coefficient_derivation : 8 * 0.49254 = 3.94032

Source of the M₁ coefficient: 8 · 0.49254 = 3.94032.

6. Historical switching heuristic and its failure

Definition of the switched set B

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.switchedSet (N z y : ℕ) : Finset ℕ

Switched set B: N-p₁p₂p₃, where z ≤ p₁ < y ≤ p₂ ≤ p₃, p₁p₂p₃ < N, (p₁p₂p₃, N) = 1。

This is not the triple-factor object used by tripleFactorCount: it additionally requires coprimality with N and a product less than N, while p₂ < p₃ excludes repeated factors p₂ = p₃. Their exact relationship remains part of the switching bridge to be formalized.

Equations

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

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.switchedSieveSum (N z y : ℕ) : ℝ

Sieve function S(B, P, y) on the switched set B.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.switchedSieveSum N z y = ∑ n ∈ MathlibNt.SieveTheory.SwitchingPrinciple.switchedSet N z y, if ∀ (p : ℕ), Nat.Prime p → p < y → ¬p ∣ n then 1 else 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.switching_identity (N z y : ℕ) (_hz : 2 ≤ z) (_hy : y ≤ N) : ∃ (C : ℝ), 1 / 2 * ↑{n ∈ Finset.range (N + 1) | (∀ (p : ℕ), Nat.Prime p → p < z → ¬p ∣ n) ∧ ∃ (p₁ : ℕ) (p₂ : ℕ) (p₃ : ℕ), Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ Nat.Prime p₃ ∧ z ≤ p₁ ∧ p₁ < y ∧ y ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₁ < p₂ ∧ p₂ < p₃ ∧ n = p₁ * p₂ * p₃}.card = 1 / 2 * switchedSieveSum N z y + C ∧ |C| ≤ ↑N + 1

Unconditional coarse bound for the switching identity: the third term equals (1/2) S(B, P, y) + C, where |C| ≤ N+1.

The former statement claimed O(N^(1/3)), but no switching correspondence between the two current finite-set definitions has been formalized to justify that sharper error. This records the coarse bound obtained because both counts are bounded by range (N+1); the cube-root error requires a separate formalization of the switching principle.

8. Audited proof structures

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSieveProduct_pos_aux (N : ℕ) : 0 ≤ correctedChenSieveProduct N

Nonnegativity of the corrected sieve product: every factor 1 - nu p is positive at a sifting prime.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenJR_ant_lower_bound : AnalyticNumberTheory.Sieve.UniformJurkatRichertLowerBound correctedChenBoundingSieve (fun (N : ℕ) => ↑N ^ (1 / 10)) (fun (N : ℕ) => ↑N ^ (1 / 2)) fun (x : ℝ) => 1

Independent instance of the uniform JR lower bound for the corrected Chen sieve: the ordinary Möbius function is a lower Möbius sequence, and mainSum mu = V exactly. Taking fs = 1 and eta0 = 1/2 gives X*V*(1-1/2) - errSum(1) <= siftedSum.

This independently applies the UniformJurkatRichertLowerBound interface, with uniform quantifiers N₀, eta0 preceding forall N, to recover a lower bound of the same form as correctedChenCandidates_card_ge_X_mul_sieveProduct_sub_errSum.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPositivity_via_jr_ant (hjr : AnalyticNumberTheory.Sieve.UniformJurkatRichertLowerBound correctedChenBoundingSieve (fun (N : ℕ) => ↑N ^ (1 / 10)) (fun (N : ℕ) => ↑N ^ (1 / 2)) fun (x : ℝ) => 1) (hPan : ChenWeightedPanInput) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → 0 < ↑(correctedChenCandidates N).card

Independent positivity route, without Ω: the UniformJurkatRichertLowerBound instance with the exact ordinary Möbius main term, together with weighted Pan control of errSum, gives strictly positive corrected-candidate counts for sufficiently large even numbers:

0 < card(correctedChenCandidates N).

This is parallel to the direct proof using correctedChenCandidates_card_ge_X_mul_sieveProduct_sub_errSum. Here the same lower bound follows through the JR interface, with uniform quantifiers N₀, eta₀ before ∀ N and X·V·(1-eta₀) - errSum(1) ≤ siftedSum = card.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chensTheorem_of_jurkatRichertWeightedLowerBound_and_triplePenalty (hJR : ChenJurkatRichertWeightedLowerBound) (hTriple : ChenJurkatRichertTriplePenaltyUpperBound) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

The canonical JR weighted lower bound reaches Chen's theorem once the remaining genuine strict-triple penalty has its source-scale upper bound.