Varying-prime asymptotics and q¹ penalty distribution

Upper Rosser density and weighted distribution inputs control varying-prime asymptotics. Negligible proper powers reduce the full penalty to q¹ counts; double Möbius identities retain the separate, explicit aggregate-error hypotheses.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

def MathlibNt.SieveTheory.SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma : Prop

The generic dimension-one upper fundamental lemma for the explicit Rosser coefficient. The only analytic input is local: for a sieve whose primes lie below z, at real level Δ and ratio s = log Δ / log z, the Rosser density sum is at most (F(s) + ρ) V(S).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma = ∀ (K ρ : ℝ), 1 < K → 0 < ρ → ∃ (z₀ : ℝ), ∀ (S : BoundingSieve) (z Δ s : ℝ), z₀ ≤ z → 2 ≤ z → 0 < Δ → MathlibNt.SieveTheory.SwitchingPrinciple.HasDimensionOneLocalProductBound S K → (∀ p ∈ S.prodPrimes.primeFactors, ↑p ≤ z) → s = Real.log Δ / Real.log z → 3 / 2 ≤ s → s ≤ 4 → BoundingSieve.mainSum (MathlibNt.SieveTheory.LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditioned_dimensionOneLocalProductBound {N q : ℕ} {K : ℝ} (h : HasDimensionOneLocalProductBound (jurkatRichertSourceBoundingSieve N) K) : HasDimensionOneLocalProductBound (jurkatRichertSourceConditionedBoundingSieve N q) K

Conditioning by q changes only the carrier and total mass, not the sifting product or its local density.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceConditioned_primeFactor_le_cutoff (N q p : ℕ) : p ∈ (jurkatRichertSourceConditionedBoundingSieve N q).prodPrimes.primeFactors → ↑p ≤ ↑N ^ (1 / 10)

Every prime in a conditioned source sieve lies below the literal real sifting cutoff N^(1/10).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceUpperSieveRatio_mem {N q : ℕ} {ε : ℝ} (hN : 1 < N) (hε : 0 < ε) (hεSmall : ε < 1 / 60) (hq : q ∈ jurkatRichertSourceMediumPrimes N) : jurkatRichertSourceUpperSieveRatio N q ε ∈ Set.Icc (3 / 2) 4

For the epsilon range produced by prime-q partial summation, every medium-q upper-sieve ratio lies in the generic fundamental lemma's interval.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQPrimeSumAsymptotic : Prop

Prime-q partial summation for the explicit local-density model. This is the sole interface that evaluates the q-sum, and its conclusion exhibits Chen's exact coefficient 8 * (log 8 + K / 2).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQPrimeSumAsymptotic = ∀ (δ : ℝ), 0 < δ → ∃ (ε : ℝ), 0 < ε ∧ ε < 1 / 60 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, Even N → MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQDensityModel N ε ≤ (8 * (Real.log 8 + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertK / 2) + δ) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertVaryingQPrimeSumAsymptotic : ChenJurkatRichertVaryingQPrimeSumAsymptotic

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertVaryingQUpperDensity_of_fundamentalLemma (hfund : DimensionOneUpperRosserDensityFundamentalLemma) (ε : ℝ) (hε : 0 < ε) (hεSmall : ε < 1 / 60) (δ : ℝ) (hδ : 0 < δ) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → jurkatRichertSourceVaryingQMainSum N ε ≤ jurkatRichertSourceVaryingQDensityModel N ε + δ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

Chen's aggregate upper-density estimate is derived by applying the generic fundamental lemma separately at every medium prime. The additive pointwise errors are summed using the bounded shifted reciprocal-prime mass and the common Mertens density.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQUpperDistribution : Prop

The standard aggregate distribution input for the exact level-D/q remainders. The explicit Rosser coefficient is the weight to which Bombieri--Vinogradov is applied.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQUpperDistribution = ∀ (ε : ℝ), 0 < ε → ε < 1 / 6 → ∀ (δ : ℝ), 0 < δ → ∀ᶠ (N : ℕ) in Filter.atTop, Even N → MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceVaryingQRemainderSum N ε ≤ δ * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertVaryingQUpperDistribution_of_weightedBV (hBV : ChenJurkatRichertVaryingQWeightedBombieriVinogradov) : ChenJurkatRichertVaryingQUpperDistribution

The source-faithful 3^ω-weighted Bombieri--Vinogradov interface implies the exact varying-q upper-distribution statement. The proof expands upperErrSum, uses standard AP errors only on the reduced q ∤ N lanes, and absorbs the nonreduced lanes and source exceptional-prime corrections through the preceding unconditional power-saving theorem.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQUpperSieveStandardInput : Prop

The only two standard analytic inputs for the varying-q upper sieve are the generic dimension-one upper fundamental lemma and the source-faithful weighted Bombieri--Vinogradov estimate. Prime-q partial summation is proved internally.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQUpperSieveStandardInput = (MathlibNt.SieveTheory.SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma ∧ MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov)

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQUpperSieveAsymptotic : Prop

The aggregate upper asymptotic, retained as a derived statement for the weighted-count algebra below.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQUpperSieveAsymptotic = ∀ (η : ℝ), 0 < η → ∀ᶠ (N : ℕ) in Filter.atTop, Even N → MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertSourceMediumPrimeAggregate N ≤ (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertQ1MainCoefficient MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertK + η) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertVaryingQUpperSieveAsymptotic_of_standardInput (hinput : ChenJurkatRichertVaryingQUpperSieveStandardInput) : ChenJurkatRichertVaryingQUpperSieveAsymptotic

The explicit q-conditioned upper Rosser inequalities, the generic density fundamental lemma, unconditional prime-q partial summation, and the distribution estimate derived from weighted Bombieri--Vinogradov recover Chen's coefficient 8 * (log 8 + K / 2).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertDistinctWeightedLowerBound_of_asymptotics (hbase : ChenJurkatRichertBaseLowerSieveAsymptotic) (hupper : ChenJurkatRichertVaryingQUpperSieveStandardInput) : ChenJurkatRichertDistinctWeightedLowerBound

Chen's equations (26)--(27), with the exact finite source weight exposed: the base lower sieve and varying-q upper sieve imply the published distinct weighted lower bound. The elementary integral estimate is internal.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenQ1Count_eq_reindexed (N : ℕ) : correctedChenQ1Count N = ∑ q ∈ Finset.range (correctedChenY N) with Nat.Prime q ∧ correctedChenZ N ≤ q, ↑{p ∈ correctedChenCandidates N | q ∣ N - p}.card

Reindexing the q¹ count: Σ_p #{q ∈ [z,y) : q | N-p} = Σ_{q ∈ [z,y)} #{p ∈ candidates : q | N−p}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenProperPowerSum_le_negligible (N : ℕ) (hNbig : 2 ^ 110 < N) (hEven : Even N) : ∑ p ∈ correctedChenCandidates N, ∑ q ∈ Finset.range (correctedChenY N) with Nat.Prime q ∧ correctedChenZ N ≤ q ∧ q ^ 2 ∣ N - p, ↑((N - p).factorization q) ≤ 60 * ↑N ^ (9 / 10)

Uniform bound for the proper-power part: Σ_p Σ_{q ∈ [z,y), q²|N-p} v_q(N-p) ≤ 60·N^{9/10}, combining multiplicity ≤ 10 with the 6·N^{9/10} counting bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPrimePowerSum_le_q1Count_add_negligible (N : ℕ) (hNbig : 2 ^ 110 < N) (hEven : Even N) : ∑ p ∈ correctedChenCandidates N, primePowerSum (N - p) (correctedChenZ N) (correctedChenY N) ≤ correctedChenQ1Count N + 60 * ↑N ^ (9 / 10)

Reduction of the prime-power penalty sum: for even N > 2^110,

Σ_p primePowerSum(N-p) ≤ q¹ count + 60·N^{9/10},

where the q¹ count = Σ_p #{q ∈ [z,y) : q | N-p} is the only remaining analytic input, to be paired with weighted Pan distribution bounds; the proper-power part is absorbed by 60·N^{9/10}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hPrimePower_of_q1Count_bound (hq1 : ∃ (Cq : ℝ), 0 < Cq ∧ ∃ (Nq : ℕ), ∀ (N : ℕ), Nq ≤ N → Even N → correctedChenQ1Count N ≤ Cq * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) (hneg : ∃ (Nn : ℕ), ∀ (N : ℕ), Nn ≤ N → Even N → 60 * ↑N ^ (9 / 10) ≤ 1 / 2 * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) : ∃ (Cₚ : ℝ), 0 < Cₚ ∧ ∃ (N₀ₚ : ℕ), ∀ (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

Deriving hPrimePower from its inputs: suppose the q¹ count satisfies the uniform upper bound q¹Count(N) ≤ Cq·𝔖_trunc·N/log²N, from a weighted Pan/distribution input, and the proper-power part is negligible. Then hPrimePower holds, namely Σ_p primePowerSum(N−p) ≤ (Cq + 1/2)·𝔖_trunc·N/log²N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.properPower_negligible_threshold : ∃ (Nn : ℕ), ∀ (N : ℕ), Nn ≤ N → Even N → 60 * ↑N ^ (9 / 10) ≤ 1 / 2 * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

Negligibility threshold for proper powers: for sufficiently large even N, 60·N^{9/10} ≤ (1/2)·𝔖_trunc·N/log²N. This follows directly from 𝔖 ≥ 1/2 and the elementary growth bound 240·log²N ≤ N^{1/10}, using log = o(N^{1/20}). It discharges the hneg input of hPrimePower_of_q1Count_bound, leaving only the q¹ distribution bound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertDistinctWeightedCount_sub_proper_le (N : ℕ) (hNbig : 2 ^ 110 < N) (hEven : Even N) : jurkatRichertDistinctWeightedCount N - 30 * ↑N ^ (9 / 10) ≤ jurkatRichertWeightedCount N

Exact finite separation between the literature's distinct-q weight and the valuation-weighted corrected endpoint. Proper powers cost at most 30 * N^(9/10) after the factor 1/2 in the Richert weight.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_correctedChenProperPowerError_le_liuSingularSeries (ρ : ℝ) (hρ : 0 < ρ) : ∀ᶠ (N : ℕ) in Filter.atTop, 60 * ↑N ^ (9 / 10) ≤ ρ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The proper-prime-power error is absorbed into an arbitrary positive multiple of the genuine Liu singular-series main scale. This uses the positive universal Euler-product lower bound, not a fixed q1 coefficient.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertWeightedLowerBound_of_distinct (hJR : ChenJurkatRichertDistinctWeightedLowerBound) : ChenJurkatRichertWeightedLowerBound

The source-faithful distinct-medium-prime theorem produces the canonical valuation-weighted JR endpoint. The finite lower-floor and exceptional-fibre loss is combined with the proper-prime-power loss and absorbed into the main scale; the triple penalty remains outside this theorem.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertWeightedLowerBound_of_asymptotics (hbase : ChenJurkatRichertBaseLowerSieveAsymptotic) (hupper : ChenJurkatRichertVaryingQUpperSieveStandardInput) : ChenJurkatRichertWeightedLowerBound

The complete Chen Lemma 9 analytic producer followed by the proved source-to-valuation correction. Its only inputs are the base lower sieve and the varying-q aggregate upper sieve.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenJurkatRichertWeightedLowerBound_of_literature_inputs (hLowerDensity : DimensionOneLowerRosserDensityFundamentalLemma) (hBV : BombieriVinogradov.StandardBombieriVinogradov) (hUpperDensity : DimensionOneUpperRosserDensityFundamentalLemma) (hWeightedBV : ChenJurkatRichertVaryingQWeightedBombieriVinogradov) : ChenJurkatRichertWeightedLowerBound

Chen's weighted lower bound directly from the four remaining Jurkat--Richert literature inputs. The broader base and varying-q asymptotic predicates remain available as derived APIs, but are not assumptions here.

Conditional q¹ distribution bound and its analytic inputs

This section formulates the q¹ analytic input: the weighted Pan mean-value theorem AnalyticNumberTheory.Sieve.PanMeanValueUniform is assembled by of_sourceFaithfulSignedInputs from two character mean-value bounds and a signed main-term bound (see the Pan bridge). With the required aggregate estimates, the goal is hq1, a uniform upper bound for correctedChenQ1Count N:

q1Count(N) ≤ Cq · 𝔖_trunc(N, z−1) · N/log²N.

The conditional proof chain is:

1. Finite reindexing: correctedChenQ1Count_eq_reindexed turns Σ_p #{q | N-p} into Σ_q #{p ∈ candidates : q | N-p}, for primes q ∈ [z,y).
2. Structural reduction: the candidate AP count is expanded by two layers of Möbius inversion. First, candidates are the unsifted support restricted by coprimality with P_sift. Second, the unsifted support is expanded using the forbidden-prime product P_forb. This reduces to prime-AP base counts q1APBaseCount N m and gives the exact algebraic inequality q1Count ≤ q1MainTermSum N + q1ErrorTermSum N.
3. Main-term absorption: q1MainTermAbsorption bounds the main term using the singular series singularSeriesTruncated and the prime-reciprocal range bound primeReciprocalSum_range_le, absorbing it into C₁·𝔖_trunc·N/log²N.
4. Uniform error bound: q1APErrorUniformBound is an output required of a weighted q¹ aggregate theorem for the full double Möbius error sum. One cannot insert all divisors of the sifting product and their 3^ω-weighted lcm fibers, without truncation, into the classical Pan/Bombieri--Vinogradov theorem, which controls only m ≤ N^(1/2)/log(N)^B.
5. Assembly: hq1_of_q1AnalyticInputs combines these two analytic inputs with elementary logarithmic estimates and 𝔖_trunc ≥ 1/2 to give ∃ Cq Nq, hq1.

Parity: for an even modulus m, the AP base count can contain only p = 2, requiring m | N-2. Thus q1APMainValue uses the exact value, 0 or 1, for even moduli, and the error vanishes by q1APError_even_zero. Odd moduli use the main term li(N)/φ(m). This avoids the degeneracy of the Möbius main term at the r = 2 factor, as in the classical treatment.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1APBaseCount (N m : ℕ) : ℕ

Prime-AP base count for q¹: #{p < N : p prime, 2 ≤ N-p, p ≡ N [MOD m]}.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1APBaseCount N m = {p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ p ≡ N [MOD m]}.card

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

Parity-corrected main term: for even moduli m, the AP base count contains only p = 2 when m | N-2, so use its exact value; for odd moduli use li(N)/φ(m).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1APMainValue N m = if Even m then if m ∣ N - 2 then 1 else 0 else AnalyticNumberTheory.Sieve.logarithmicIntegral ↑N / ↑m.totient

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

q¹ prime-AP error: base count minus main term; zero for even moduli, by q1APError_even_zero.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1APError N m = ↑(MathlibNt.SieveTheory.SwitchingPrinciple.q1APBaseCount N m) - MathlibNt.SieveTheory.SwitchingPrinciple.q1APMainValue N m

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

Candidate AP count: #{p ∈ candidates : q | N-p}.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPCount N q = ↑{p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N | q ∣ N - p}.card

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

Double Möbius expansion of the candidate AP count in terms of base counts.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPDoubleSum N q = ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors, ↑(ArithmeticFunction.moebius d) * ∑ e ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenForbiddenProduct N).divisors, ↑(ArithmeticFunction.moebius e) * ↑(MathlibNt.SieveTheory.SwitchingPrinciple.q1APBaseCount N ((q.lcm d).lcm e))

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

Main term of the candidate AP count, with signed Möbius weights.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPMain N q = ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors, ↑(ArithmeticFunction.moebius d) * ∑ e ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenForbiddenProduct N).divisors, ↑(ArithmeticFunction.moebius e) * MathlibNt.SieveTheory.SwitchingPrinciple.q1APMainValue N ((q.lcm d).lcm e)

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

Signed error sum of the candidate AP count.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPErrorSigned N q = ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors, ↑(ArithmeticFunction.moebius d) * ∑ e ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenForbiddenProduct N).divisors, ↑(ArithmeticFunction.moebius e) * MathlibNt.SieveTheory.SwitchingPrinciple.q1APError N ((q.lcm d).lcm e)

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

Error bound for the candidate AP count, with absolute Möbius weights.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPError N q = ∑ d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors, |↑(ArithmeticFunction.moebius d)| * ∑ e ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenForbiddenProduct N).divisors, |↑(ArithmeticFunction.moebius e)| * |MathlibNt.SieveTheory.SwitchingPrinciple.q1APError N ((q.lcm d).lcm e)|

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

Total q¹ main term: Σ_{q ∈ [z,y), q prime} q1CandidateAPMain N q.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1MainTermSum N = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N) with Nat.Prime q ∧ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N ≤ q, MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPMain N q

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

Total q¹ error: Σ_{q ∈ [z,y), q prime} q1CandidateAPError N q.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1ErrorTermSum N = ∑ q ∈ Finset.range (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N) with Nat.Prime q ∧ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N ≤ q, MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPError N q

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

Möbius coprimality indicator for the sifting product: Σ_{d | P_sift, d | m} μ(d) = 1_{∀ prime r | P_sift: ¬ r | m}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_correctedChenCandidates_iff_coprime_sifting (N p : ℕ) : p ∈ correctedChenCandidates N ↔ p ∈ correctedChenUnsiftedPrimeSupport N ∧ ∀ (r : ℕ), Nat.Prime r → r ∣ correctedChenSiftingProduct N → ¬r ∣ N - p

Candidates are the unsifted support restricted by coprimality with P_sift: p ∈ candidates iff p ∈ unsifted and N-p has no prime factor dividing P_sift.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.candidatesAPCount_eq_unsiftedMoebiusSum (N q : ℕ) : ↑{p ∈ correctedChenCandidates N | q ∣ N - p}.card = ∑ d ∈ (correctedChenSiftingProduct N).divisors, ↑(ArithmeticFunction.moebius d) * ↑{p ∈ correctedChenUnsiftedPrimeSupport N | p ≡ N [MOD q.lcm d]}.card

First Möbius decomposition of the candidate AP count: candidates are the unsifted support restricted by coprimality with P_sift, so #{p ∈ candidates : q | N-p} = Σ_{d | P_sift} μ(d)·#{p ∈ unsifted : p ≡ N [MOD lcm(q,d)]}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPCount_eq_doubleSum (N q : ℕ) : q1CandidateAPCount N q = q1CandidateAPDoubleSum N q

Exact double Möbius expansion of the candidate AP count: A_q = Σ_{d,e} μ(d)μ(e)·base(lcm(q,d,e)).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPCount_le_main_add_error (N q : ℕ) : q1CandidateAPCount N q ≤ q1CandidateAPMain N q + q1CandidateAPError N q

For each q, A_q ≤ main(q) + error(q): split each base count as base = main' + err and bound the signed error sum by absolute values.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1Count_le_mainTerm_add_error (N : ℕ) : correctedChenQ1Count N ≤ q1MainTermSum N + q1ErrorTermSum N

Finite q¹ reduction: q1Count ≤ q1MainTermSum + q1ErrorTermSum, by exact algebra (reindexing, double Möbius expansion, and splitting the base counts).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1APBaseCount_even (N m : ℕ) (hN : Even N) (hN4 : 4 ≤ N) (hm : Even m) : q1APBaseCount N m = if m ∣ N - 2 then 1 else 0

For even moduli, the AP base count contains only p = 2: for even N ≥ 4 and even m, q1APBaseCount N m = 1 if m | N-2, and is zero otherwise.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1APError_even_zero {N m : ℕ} (hN : Even N) (hN4 : 4 ≤ N) (hm : Even m) : q1APError N m = 0

The q¹ error vanishes for even moduli because q1APMainValue uses their exact count.

def MathlibNt.SieveTheory.SwitchingPrinciple.q1MainTermAbsorption : Prop

q¹ main-term absorption, an analytic input: Σ_{q ∈ [z,y)} q1CandidateAPMain N q ≤ C₁·𝔖_trunc·N/log²N.

The main-term structure, from the exact Möbius decomposition q1CandidateAPCount_eq_doubleSum, is q1CandidateAPMain N q = li(N)/φ(q)·∏_{2<r<z}(1-1/(r-1)) + O(parity correction), where li(N) = N/log N. The product is absorbed using the local-factor structure of singularSeriesTruncated and primeReciprocalSum_range_le, the Mertens-type range bound for prime reciprocals, into C₁·𝔖_trunc·N/log²N. This logarithmic absorption is an analytic step and remains an explicit input to the conditional argument; it requires the prime-reciprocal bound and the singular-series product structure.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1MainTermAbsorption = ∃ (C₁ : ℝ), 0 < C₁ ∧ ∃ (N₁ : ℕ), ∀ (N : ℕ), N₁ ≤ N → Even N → MathlibNt.SieveTheory.SwitchingPrinciple.q1MainTermSum N ≤ C₁ * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

def MathlibNt.SieveTheory.SwitchingPrinciple.q1APErrorUniformBound : Prop

Uniform q¹ error bound, an analytic output required of a weighted aggregate theorem: Σ_{q ∈ [z,y)} q1CandidateAPError N q ≤ C₂·N/log³N.

q1CandidateAPError is the double Möbius error sum Σ_q Σ_{d,e} |μ(d)μ(e)|·|err(lcm(q,d,e))|, where err(m) = π'(N;m) - main term. The parity correction in q1APMainValue makes it exactly zero for even moduli; see q1APError_even_zero. The classical Pan theorem gives a μ²(m)3^{ω(m)}-weighted average only for m ≤ N^{1/2}/log(N)^B. This definition retains all divisors d | P_sift and e | P_forb, so lcm(q,d,e) has no such modulus upper bound. This all-positive error interface is retained only for the finite algebraic audit. The canonical route in Q1LevelSupportedSieve first bounds q¹ counts with finite-level Selberg squares, then passes reduced moduli within the cutoff to the weighted Pan/BV input; it no longer uses this definition.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1APErrorUniformBound = ∃ (C₂ : ℝ), 0 < C₂ ∧ ∃ (N₂ : ℕ), ∀ (N : ℕ), N₂ ≤ N → Even N → MathlibNt.SieveTheory.SwitchingPrinciple.q1ErrorTermSum N ≤ C₂ * ↑N / Real.log ↑N ^ 3

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hq1_of_q1AnalyticInputs (hMain : q1MainTermAbsorption) (hErr : q1APErrorUniformBound) : ∃ (Cq : ℝ), 0 < Cq ∧ ∃ (Nq : ℕ), ∀ (N : ℕ), Nq ≤ N → Even N → correctedChenQ1Count N ≤ Cq * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

Conditional hq1 theorem: assume main-term absorption q1MainTermAbsorption and the aggregate error bound q1APErrorUniformBound. The latter is the required Pan-bridge output, not a consequence of PanMeanValueUniform without further truncation control. Then the q¹ count has a uniform bound ∃ Cq Nq: q1Count(N) ≤ Cq·𝔖_trunc·N/log²N, exactly the hq1 input of corrected_chens_theorem_of_q1Count_and_triple.

Assembly: q1Count ≤ Main + Error by q1Count_le_mainTerm_add_error; the main term is ≤ C₁·𝔖·X, and the error is ≤ C₂·N/log³N ≤ (1/4)·N/log²N (errLogCube_negligible) ≤ (1/2)·𝔖·X (𝔖 ≥ 1/2, singularSeriesTruncated_ge_half), so Cq = C₁ + 1/2.