The corrected sieve and the Pan counting bridge

Corrected candidate carriers, Selberg main terms, forbidden-prime products, and Möbius/CRT identities connect finite arithmetic-progression counts to the weighted Pan remainder. Support and truncation hypotheses remain explicit.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

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

Corrected upper switching cutoff. Using a ceiling makes the intended cube-scale coverage an explicit parameter condition rather than a rounding accident.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N = ⌈↑N ^ (1 / 3)⌉₊

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

The base candidates for a replacement switching argument. Unlike the historical W-candidates, the unit fibre is excluded at the definition level. The future analytic lower bound must be proved anew for this object.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N = {p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ ∀ (r : ℕ), Nat.Prime r → r < MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N → ¬r ∣ N - p}

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

Complements used before the corrected sieve removes small primes not already forced away by parity or by a prime factor of N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenUnsiftedComplements N = Finset.image (fun (p : ℕ) => N - p) ({p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ ∀ (r : ℕ), Nat.Prime r → r < MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N → r ≤ 2 ∨ r ∣ N → ¬r ∣ N - p})

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

Product of the small primes which remain to be sieved from the corrected complement support.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N = {r ∈ Finset.range (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N) | Nat.Prime r ∧ 2 < r ∧ ¬r ∣ N}.prod id

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct_squarefree (N : ℕ) : Squarefree (correctedChenSiftingProduct N)

The corrected sifting product is squarefree because its factors are distinct primes.

@[reducible, inline]

noncomputable abbrev MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenNu : ArithmeticFunction ℝ

Goldbach local density for the corrected sieve: the reusable AnalyticNumberTheory density ν(d) = ∏_{p | d} 1/(p-1) (AnalyticNumberTheory.Sieve.goldbachNu).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenNu = AnalyticNumberTheory.Sieve.goldbachNu

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.primeFactors_prod_eq_self {S : Finset ℕ} (hS : ∀ p ∈ S, Nat.Prime p) : (S.prod id).primeFactors = S

The prime factors of a product of distinct primes are exactly the set of those primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct_ne_zero (N : ℕ) : correctedChenSiftingProduct N ≠ 0

The corrected sifting product is nonzero: it is a product of primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct_primeFactors (N : ℕ) : (correctedChenSiftingProduct N).primeFactors = {r ∈ Finset.range (correctedChenZ N) | Nat.Prime r ∧ 2 < r ∧ ¬r ∣ N}

The prime divisors of the corrected sifting product are exactly its factor primes: 2 < r < z with r ∤ N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.prime_dvd_correctedChenSiftingProduct {N p : ℕ} (hp : Nat.Prime p) : p ∣ correctedChenSiftingProduct N ↔ p < correctedChenZ N ∧ 2 < p ∧ ¬p ∣ N

A prime divides the corrected sifting product exactly when it is one of the sieved primes: 2 < p < z and p ∤ N.

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

The corrected Chen sieve as a mathlib BoundingSieve record: the unsifted complements as support, the surviving small-prime product as prodPrimes, unit weights, and the Goldbach local density ν(p) = 1/(p-1).

The total mass is the analytic main term N / log N. With the density identification ν(d) = 1/φ(d) for squarefree d, the remainder rem d = multSum d − ν(d)·N/log N is exactly the congruence-count error that the averaged Pan-type distribution condition (CorrectedChenDistributionCondition) controls; the difference between N/log N and the true support cardinality is absorbed by the main-term constants of the analytic workline, not by the errSum.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenBoundingSieve N = { support := MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenUnsiftedComplements N, prodPrimes := MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N, prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 1, weights_nonneg := MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenBoundingSieve._proof_1, totalMass := ↑N / Real.log ↑N, nu := MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenNu, nu_mult := AnalyticNumberTheory.Sieve.goldbachNu_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenTotalMass_eq (N : ℕ) : (correctedChenBoundingSieve N).totalMass = ↑N / Real.log ↑N

The corrected sieve total mass is the analytic main term N / log N.

Optimal Selberg upper bound and the main-term identities

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

Apply AnalyticNumberTheory.Sieve.selberg_upper_bound_optimal: the sifted sum of the corrected sieve is bounded by totalMass·(Σ selbergTerms)⁻¹ + errSum(Λ²w*). This is an unconditional instance of the classical Selberg upper-bound sieve S ≤ X/G(z) + R for correctedChenBoundingSieve.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSelbergMainTerm_eq_prod (N : ℕ) : (∑ l ∈ (correctedChenBoundingSieve N).prodPrimes.divisors, BoundingSieve.selbergTerms l)⁻¹ = ∏ p ∈ (correctedChenBoundingSieve N).prodPrimes.primeFactors, (1 - correctedChenNu p)

Apply selbergMainTerm_eq_prod_one_sub_nu: the Selberg main term equals the sieve product ∏_{p | P(N)} (1 − ν(p)).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSelbergMainTerm_eq_goldbachSieveProduct (N : ℕ) (hN : Even N) : (∑ l ∈ (correctedChenBoundingSieve N).prodPrimes.divisors, BoundingSieve.selbergTerms l)⁻¹ = MertensTheorem.goldbachSieveProduct N (correctedChenZ N)

The main-term sieve product equals MertensTheorem.goldbachSieveProduct N z. For even N, the factor at p = 2 is excluded on both sides by p ∤ N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSelbergMainTerm_eq_primeProduct_mul_singularSeries (N : ℕ) (hN : Even N) : (correctedChenBoundingSieve N).totalMass * (∑ l ∈ (correctedChenBoundingSieve N).prodPrimes.divisors, BoundingSieve.selbergTerms l)⁻¹ = ↑N / Real.log ↑N * MertensTheorem.primeProduct (correctedChenZ N - 1) * SingularSeries.singularSeriesTruncated N (correctedChenZ N - 1)

Main-term identity: totalMass·(Σ selbergTerms)⁻¹ = (N/log N)·primeProduct(z−1)·𝔖_trunc(N, z−1), the exact application of sieveProduct_identity to the Selberg main term.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.coprime_correctedChenSiftingProduct_iff {N a : ℕ} : (correctedChenSiftingProduct N).Coprime a ↔ ∀ (r : ℕ), Nat.Prime r → r < correctedChenZ N → 2 < r → ¬r ∣ N → ¬r ∣ a

An element is coprime to the corrected sifting product exactly when no sieved prime (that is, no prime 2 < r < z with r ∤ N) divides it.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftedComplements_eq_correctedCandidate_image (N : ℕ) : {a ∈ correctedChenUnsiftedComplements N | (correctedChenSiftingProduct N).Coprime a} = Finset.image (fun (p : ℕ) => N - p) (correctedChenCandidates N)

The small-prime sieve leaves exactly the corrected candidates: an unsifted complement survives the sieve precisely when its prime partner lies in the corrected candidate set.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftedCard_eq_correctedCandidateCard (N : ℕ) : {a ∈ correctedChenUnsiftedComplements N | (correctedChenSiftingProduct N).Coprime a}.card = (correctedChenCandidates N).card

The number of unsifted complements that survive the corrected sieve is exactly the number of corrected candidates.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenBoundingSieve_siftedSum_eq_card (N : ℕ) : BoundingSieve.siftedSum = ↑(correctedChenCandidates N).card

The BoundingSieve sifted sum for the corrected Chen sieve is exactly the corrected candidate count.

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

The prime support of the unsifted complements: primes p < N whose complement is at least two and carries no r ≤ 2 or r | N prime divisor below z. It is the preimage of the sieve support under p ↦ N - p.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenUnsiftedPrimeSupport N = {p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ ∀ (r : ℕ), Nat.Prime r → r < MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N → r ≤ 2 ∨ r ∣ N → ¬r ∣ N - p}

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

Forbidden-prime product for the Pan bridge: F(N) = ∏_{r < z, r prime, r ≤ 2 ∨ r | N} r. The support condition ∀ r < z: (r ≤ 2 ∨ r | N) → ¬ r | N−p is exactly (N−p, F(N)) = 1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenForbiddenProduct N = {r ∈ Finset.range (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N) | Nat.Prime r ∧ (r ≤ 2 ∨ r ∣ N)}.prod id

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenForbiddenProduct_squarefree (N : ℕ) : Squarefree (correctedChenForbiddenProduct N)

The forbidden-prime product is squarefree, being a product of distinct primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenForbiddenProduct_ne_zero (N : ℕ) : correctedChenForbiddenProduct N ≠ 0

The forbidden-prime product is nonzero.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenForbiddenProduct_primeFactors (N : ℕ) : (correctedChenForbiddenProduct N).primeFactors = {r ∈ Finset.range (correctedChenZ N) | Nat.Prime r ∧ (r ≤ 2 ∨ r ∣ N)}

Its set of prime factors is exactly the filtered set of primes.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.prime_dvd_correctedChenForbiddenProduct_iff {N r : ℕ} (hr : Nat.Prime r) : r ∣ correctedChenForbiddenProduct N ↔ r < correctedChenZ N ∧ (r ≤ 2 ∨ r ∣ N)

Characterization of r | F(N): r is prime, r < z, and (r ≤ 2 ∨ r | N).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_correctedChenUnsiftedPrimeSupport_iff_coprime (N p : ℕ) : p ∈ correctedChenUnsiftedPrimeSupport N ↔ Nat.Prime p ∧ 2 ≤ N - p ∧ ∀ (r : ℕ), Nat.Prime r → r ∣ correctedChenForbiddenProduct N → ¬r ∣ N - p

Coprimality characterization of support for the Pan bridge: p ∈ support ⟺ p.Prime ∧ 2 ≤ N−p ∧ ∀ prime r | F(N): ¬ r | N−p.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.moebius_coprime_sum_forbidden (N m : ℕ) : (∑ e ∈ (correctedChenForbiddenProduct N).divisors, if e ∣ m then ↑(ArithmeticFunction.moebius e) else 0) = if ∀ (r : ℕ), Nat.Prime r → r ∣ correctedChenForbiddenProduct N → ¬r ∣ m then 1 else 0

Möbius coprimality indicator for the Pan bridge: Σ_{e | F(N), e | m} μ(e) = 1_{∀ prime r | F(N): ¬ r | m}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.unsiftedPrimeSupport_AP_count_eq_moebiusSum (N d : ℕ) : ↑{p ∈ correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card = ∑ e ∈ (correctedChenForbiddenProduct N).divisors, ↑(ArithmeticFunction.moebius e) * ↑{p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ p ≡ N [MOD d] ∧ e ∣ N - p}.card

Möbius decomposition of the support AP count for the Pan bridge: the inner count in Chen's distribution condition expands as a Möbius-weighted sum of prime-AP base counts over forbidden-prime divisors. Each base count is then linked to primesInAPBelow/panDistributionError.

The Pan bridge: lcm merging and compatibility of congruences

theorem MathlibNt.SieveTheory.SwitchingPrinciple.modEq_and_dvd_complement_iff_modEq_lcm {N p d e : ℕ} (hp : p < N) : p ≡ N [MOD d] ∧ e ∣ N - p ↔ p ≡ N [MOD d.lcm e]

Merging congruences (the compatible CRT case): for p < N, p ≡ N [MOD d] and e ∣ N-p hold exactly when p ≡ N [MOD lcm d e]. This justifies replacing the inner condition of unsiftedPrimeSupport_AP_count_eq_moebiusSum, p ≡ N [MOD d] ∧ e | N-p, by the single modulus lcm(d,e): e | N-p is equivalent to p ≡ N [MOD e] by prime_dvd_complement_iff_modEq. The congruences have the same residue N, so they are automatically compatible; coprimality of d,e is unnecessary.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.unsiftedPrimeSupport_AP_count_lcm_merge (N d e : ℕ) : {p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ p ≡ N [MOD d] ∧ e ∣ N - p}.card = {p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ p ≡ N [MOD d.lcm e]}.card

Counting form of lcm merging: the inner count in the Möbius decomposition, #{p < N : p ≡ N [MOD d] ∧ e | N-p}, becomes #{p < N : p ≡ N [MOD lcm(d,e)]}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.unsiftedPrimeSupport_AP_count_eq_moebiusSum_lcm (N d : ℕ) : ↑{p ∈ correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card = ∑ e ∈ (correctedChenForbiddenProduct N).divisors, ↑(ArithmeticFunction.moebius e) * ↑{p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ p ≡ N [MOD d.lcm e]}.card

lcm form of the Möbius decomposition: as in unsiftedPrimeSupport_AP_count_eq_moebiusSum, but with each inner base count merged using lcm(d,e). The count #{p < N : p ≡ N [MOD lcm(d,e)]} is exactly the input to the a=1 Pan distribution error via primesInAPBelow_one/panDistributionError_one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenUnsiftedComplements_eq_image (N : ℕ) : correctedChenUnsiftedComplements N = Finset.image (fun (p : ℕ) => N - p) (correctedChenUnsiftedPrimeSupport N)

The unsifted complement support is definitionally the image of the prime support under p ↦ N - p.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenMultSum_eq_multiples_card (N d : ℕ) : BoundingSieve.multSum d = ↑{a ∈ correctedChenUnsiftedComplements N | d ∣ a}.card

The corrected sieve multSum is the number of support elements divisible by d.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenMultiples_card_eq_primeSupport (N d : ℕ) : {a ∈ correctedChenUnsiftedComplements N | d ∣ a}.card = {p ∈ correctedChenUnsiftedPrimeSupport N | d ∣ N - p}.card

Counting the multiples of d in the sieve support is the same as counting the prime-support partners with d ∣ N - p.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenMultSum_eq_modEq_count (N d : ℕ) : BoundingSieve.multSum d = ↑{p ∈ correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card

The corrected sieve distribution count is the number of prime-support partners congruent to N modulo d. This is the finite seam at which a Bombieri--Vinogradov/Pan input bounds multSum and hence errSum.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenRem_eq_modEq_count (N d : ℕ) : BoundingSieve.rem d = ↑{p ∈ correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card - correctedChenNu d * (correctedChenBoundingSieve N).totalMass

The corrected sieve remainder at d is the prime-support congruence count minus the density main term.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenErrSum_eq_modEq (N : ℕ) (muPlus : ℕ → ℝ) : BoundingSieve.errSum muPlus = ∑ d ∈ (correctedChenSiftingProduct N).divisors, |muPlus d| * |↑{p ∈ correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card - correctedChenNu d * (correctedChenBoundingSieve N).totalMass|

The corrected sieve errSum is the sum over sieve divisors of the absolute congruence-count error. This is the exact finite form that a uniform distribution estimate must bound.

def MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenDistributionCondition : Prop

The uniform Bombieri--Vinogradov-style distribution condition required by the corrected sieve: for every A > 0 there is a uniform C such that the 3^{ω(d)}-weighted sum over sieve divisors of the congruence-count errors is at most C · N/log^A N, uniformly for all sufficiently large even N.

This is the averaged Pan form, not a per-modulus bound: the individual errors do not sum to a log^{-A} bound because the divisor count of the sifting product is exponential in z. The local bombieri_vinogradov interface in BombieriVinogradov.lean is only its fixed-parameter remainder form; this averaged target is what actually bounds the corrected sieve's errSum (see correctedChenErrSum_le_panWeighted).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenDistributionCondition = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 1000 ≤ N → Even N → ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors, 3 ^ d.primeFactors.card * |↑{p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card - MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenNu d * (↑N / Real.log ↑N)| ≤ C * ↑N / Real.log ↑N ^ A

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenErrSum_le_panWeighted (N : ℕ) : (BoundingSieve.errSum fun (x : ℕ) => 1) ≤ ∑ d ∈ (correctedChenSiftingProduct N).divisors, 3 ^ d.primeFactors.card * |↑{p ∈ correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card - correctedChenNu d * (correctedChenBoundingSieve N).totalMass|

The counting-sieve errSum is bounded by the 3^{ω(d)}-weighted congruence-error sum controlled by CorrectedChenDistributionCondition.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenErrSum_uniform_of_distribution {A : ℝ} (hA : 0 < A) (N : ℕ) (hN : 1000 ≤ N) (hEven : Even N) (hdist : CorrectedChenDistributionCondition) : ∃ (C : ℝ), 0 < C ∧ (BoundingSieve.errSum fun (x : ℕ) => 1) ≤ C * ↑N / Real.log ↑N ^ A

Given the averaged Pan-type distribution condition, the counting-sieve errSum of the corrected sieve is uniformly O(N / log^A N). This closes the errSum line conditionally on the single analytic input CorrectedChenDistributionCondition.

Applying the weighted Pan--Bombieri--Vinogradov input

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenWeightedPanInput : Prop

The reusable AnalyticNumberTheory weighted Pan-BV input (AnalyticNumberTheory.Sieve.WeightedPanCondition) instantiated at the corrected Chen sieve: x N = N, S N = correctedChenBoundingSieve N, w d = 3^{ω(d)}. This is exactly the input formalized in analytic-number-theory-lean, issue #7.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenWeightedPanInput = AnalyticNumberTheory.Sieve.WeightedPanCondition (fun (N : ℕ) => ↑N) MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenBoundingSieve fun (d : ℕ) => 3 ^ d.primeFactors.card

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPanSum_eq_weightedPanRemainder (N : ℕ) : ∑ d ∈ (correctedChenSiftingProduct N).divisors, 3 ^ d.primeFactors.card * |↑{p ∈ correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD d]}.card - correctedChenNu d * (↑N / Real.log ↑N)| = AnalyticNumberTheory.Sieve.weightedPanRemainder (correctedChenBoundingSieve N) fun (d : ℕ) => 3 ^ d.primeFactors.card

The corrected sieve's weighted Pan sum is weightedPanRemainder: the congruence-count error at d is exactly the BoundingSieve remainder rem d = multSum d − ν(d)·N/log N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenDistributionCondition_iff_chenWeightedPanInput : CorrectedChenDistributionCondition ↔ ChenWeightedPanInput

Applying the weighted Pan-BV input: the corrected sieve's distribution condition is exactly WeightedPanCondition instance.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenErrSum_le_weightedPanInput (N : ℕ) : (BoundingSieve.errSum fun (x : ℕ) => 1) ≤ AnalyticNumberTheory.Sieve.weightedPanRemainder (correctedChenBoundingSieve N) fun (d : ℕ) => 3 ^ d.primeFactors.card

The counting-sieve errSum is bounded by the weighted Pan remainder: apply the reusable errSum_le_threeOmegaWeightedPanRemainder at the corrected Chen instance.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenErrSum_uniform_of_weightedPanInput {A : ℝ} (hA : 0 < A) (N : ℕ) (hN : 1000 ≤ N) (hEven : Even N) (hinput : ChenWeightedPanInput) : ∃ (C : ℝ), 0 < C ∧ (BoundingSieve.errSum fun (x : ℕ) => 1) ≤ C * ↑N / Real.log ↑N ^ A

Given the weighted Pan-BV input, the corrected sieve's errSum is uniformly O(N / log^A N), the remainder bound formulated in analytic-number-theory-lean, issue #7.

Completing the Pan bridge: PanMeanValueUniform ⇒ ChenWeightedPanInput

This section proves only the finite bridge from the a = 1 base count to correctedChenBoundingSieve.rem. It does not represent the general p₁p₂ weights in Liu's eqn-adef, and therefore does not treat the noncoprime R₁ in eqn-r0. At the end, the source-faithful signed API is used to assemble PanMeanValueUniform; the paper's R₁ and the signed main-term bound remain explicit analytic inputs.

@[reducible, inline]

abbrev MathlibNt.SieveTheory.SwitchingPrinciple.chenPanWeightOne (a : ℕ) : ℝ

The a=1 weight for the Pan bridge: f(1) = 1 and zero elsewhere, reducing panDistributionSum to the a = 1 distribution error Δ(y; 1, q, l).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenPanWeightOne a = if a = 1 then 1 else 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.supportAPBaseCount_eq_primesInAPBelow (N q : ℕ) (hN : 2 ≤ N) : {p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ p ≡ N [MOD q]}.card = AnalyticNumberTheory.Sieve.primesInAPBelow (N - 2) 1 q (N % q)

Base count = the a=1 Pan scaled count: #{p < N : p prime, 2 ≤ N-p, p ≡ N [MOD q]} is exactly primesInAPBelow (N-2) 1 q (N % q), the a = 1 case of Liu 2022 §II, and the input side of primesInAPBelow_one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.supportAPBaseCount_distributionError (N q : ℕ) (hN : 2 ≤ N) : ↑{p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ p ≡ N [MOD q]}.card - AnalyticNumberTheory.Sieve.logarithmicIntegral (↑N - 2) / ↑q.totient = AnalyticNumberTheory.Sieve.panDistributionError (N - 2) 1 q (N % q)

The distribution error of the base count equals the a=1 Pan distribution error: (baseCount q) − li(N−2)/φ(q) = panDistributionError (N−2) 1 q (N % q), namely Δ(N-2; 1, q, N mod q) = π(N-2; q, N mod q) - li(N-2)/φ(q).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenRem_eq_moebiusBaseCount (N d : ℕ) (hd : d ∣ correctedChenSiftingProduct N) : BoundingSieve.rem d = ∑ e ∈ (correctedChenForbiddenProduct N).divisors, ↑(ArithmeticFunction.moebius e) * ↑{p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ p ≡ N [MOD d.lcm e]}.card - 1 / ↑d.totient * (↑N / Real.log ↑N)

Exact remainder under Möbius decomposition (factor-by-factor decomposition): for d | P(N), rem d = Σ_{e | F(N)} μ(e)·baseCount(lcm(d,e)) − li(N)/φ(d), where baseCount(q) = #{p < N : p prime, 2 ≤ N-p, p ≡ N [MOD q]} is the prime-AP base count. On the main-term side, ν(d) = 1/φ(d) for squarefree d | P, and totalMass = N/log N = li(N).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.panDistributionSum_one_eq_distributionError (y X q l : ℕ) (hX : 1 ≤ X) : AnalyticNumberTheory.Sieve.panDistributionSum y X q l chenPanWeightOne = AnalyticNumberTheory.Sieve.panDistributionError y 1 q l

For the a=1 weight, panDistributionSum reduces to panDistributionError.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenPanWeightOne_eq_zero_of_not_coprime {a q : ℕ} (hcop : ¬a.Coprime q) : chenPanWeightOne a = 0

The delta weight has no non-coprime contribution. This proves why the a = 1 bridge bypasses, rather than estimates, Liu's general-f R₁.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenPanWeightOne_noncoprimeSum_eq_zero (y X q l : ℕ) : (∑ a ∈ Finset.range (X + 1), if ¬a.Coprime q then chenPanWeightOne a * AnalyticNumberTheory.Sieve.panDistributionError y a q l else 0) = 0

The entire finite non-coprime lane vanishes for chenPanWeightOne.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenPanWeightOne_fullSum_eq_distributionError (y X q l : ℕ) (hX : 1 ≤ X) : ∑ a ∈ Finset.range (X + 1), chenPanWeightOne a * AnalyticNumberTheory.Sieve.panDistributionError y a q l = AnalyticNumberTheory.Sieve.panDistributionError y 1 q l

The unrestricted finite sum also collapses to the a = 1 base-count error. Together with the preceding theorem, this is the exact scope of the delta-weight bridge.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.coprime_siftingProduct_N (N : ℕ) : (correctedChenSiftingProduct N).Coprime N

The sifting product is coprime to N: each prime factor of P(N) satisfies r ∤ N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.moebius_sq_eq_one_of_squarefree {d : ℕ} (hd : Squarefree d) : ↑(ArithmeticFunction.moebius d) ^ 2 = 1

For a squarefree modulus, μ(d)² = 1, since μ(d) = ±1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.panMaxL_nonneg (y X q : ℕ) (f : ℕ → ℝ) : 0 ≤ AnalyticNumberTheory.Sieve.panMaxL y X q f

panMaxL is nonnegative: it is a maximum of absolute values, or zero.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.panMaxY_nonneg (X q x : ℕ) (f : ℕ → ℝ) : 0 ≤ AnalyticNumberTheory.Sieve.panMaxY X q x f

panMaxY is nonnegative.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_distributionError_le_panMaxY_of_coprime (N d : ℕ) (hN : 2 ≤ N) (hd0 : d ≠ 0) (hcop : (N % d).Coprime d) : |AnalyticNumberTheory.Sieve.panDistributionError (N - 2) 1 d (N % d)| ≤ AnalyticNumberTheory.Sieve.panMaxY N d ⌊↑N⌋₊ chenPanWeightOne

The delta-one distribution error at any reduced residue is bounded by Pan's two nested maxima.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_distributionError_le_panMaxY (N d : ℕ) (hd : d ∣ correctedChenSiftingProduct N) (hN : 2 ≤ N) : |AnalyticNumberTheory.Sieve.panDistributionError (N - 2) 1 d (N % d)| ≤ AnalyticNumberTheory.Sieve.panMaxY N d ⌊↑N⌋₊ chenPanWeightOne

Pan control of the distribution error: for d | P(N), |Δ(N-2; 1, d, N mod d)| ≤ panMaxY N d N (a=1 weight). The modulus d is coprime to N, since its prime factors divide P and do not divide N. Thus (N mod d, d) = 1 places the residue in unitResidues d, the range of the panMaxL maximum. This statement also covers d = 1, whose unique canonical residue is 0.

def MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenPanTruncationInput : Prop

Support/truncation input: the part of Chen's remainder not covered by the modulus sum q ≤ x^{1/2}/log^B x in the weighted Pan mean-value theorem consists of the errors |Δ'(d)| for large moduli d > D and for d = 1, together with |rem d - Δ'(d)|. The latter includes the Möbius correction Σ_{1≠e|F} μ(e)·baseCount(lcm(d,e)) and the main-term difference (li(N)-li(N-2))/φ(d). These are uniformly bounded by C·N/log^A N. Classical sources: the support truncation in Pan 1963 / Halberstam--Richert Ch. 10. This is the Möbius support correction for the a = 1 base count, not the R₁ for general p₁p₂ weights in Liu 2022 eqn-r0; the latter remains a separate open input. Its proof, involving Titchmarsh-type averages and prime-AP counts for large moduli, is a research-level input.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenPanTruncationInput = ∀ (A : ℝ), 0 < A → ∀ (B : ℝ), ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℕ), ∀ (N : ℕ), x₀ ≤ N → Even N → ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors, 3 ^ d.primeFactors.card * |BoundingSieve.rem d - AnalyticNumberTheory.Sieve.panDistributionError (N - 2) 1 d (N % d)| + ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors with ¬(2 ≤ d ∧ d ≤ ⌊↑N ^ (1 / 2) / Real.log ↑N ^ B⌋₊), 3 ^ d.primeFactors.card * |AnalyticNumberTheory.Sieve.panDistributionError (N - 2) 1 d (N % d)| ≤ C * ↑N / Real.log ↑N ^ A

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPanSum_reduction (N : ℕ) (hN : 1000 ≤ N) (B : ℝ) : ∑ d ∈ (correctedChenSiftingProduct N).divisors, 3 ^ d.primeFactors.card * |BoundingSieve.rem d| ≤ ∑ q ∈ Finset.range (⌊↑N ^ (1 / 2) / Real.log ↑N ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panMaxY N q ⌊↑N⌋₊ chenPanWeightOne + ∑ d ∈ (correctedChenSiftingProduct N).divisors, 3 ^ d.primeFactors.card * |BoundingSieve.rem d - AnalyticNumberTheory.Sieve.panDistributionError (N - 2) 1 d (N % d)| + ∑ d ∈ (correctedChenSiftingProduct N).divisors with ¬(2 ≤ d ∧ d ≤ ⌊↑N ^ (1 / 2) / Real.log ↑N ^ B⌋₊), 3 ^ d.primeFactors.card * |AnalyticNumberTheory.Sieve.panDistributionError (N - 2) 1 d (N % d)|

Reduction of Chen's weighted remainder sum: for N ≥ 1000 and any B, Σ_{d | P(N)} 3^{ω(d)}·|rem d| ≤ PanSum(N,B) + Trunc(N,B), where PanSum is the panMaxY-weighted modulus sum in PanMeanValueUniform, controlled by hpan, and Trunc comprises the two remainder terms controlled by CorrectedChenPanTruncationInput: |rem d - Δ'(d)| and |Δ'(d)| for uncovered moduli.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_rem_le_const_mul_N (N d : ℕ) (hN : 1000 ≤ N) (hd : d ∣ correctedChenSiftingProduct N) : |BoundingSieve.rem d| ≤ (1 + 1 / Real.log 1000) * ↑N

Trivial remainder bound: for d | P(N) and N ≥ 1000, |rem d| ≤ (1 + 1/log 1000)·N, using support cardinality ≤ N and ν(d) = 1/φ(d) ≤ 1, N/logN ≤ N/log 1000).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.threeOmegaDivisorSum_le_sixOmega (P : ℕ) (hP : Squarefree P) (hP0 : P ≠ 0) : ∑ d ∈ P.divisors, 3 ^ d.primeFactors.card ≤ 6 ^ P.primeFactors.card

Divisor sum: for squarefree P, Σ_{d | P} 3^{ω(d)} ≤ 6^{ω(P)}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.threeOmegaDivisorSum_siftingProduct_le_sixPowZ (N : ℕ) : ∑ d ∈ (correctedChenSiftingProduct N).divisors, 3 ^ d.primeFactors.card ≤ 6 ^ correctedChenZ N

Weighted divisor sum for the sifting product: Σ_{d | P(N)} 3^{ω(d)} ≤ 6^{z(N)}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ_le_of_le (N x₀ : ℕ) (hNx : N ≤ x₀) : correctedChenZ N ≤ correctedChenZ x₀

z(N) ≤ z(x₀) for N ≤ x₀, by monotonicity of the real power and the floor.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPanSum_small_bound (N x₀ : ℕ) (hN : 1000 ≤ N) (hNx : N ≤ x₀) : ∑ d ∈ (correctedChenSiftingProduct N).divisors, 3 ^ d.primeFactors.card * |BoundingSieve.rem d| ≤ 6 ^ correctedChenZ x₀ * ((1 + 1 / Real.log 1000) * ↑N)

Trivial remainder-sum bound on the small-N interval 1000 ≤ N < x₀: Σ_{d | P(N)} 3^{ω(d)}·|rem d| ≤ 6^{z(x₀)}·(1 + 1/log 1000)·N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPanInput_of_panMeanValueUniform (hpan : AnalyticNumberTheory.Sieve.PanMeanValueUniform (fun (N : ℕ) => ↑N) chenPanWeightOne) (htrunc : CorrectedChenPanTruncationInput) : ChenWeightedPanInput

The a = 1 base-count bridge: the delta-weight instance of the classical weighted Pan mean-value theorem, together with the support/truncation input, implies ChenWeightedPanInput for the current sieve. This theorem does not identify this remainder with Liu's general-f paper R. The reduction correctedChenPanSum_reduction gives Chen's remainder sum Σ_d 3^{ω(d)}|rem d| ≤ PanSum + Trunc. The term PanSum is controlled by hpan (PanMeanValueUniform), while Trunc is controlled by htrunc (CorrectedChenPanTruncationInput); the finite range N < x₀ is absorbed using the trivial bound. The source-faithful assembly is PanMeanValueUniform.of_sourceFaithfulSignedInputs, which explicitly takes PanSourceFaithfulSignedMainBound; the exact signed pointwise decomposition is already proved in AnalyticNumberTheory. Here only the statement PanMeanValueUniform is used directly.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenPanInput_of_sourceFaithfulSignedInputs {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) : ChenWeightedPanInput

Source-faithful Pan wrapper: PanMeanValueUniform.of_sourceFaithfulSignedInputs combines two character mean-value bounds, the signed-main inverse-log bound with explicit u,v, the proved logarithmic growth estimate, and δ₁(0)=0 into PanMeanValueUniform. Adding support truncation yields ChenWeightedPanInput. The exact signed pointwise decomposition is an internal theorem of AnalyticNumberTheory, not a hypothesis; the paper's R₁ and PanSourceFaithfulSignedMainBound remain open inputs.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates_card_ge_mainSum_sub_errSum (N : ℕ) (muMinus : ℕ → ℝ) (hmu : AnalyticNumberTheory.Sieve.IsLowerMoebius muMinus) : (correctedChenBoundingSieve N).totalMass * BoundingSieve.mainSum muMinus - BoundingSieve.errSum muMinus ≤ ↑(correctedChenCandidates N).card

The corrected candidate count is at least the lower-sieve main term minus the explicit errSum: the finite seam through which a uniform Jurkat--Richert lower bound for mainSum μ⁻ (with the closed N / log N total mass) proves CorrectedChenAnalyticPositivity.