AnalyticNumberTheory.Sieve.PanVaughanPointwise

Pointwise Vaughan decomposition and analytic main-term interfaces

This module contains the finite algebra connecting PanAssembly.PanVaughanPointwiseSplit to the pointwise proposition PanChebyshevApprox. That proposition is an assumption in the reduction, not a universally valid estimate; the counterexamples and corrected signed block below explain the necessary qualifications.

The finite steps are:

1. An all-n Vaughan identity, extending the v < n form by the correction −(if n ≤ v then Λ n else 0).
2. AP sums apMiddle and apSmall.
3. The exact identity apVonMangoldt y q l = apV1 y q l u − apMiddle y q l u v + apV3 y q l u v + apSmall y q l v and its triangle bound |apVonMangoldt| ≤ |apV1| + |apV3| + |apMiddle| + |apSmall|.
4. The same decomposition after coprime scaling by a (panWeightedVonMangoldt_abs_le), retaining the signed middle/small block under one absolute value.
5. The pointwise proposition PanChebyshevApprox, with the AP Chebyshev/main-term comparison as its analytic content.
6. The finite max-composition implication PanChebyshevApprox → PanVaughanPointwiseSplit.

The exact prime-count identity is π(y;q,l) = Σ_{n≤y,n≡l(q)} Λ(n)/log n − primePowerCorrection. apLogVonMangoldt, apPrimePowerCorrection, and apLogVonMangoldt_eq_primesInAP_add_pp implement this identity; the correction is nonnegative. The prime evaluation vonMangoldt_eq_log_of_prime reuses mathlib's ArithmeticFunction.vonMangoldt_apply_prime.

The log-weighted Vaughan decomposition yields panDistributionSum_eq_mainStep, under f 0 = 0, and the conditional reduction PanChebyshevApprox.of_mainStep. Neither the unrestricted original PanChebyshevApprox nor the universally quantified pure-li PanChebyshevMainStep is valid: explicit counterexamples are proved below. The corrected shape retains middle/small and li in a single signed block and keeps the prime-power correction explicit.

These identities do not prove the necessary uniform analytic main-term comparison. The classical route uses AP distribution, partial summation, suitable weight/support bounds, and the large sieve; the genuine logarithmic integral must also be distinguished from the x/log x proxy defined in PrimeNumberTheorem. See Pan 1963, Halberstam--Richert 1974 Ch. 10, and Liu 2022 §II--III.

In PanAssembly, PanVaughanPointwiseSplitSigned and PanSignedMainTermBound feed PanMeanValueUniform.of_signedAnalyticInputs. The pure-li split feeds only PanVaughanSplitCrude. Even a small Moebius tail Σ_{d>u} μ(d)/d does not turn a positive pure-li block into a logarithmic saving: the schematic aggregate (x/log x)·(1+log X)·log³Q is too large. The classical signed comparison has the shape |Σ f(a)·((apSmall−apMiddle)/log(y/a)−li(y/a)/φ(q))|, with the log-normalized identity treated exactly below. Coprimality, harmonic-sum control for the Chen weights, and subtraction of the sieve main term remain essential. See PanMainTermSieveBound, PanMainSieveAbsorption, and PAN_PROOF_ATLAS.md; the pure-li route establishes only the separate coarse polylogarithmic bound.

1. The Vaughan identity for all n

theorem AnalyticNumberTheory.Sieve.vaughanIdentity_threeTerm_general (n u v : ℕ) : vaughanFirst n u - vaughanMiddle n u v + vaughanThird n u v = if v < n then ArithmeticFunction.vonMangoldt n else 0

All-n Vaughan identity: for any n u v : ℕ, Λ n = vaughanFirst n u − vaughanMiddle n u v + vaughanThird n u v + (if n ≤ v then Λ n else 0). The existing vaughanIdentity_threeTerm covers v < n; vaughanFullSecondSum identifies the small-range correction, which combines with vaughanIdentity to give the all-n form. This form can be summed over APs without imposing v < n.

2. AP middle and small terms

noncomputable def AnalyticNumberTheory.Sieve.apMiddle (y q l u v : ℕ) : ℝ

AP sum of the Type I' middle term: Σ_{n≤y, n≡l [MOD q]} vaughanMiddle n u v. This counts the contribution from a ≤ u and b ≤ v in Vaughan's identity.

Equations

• AnalyticNumberTheory.Sieve.apMiddle y q l u v = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then AnalyticNumberTheory.Sieve.vaughanMiddle n u v else 0

noncomputable def AnalyticNumberTheory.Sieve.apSmall (y q l v : ℕ) : ℝ

AP sum of the small-factor exception: Σ_{n≤y, n≡l [MOD q], n≤v} Λ n. It occurs because the uncorrected Vaughan identity assumes v < n.

Equations

• AnalyticNumberTheory.Sieve.apSmall y q l v = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then if n ≤ v then ArithmeticFunction.vonMangoldt n else 0 else 0

3. Finite Vaughan decomposition of apVonMangoldt

theorem AnalyticNumberTheory.Sieve.apVonMangoldt_eq_pieces (y q l u v : ℕ) : apVonMangoldt y q l = apV1 y q l u - apMiddle y q l u v + apV3 y q l u v + apSmall y q l v

Exact AP Vaughan decomposition: apVonMangoldt y q l = apV1 y q l u − apMiddle y q l u v + apV3 y q l u v + apSmall y q l v for arbitrary y q l u v.

theorem AnalyticNumberTheory.Sieve.apVonMangoldt_abs_le_pieces (y q l u v : ℕ) : |apVonMangoldt y q l| ≤ |apV1 y q l u| + |apV3 y q l u v| + |apMiddle y q l u v| + |apSmall y q l v|

Triangle bound for the AP decomposition: |apVonMangoldt y q l| ≤ |apV1 y q l u| + |apV3 y q l u v| + |apMiddle y q l u v| + |apSmall y q l v|. In the weighted refinement, the middle/small difference is kept together for comparison with the main term.

4. Weighted triangle decomposition after absorbing a

theorem AnalyticNumberTheory.Sieve.panWeightedVonMangoldt_abs_le (y X q l u v : ℕ) (f : ℕ → ℝ) : |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * apVonMangoldt (y / a) q (natInvMod q a * l % q) else 0| ≤ |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * apV1 (y / a) q (natInvMod q a * l % q) u else 0| + |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * apV3 (y / a) q (natInvMod q a * l % q) u v else 0| + |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (apSmall (y / a) q (natInvMod q a * l % q) v - apMiddle (y / a) q (natInvMod q a * l % q) u v) else 0|

Weighted Vaughan decomposition after absorbing a: the coprime scaled AP sum satisfies `|Σ f(a)·apVonMangoldt(y/a,q,l·a⁻¹)| ≤ |Σ f(a)·apV1(y/a,q,l·a⁻¹)|

• |Σ f(a)·apV3(y/a,q,l·a⁻¹)|
• |Σ f(a)·(−apMiddle+apSmall)(y/a,q,l·a⁻¹)|`. This is the finite algebra underlying the analytic Chebyshev/main-term comparison.

5. Pointwise comparison proposition PanChebyshevApprox

def AnalyticNumberTheory.Sieve.PanChebyshevApprox (f : ℕ → ℝ) (u v : ℕ) : Prop

Pointwise Chebyshev/main-term comparison proposition: for all X,q,y,l with q > 0 and (l,q)=1, `|panDistributionSum y X q l f| ≤ |panPieceSum (fun y q l => apV1 y q l u / log y)|

• |panPieceSum (fun y q l => apV3 y q l u v / log y)|
• |panPieceSum (fun y q l => li y / φ(q))|`, with the common outer parameters suppressed.

The intended comparison starts from the AP Chebyshev relation π(y;q,l)·log y ≈ Σ_{n≤y,n≡l(q)} Λ(n) and Vaughan's Type I, Type II, and middle/small decomposition (Liu 2022 §III Theorem 2; Halberstam--Richert 1974 Ch. 10). The zero-index term, relevant only at q=1, and real-versus- natural quotient rounding also have to be handled. Here li is the working x/log x proxy.

This proposition is only an assumption in the coarse reduction. not_PanChebyshevApprox_of_f0 disproves its unrestricted form. Furthermore, the pure-li block cannot supply inverse-log decay: the outer sum Σ_{q≤Q} μ²(q)3^{ω(q)}/φ(q) grows polylogarithmically, while positive choices such as f=1 leave the inner main term of the indicated y·log X/(φ(q)log y) size in suitable ranges. An arbitrary signed sum cannot be lower-bounded by its absolute majorant; the positive example is enough to exhibit the obstruction. See PanMainTerm and the corrected block in PanChebyshevApproxCorrected and panDistributionSum_abs_le_logPieces_mainBlock.

Equations

• AnalyticNumberTheory.Sieve.PanChebyshevApprox f u v = ∀ (X q y l : ℕ), 0 < q → l.Coprime q → |AnalyticNumberTheory.Sieve.panDistributionSum y X q l f| ≤ |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y| + |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y| + |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q x : ℕ) => AnalyticNumberTheory.Sieve.logarithmicIntegral ↑y / ↑q.totient|

6. Finite composition of the residue and truncation maxima

theorem AnalyticNumberTheory.Sieve.panMaxL_le_pieces_sum (y X q : ℕ) (f : ℕ → ℝ) (g1 g2 g3 : ℕ → ℕ → ℕ → ℝ) (h : ∀ (l : ℕ), l.Coprime q → |panDistributionSum y X q l f| ≤ |panPieceSum y X q l f g1| + |panPieceSum y X q l f g2| + |panPieceSum y X q l f g3|) : panMaxL y X q f ≤ panPieceMaxL y X q f g1 + panPieceMaxL y X q f g2 + panPieceMaxL y X q f g3

Residue-max reduction: a pointwise (y,l) estimate gives panMaxL ≤ the sum of the three panPieceMaxL bounds. All maxima are finite and use unitResidues q, with zero for an empty residue set.

theorem AnalyticNumberTheory.Sieve.panMaxY_le_pieces_sum (X q x : ℕ) (f : ℕ → ℝ) (g1 g2 g3 : ℕ → ℕ → ℕ → ℝ) (h : ∀ (y' l : ℕ), l.Coprime q → |panDistributionSum y' X q l f| ≤ |panPieceSum y' X q l f g1| + |panPieceSum y' X q l f g2| + |panPieceSum y' X q l f g3|) : panMaxY X q x f ≤ panPieceMaxY X q x f g1 + panPieceMaxY X q x f g2 + panPieceMaxY X q x f g3

Truncation-max reduction: a pointwise (y,l) estimate gives panMaxY ≤ the sum of the three panPieceMaxY bounds by finite max composition.

7. Reduction to PanVaughanPointwiseSplit

theorem AnalyticNumberTheory.Sieve.PanVaughanPointwiseSplit.of_chebyshevApprox {x f : ℕ → ℝ} {u v : ℕ} (h : PanChebyshevApprox f u v) : PanVaughanPointwiseSplit x f u v

The pointwise proposition PanChebyshevApprox implies PanVaughanPointwiseSplit by finite max composition. This conditional reduction does not prove the assumed estimate. It introduces no extra logarithm-positivity assumption: the log-normalized pieces are passed unchanged to the finite maximum lemmas.

8. Exact AP prime-count identity and the main-step reduction

The exact Chebyshev identity is π(y;q,l) = Σ_{n≤y,n≡l(q)} Λ(n)/log n − Σ_{p^k≤y,k≥2,p^k≡l(q)} 1/k. Together with Vaughan's identity, it exposes the middle/small block whose cancellation against the main term is analytic, not finite algebra.

PrimeNumberTheorem.logarithmicIntegral is the proxy x/log x, not the actual logarithmic integral. The identity below does not use PNT-AP, but an analytic main-term estimate must account for this distinction and cannot treat the proxy as an exact prime-count main term with arbitrary logarithmic savings.

noncomputable def AnalyticNumberTheory.Sieve.apLogVonMangoldt (y q l : ℕ) : ℝ

Log-normalized AP von Mangoldt sum: Σ_{n≤y,n≡l [MOD q]} Λ(n)/log n. Primes contribute 1 and powers p^k, k ≥ 2, contribute 1/k. Removing the latter gives π(y;q,l).

Equations

• AnalyticNumberTheory.Sieve.apLogVonMangoldt y q l = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then ArithmeticFunction.vonMangoldt n / Real.log ↑n else 0

noncomputable def AnalyticNumberTheory.Sieve.apPrimePowerCorrection (y q l : ℕ) : ℝ

Prime-power correction: Σ_{p^k≤y,k≥2,p^k≡l [MOD q]} 1/k. The implementation sums over nonprime n with von Mangoldt weight; non-prime-powers contribute zero.

Equations

• AnalyticNumberTheory.Sieve.apPrimePowerCorrection y q l = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then if Nat.Prime n then 0 else ArithmeticFunction.vonMangoldt n / Real.log ↑n else 0

theorem AnalyticNumberTheory.Sieve.vonMangoldt_eq_log_of_prime {p : ℕ} (hp : Nat.Prime p) : ArithmeticFunction.vonMangoldt p = Real.log ↑p

For prime p, Λ p = log p, by mathlib's prime evaluation.

theorem AnalyticNumberTheory.Sieve.vonMangoldt_nonneg (n : ℕ) : 0 ≤ ArithmeticFunction.vonMangoldt n

The von Mangoldt function is nonnegative.

theorem AnalyticNumberTheory.Sieve.apPrimePowerCorrection_nonneg (y q l : ℕ) : 0 ≤ apPrimePowerCorrection y q l

The prime-power correction is nonnegative.

theorem AnalyticNumberTheory.Sieve.apLogVonMangoldt_eq_primesInAP_add_pp (y q l : ℕ) : apLogVonMangoldt y q l = ↑(primesInAP y q l) + apPrimePowerCorrection y q l

Exact AP Chebyshev identity: primesInAP y q l = apLogVonMangoldt y q l − apPrimePowerCorrection y q l. This is finite algebra and counting, with no analytic input.

theorem AnalyticNumberTheory.Sieve.apLogVonMangoldt_eq_primesInAPBelow_inv (y a q l : ℕ) (ha : 0 < a) (hcop : a.Coprime q) : apLogVonMangoldt (y / a) q (natInvMod q a * l % q) = ↑(primesInAPBelow y a q l) + apPrimePowerCorrection (y / a) q (natInvMod q a * l % q)

Chebyshev identity after absorbing a: if (a,q)=1 and a ≥ 1, primesInAPBelow y a q l = apLogVonMangoldt(y/a,q,l·a⁻¹) − apPrimePowerCorrection(y/a,q,l·a⁻¹).

noncomputable def AnalyticNumberTheory.Sieve.apV1Log (y q l u : ℕ) : ℝ

Log-weighted form of the Type I piece.

Equations

• AnalyticNumberTheory.Sieve.apV1Log y q l u = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then AnalyticNumberTheory.Sieve.vaughanFirst n u / Real.log ↑n else 0

noncomputable def AnalyticNumberTheory.Sieve.apV3Log (y q l u v : ℕ) : ℝ

Log-weighted form of the Type II (V3) piece.

Equations

• AnalyticNumberTheory.Sieve.apV3Log y q l u v = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then AnalyticNumberTheory.Sieve.vaughanThird n u v / Real.log ↑n else 0

noncomputable def AnalyticNumberTheory.Sieve.apMiddleLog (y q l u v : ℕ) : ℝ

Log-weighted form of the Type I' middle term.

Equations

• AnalyticNumberTheory.Sieve.apMiddleLog y q l u v = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then AnalyticNumberTheory.Sieve.vaughanMiddle n u v / Real.log ↑n else 0

noncomputable def AnalyticNumberTheory.Sieve.apSmallLog (y q l v : ℕ) : ℝ

Log-weighted form of the small-factor exception.

Equations

• AnalyticNumberTheory.Sieve.apSmallLog y q l v = ∑ n ∈ Finset.range (y + 1), if n ≡ l [MOD q] then (if n ≤ v then ArithmeticFunction.vonMangoldt n else 0) / Real.log ↑n else 0

theorem AnalyticNumberTheory.Sieve.apLogVonMangoldt_eq_logPieces (y q l u v : ℕ) : apLogVonMangoldt y q l = apV1Log y q l u - apMiddleLog y q l u v + apV3Log y q l u v + apSmallLog y q l v

Log-weighted Vaughan decomposition: apLogVonMangoldt = apV1Log − apMiddleLog + apV3Log + apSmallLog. This follows by dividing the pointwise identity by log n and summing.

theorem AnalyticNumberTheory.Sieve.panDistributionSum_abs_le_primes_li (y X q l : ℕ) (f : ℕ → ℝ) : |panDistributionSum y X q l f| ≤ |∑ a ∈ Finset.range (X + 1), if a.Coprime q then f a * ↑(primesInAPBelow y a q l) else 0| + |∑ a ∈ Finset.range (X + 1), if a.Coprime q then f a * (logarithmicIntegral (↑y / ↑a) / ↑q.totient) else 0|

Triangle reduction: |panDistributionSum| ≤ |prime-count sum| + |li main-term sum|. This is the coarse separation used in the original comparison; it does not supply the signed main-term cancellation.

Exact main-step identity and its conditional reduction

theorem AnalyticNumberTheory.Sieve.panDistributionSum_eq_mainStep (y X q l : ℕ) (f : ℕ → ℝ) (hf0 : f 0 = 0) : panDistributionSum y X q l f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (apLogVonMangoldt (y / a) q (natInvMod q a * l % q) - logarithmicIntegral (↑y / ↑a) / ↑q.totient) - f a * apPrimePowerCorrection (y / a) q (natInvMod q a * l % q) else 0

Exact main-step identity: if f 0 = 0, then panDistributionSum is Σ_{(a,q)=1} f(a)·(V1Log − MiddleLog + V3Log + SmallLog − PrimePowerCorrection − li((y:ℝ)/a)/φ(q)). This is finite algebra via the scaled Chebyshev identity. The condition f 0 = 0 removes the zero-index exception: primesInAPBelow y 0 q l need not agree with the AP expression at y/0 = 0, which cannot represent its prime count.

def AnalyticNumberTheory.Sieve.PanChebyshevMainStep (f : ℕ → ℝ) (u v : ℕ) : Prop

Pure-li main-step proposition: for q > 0 and (l,q)=1, |Σ f·(Λlog−li_ℝ/φ)| + Σ |f|·PPC ≤ |panPieceSum(V1/log)| + |panPieceSum(V3/log)| + |panPieceSum(li_ℤ/φ)|, where the sums run over 1 ≤ a ≤ X, (a,q)=1, Λlog = apLogVonMangoldt(y/a,q,a⁻¹l), and the pieces divide by log(y/a), not by a fixed log u. For given f,u,v, this can be assumed to obtain a conditional reduction. It is not valid for all f,u,v: not_PanChebyshevMainStep supplies a counterexample. The intended comparison treats the middle/small terms, prime powers, and the real/natural li rounding difference using Moebius inversion and PNT-level estimates (Liu 2022 §III Theorem 2; Halberstam--Richert 1974 Ch. 10). The finite decomposition does not establish those comparisons or validate this pure-li right side.

Equations

• AnalyticNumberTheory.Sieve.PanChebyshevMainStep f u v = ∀ (X q y l : ℕ), 0 < q → l.Coprime q → (|∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (AnalyticNumberTheory.Sieve.apLogVonMangoldt (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) - AnalyticNumberTheory.Sieve.logarithmicIntegral (↑y / ↑a) / ↑q.totient) else 0| + ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then |f a| * AnalyticNumberTheory.Sieve.apPrimePowerCorrection (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0) ≤ |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1 y q l u / Real.log ↑y| + |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3 y q l u v / Real.log ↑y| + |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q x : ℕ) => AnalyticNumberTheory.Sieve.logarithmicIntegral ↑y / ↑q.totient|

theorem AnalyticNumberTheory.Sieve.PanChebyshevApprox.of_mainStep {f : ℕ → ℝ} {u v : ℕ} (hf0 : f 0 = 0) (hms : PanChebyshevMainStep f u v) : PanChebyshevApprox f u v

Conditional reduction to PanChebyshevApprox: PanChebyshevMainStep and f 0 = 0 imply PanChebyshevApprox, by panDistributionSum_eq_mainStep. No analytic estimate is proved by this substitution.

theorem AnalyticNumberTheory.Sieve.not_PanChebyshevApprox_of_f0 : ¬PanChebyshevApprox (fun (a : ℕ) => if a = 0 then 1 else 0) 0 0

Zero-index counterexample to unrestricted PanChebyshevApprox: take f = 1_{a=0}, X=1, q=1, y=2, l=0. The left side is 1, since primesInAPBelow 2 0 1 0 = 1 (only the prime 2 is counted), whereas the right side is 0. At a=0, each piece uses the natural quotient y/a = 0, so the Type I, Type II, and pure-li pieces vanish. Thus the scaled identity requires a condition such as f 0 = 0.

theorem AnalyticNumberTheory.Sieve.panDistributionSum_abs_le_logPieces_mainBlock (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : |panDistributionSum y X q l f| ≤ |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * apV1Log (y / a) q (natInvMod q a * l % q) u else 0| + |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * apV3Log (y / a) q (natInvMod q a * l % q) u v else 0| + |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (apMiddleLog (y / a) q (natInvMod q a * l % q) u v - apSmallLog (y / a) q (natInvMod q a * l % q) v + logarithmicIntegral (↑y / ↑a) / ↑q.totient) else 0| + ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then |f a| * apPrimePowerCorrection (y / a) q (natInvMod q a * l % q) else 0

Corrected third block, as an exact structural bound: the identities above give `|panDistributionSum| ≤ |Σ f·V1Log| + |Σ f·V3Log|

• |Σ f·(MiddleLog−SmallLog+li((y:ℝ)/a)/φ)|
• Σ |f|·PPC. The third block must retain the middle/small terms and liunder the same absolute value. A pure|Σ f·li/φ|` replacement cannot capture their cancellation.

9. The corrected signed middle/small and li block

The natural exact third block is |Σ f·(MiddleLog−SmallLog+li((y:ℝ)/a)/φ)|. The earlier pure-li block panPieceSum (fun y' => li(y')/φ(q)) cannot absorb the signed middle/small terms by itself. panDistributionSum_abs_le_logPieces_mainBlock proves the exact triangle decomposition. The propositions below distinguish the subsequent analytic comparisons from that finite result.

def AnalyticNumberTheory.Sieve.PanChebyshevApproxCorrected (f : ℕ → ℝ) (u v : ℕ) : Prop

Corrected comparison proposition in panPieceSum form: use the third piece `apMiddleLog y' q l' u v − apSmallLog y' q l' v

• logarithmicIntegral y'/φ(q)and an explicit prime-power correction. The Type I and Type II pieces here are alreadyapV1LogandapV3Log. Relating the exact corrected-block bound to this form requires f 0 = 0and control of the conversion from real division inli((y:ℝ)/a)to the natural quotient in `panPieceSum. The classical main-term comparison also uses li(x) = x/log x + O(x/log²x)` for the genuine logarithmic integral; that relation does not identify the proxy with it. These are additional inputs, not consequences of the definition.

Equations

• AnalyticNumberTheory.Sieve.PanChebyshevApproxCorrected f u v = ∀ (X q y l : ℕ), 0 < q → l.Coprime q → |AnalyticNumberTheory.Sieve.panDistributionSum y X q l f| ≤ |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV1Log y q l u| + |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apV3Log y q l u v| + |AnalyticNumberTheory.Sieve.panPieceSum y X q l f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apMiddleLog y q l u v - AnalyticNumberTheory.Sieve.apSmallLog y q l v + AnalyticNumberTheory.Sieve.logarithmicIntegral ↑y / ↑q.totient| + ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then |f a| * AnalyticNumberTheory.Sieve.apPrimePowerCorrection (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) else 0

def AnalyticNumberTheory.Sieve.PanMainTermAbsorbedBound (x f : ℕ → ℝ) (u v : ℕ) : Prop

Corrected main-term bound T3', an analytic-input proposition: the 3^{ω(q)}-weighted maximum sum of the combined li + middle − small block is bounded by C·x/log^A x, with constants preceding all sufficiently large X. This replaces the pure-li PanMainTermBound. The intended classical mechanism is the comparison ψ(x;q,l)/log x ≈ li(x)/φ(q), matching the smooth Vaughan contributions to x/φ(q) and cancelling at the x/log x scale (Halberstam--Richert 1974 Ch. 10; Liu 2022 §III). The remainder estimate O(x/log^A x) is analytic input, not a conclusion proved by this proposition.

Equations

• AnalyticNumberTheory.Sieve.PanMainTermAbsorbedBound x f u v = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → (∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panPieceMaxY X q ⌊x X⌋₊ f fun (y q l : ℕ) => AnalyticNumberTheory.Sieve.apMiddleLog y q l u v - AnalyticNumberTheory.Sieve.apSmallLog y q l v + AnalyticNumberTheory.Sieve.logarithmicIntegral ↑y / ↑q.totient) ≤ C * x X / Real.log (x X) ^ A

10. Exact main-step decomposition and a counterexample

The results above identify both the exact third block and the failure caused by allowing f 0 ≠ 0. This section also gives an explicit counterexample to universal PanChebyshevMainStep.

Exact decomposition and analytic limitations

panDistributionSum_eq_mainStep gives Σ f·(V1Log−MiddleLog+V3Log+SmallLog−PPC−li((y:ℝ)/a)/φ). The main-step left side instead majorizes the prime powers: |Σ f·(Λlog−li_ℝ/φ)| + Σ |f|·PPC. Finite algebra does not control this by |panPieceSum(V1/log)| + |panPieceSum(V3/log)| + |panPieceSum(li_ℤ/φ)| for arbitrary f,u,v, even with f 0 = 0. Signed weights can cancel the pure-li sum while leaving the middle/small contribution nonzero. Separating two large main terms by the triangle inequality also loses the cancellation needed for logarithmic savings. The exact prime-count statement is panDistributionSum_abs_le_logPieces_mainBlock; panChebyshevMainStepLHS_abs_le_corrected gives the matching bound for the main-step left side.

The separate analytic requirements are:

1. Small term: SmallLog_a = π(min(y/a,v);q,a⁻¹l) + PPC(min(y/a,v);q,a⁻¹l). This is the small-range version of apLogVonMangoldt_eq_primesInAP_add_pp. If v=o(y/a), its prime-count main term is expected to be small relative to li(y/a)/φ(q) in an appropriate AP range. If y/a ≤ v, it is the whole log-normalized AP sum and PNT-AP would compare it with li(y/a)/φ(q).
2. Middle term and Moebius tails: the heuristic after Moebius inversion has the shape MiddleLog_a ≈ (y/a/φ(q))·Σ_{d≤u}μ(d)/d·(1+o(1)). The PNT-equivalent cancellation Σ_{d≤u}μ(d)/d → 0 and a quantitative tail estimate are relevant. Neither this heuristic nor an o(li) bound follows from the finite identity; uniformity, truncation, and the logarithmic normalization have to be justified.
3. Prime powers: the proposed estimate PPC(y/a) = O(sqrt(y/a)·log(y/a)) = o(li(y/a)) at large arguments concerns prime-power counting. Its Σ |f|·PPC and modulus aggregates need separate bounds.
4. Quotient rounding: the real division in li((y:ℝ)/a) differs from the natural quotient in panPieceSum. The proposed real-analysis estimate is |li_ℝ−li_ℤ| ≤ 3/log(y/a) for the t/log t proxy, in a suitable range bounded away from the singular point 1. The necessary range and small-argument exceptions must be stated; the estimate is not an unrestricted identity.

Even an asymptotic main block of size li_ℝ/φ(q)·(1+o(1)) is not itself an inverse-log error. After weighting by the Chen coefficients, subtraction of the sieve main term and quantitative uniform remainders are needed to reach the target PanMainTermAbsorbedBound.

The remaining counterexample is not just a sign heuristic. Take X=2, q=1, y=4, l=0, u=4, v=0, and f(1)=c, f(2)=−c, with c=2/log 2 and f=0 otherwise. For the proxy li(t)=t/log t, li(4)=li(2)=c, so the pure-li piece vanishes. The left side is 2c, while the right side is c·log 3/(2 log 2) < 2c. The strict inequality is log 3 < log 16 = 4 log 2. This disproves the universally quantified main-step proposition despite f 0 = 0. More generally, the cancellation choice f(1)=li(⌊y/2⌋), f(2)=−li(⌊y⌋) at X=2,q=1 annuls the pure-li block without annulling Σ |f|·PPC. For u ≥ y, apV1 = apVonMangoldt and apV3 = 0 throughout the relevant sums.

Requirements for the corrected analytic route

PanChebyshevApproxCorrected and PanMainTermAbsorbedBound state comparisons with the combined signed third block. They separate finite algebra from the analytic estimates; they are not proofs of those estimates.

1. PNT-AP or Siegel--Walfisz: a suitable uniform version of π(x;q,l) = li(x)/φ(q) + O(x/(φ(q)log^A x)) for q ≤ log^B x, with the genuine logarithmic integral and correctly quantified constants. The fixed-parameter theorem BombieriVinogradov.bombieri_vinogradov is not a genuine averaged BV estimate and does not provide this input.
2. Quantitative Moebius tail: |Σ_{d≤u} μ(d)/d| = O(1/log u), a PNT-level input not proved by the finite reductions.
3. Weighted main-term comparison: PanMainTermAbsorbedBound, including the signed main block and the weight/support requirements, remains an assumption.
4. Rounding lemma: establish the proposed 3/log(y/a) bound under explicit domain hypotheses for the proxy, and handle the excluded small arguments separately.

The original universal comparison is therefore not an analytic input that can simply be filled in. The corrected route must retain these signed, support, and error requirements.

theorem AnalyticNumberTheory.Sieve.panChebyshevMainStepLHS_abs_le_corrected (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) : (|∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (apLogVonMangoldt (y / a) q (natInvMod q a * l % q) - logarithmicIntegral (↑y / ↑a) / ↑q.totient) else 0| + ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then |f a| * apPrimePowerCorrection (y / a) q (natInvMod q a * l % q) else 0) ≤ |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * apV1Log (y / a) q (natInvMod q a * l % q) u else 0| + |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * apV3Log (y / a) q (natInvMod q a * l % q) u v else 0| + |∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * (apMiddleLog (y / a) q (natInvMod q a * l % q) u v - apSmallLog (y / a) q (natInvMod q a * l % q) v + logarithmicIntegral (↑y / ↑a) / ↑q.totient) else 0| + ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then |f a| * apPrimePowerCorrection (y / a) q (natInvMod q a * l % q) else 0

Exact decomposition of the main-step left side: for arbitrary f,u,v, `|Σ f·(Λlog−li_ℝ/φ)| + Σ |f|·PPC ≤ |Σ f·V1Log| + |Σ f·V3Log|

• |Σ f·(MiddleLog−SmallLog+li_ℝ/φ)| + Σ |f|·PPC. Substitute apLogVonMangoldt_eq_logPiecestermwise and apply the triangle inequality. This finite bound requires no condition onf 0, since the sums here start at 1. It retains the signed middle − small + li` block rather than the pure-li piece.

theorem AnalyticNumberTheory.Sieve.not_PanChebyshevMainStep : ¬PanChebyshevMainStep (fun (a : ℕ) => if a = 1 then 2 / Real.log 2 else if a = 2 then -(2 / Real.log 2) else 0) 4 0

Counterexample to universal PanChebyshevMainStep: let X=2, q=1, y=4, l=0, u=4, v=0, and f(1)=2/log 2, f(2)=−2/log 2, with f=0 otherwise. Since li(4)=li(2), the pure-li right-hand piece is zero. The remaining right side is c·log 3/(2 log 2), while the left side is |3c/2|+c/2 = 2c, with c=2/log 2. The strict inequality follows from log 16 > log 3. The necessary third block must retain middle/small and li inside one absolute value (panDistributionSum_abs_le_logPieces_mainBlock).

11. Source-faithful signed kernels

Liu's Theorem 2 (PDF p.2) only sums over (a,q)=1. The main term in eqn-m1 and the signed error in eqn-r are on PDF p.5; the omitted non-coprime contribution is the separate R₁ term in eqn-r0 on PDF p.6. Accordingly, the kernels below do not encode coprimality: that restriction is visible in the surrounding finite sums.

The aggregate kernels used by the existing type I/II estimates are apV1 y q l u / log y and apV3 y q l u v / log y. Vaughan's exact identity instead produces the termwise-log kernels apV1Log and apV3Log. The signed main kernel records this conversion exactly, together with the middle/small pieces and Liu's real-argument logarithmic integral.

noncomputable def AnalyticNumberTheory.Sieve.panSignedMainKernel (y a q l u v : ℕ) : ℝ

The exact signed residual after removing the aggregate type I and type II kernels. Coprimality is deliberately not part of this function.

Equations

• AnalyticNumberTheory.Sieve.panSignedMainKernel y a q l u v = AnalyticNumberTheory.Sieve.apV1Log (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u - AnalyticNumberTheory.Sieve.apV1 (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u / Real.log ↑(y / a) + (AnalyticNumberTheory.Sieve.apV3Log (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u v - AnalyticNumberTheory.Sieve.apV3 (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u v / Real.log ↑(y / a)) - AnalyticNumberTheory.Sieve.apMiddleLog (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) u v + AnalyticNumberTheory.Sieve.apSmallLog (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q) v - AnalyticNumberTheory.Sieve.logarithmicIntegral (↑y / ↑a) / ↑q.totient

noncomputable def AnalyticNumberTheory.Sieve.panSignedCorrectionKernel (y a q l : ℕ) : ℝ

The prime-power correction kernel in the exact ψ/log to π conversion. It is nonnegative and contains no coprimality convention.

Equations

• AnalyticNumberTheory.Sieve.panSignedCorrectionKernel y a q l = AnalyticNumberTheory.Sieve.apPrimePowerCorrection (y / a) q (AnalyticNumberTheory.Sieve.natInvMod q a * l % q)

noncomputable def AnalyticNumberTheory.Sieve.panSignedMainSum (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) : ℝ

Signed main residual, with Liu's (a,q)=1 restriction displayed at the sum rather than hidden in the kernel.

Equations

• AnalyticNumberTheory.Sieve.panSignedMainSum y X q l f u v = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * AnalyticNumberTheory.Sieve.panSignedMainKernel y a q l u v else 0

noncomputable def AnalyticNumberTheory.Sieve.panSignedCorrectionSum (y X q l : ℕ) (f : ℕ → ℝ) : ℝ

Signed prime-power correction in the exact decomposition.

Equations

• AnalyticNumberTheory.Sieve.panSignedCorrectionSum y X q l f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then f a * AnalyticNumberTheory.Sieve.panSignedCorrectionKernel y a q l else 0

noncomputable def AnalyticNumberTheory.Sieve.panSignedCorrectionBound (y X q l : ℕ) (f : ℕ → ℝ) : ℝ

Nonnegative majorant for the signed prime-power correction.

Equations

• AnalyticNumberTheory.Sieve.panSignedCorrectionBound y X q l f = ∑ a ∈ Finset.Icc 1 X, if a.Coprime q then |f a| * AnalyticNumberTheory.Sieve.panSignedCorrectionKernel y a q l else 0

theorem AnalyticNumberTheory.Sieve.panSignedCorrectionBound_nonneg (y X q l : ℕ) (f : ℕ → ℝ) : 0 ≤ panSignedCorrectionBound y X q l f

The separate prime-power correction majorant is nonnegative.

theorem AnalyticNumberTheory.Sieve.panDistributionSum_eq_sourceFaithfulSigned (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : panDistributionSum y X q l f = ((panPieceSum y X q l f fun (y q l : ℕ) => apV1 y q l u / Real.log ↑y) + panPieceSum y X q l f fun (y q l : ℕ) => apV3 y q l u v / Real.log ↑y) + panSignedMainSum y X q l f u v - panSignedCorrectionSum y X q l f

Exact finite signed decomposition. This is the strongest statement available from the existing Vaughan and Chebyshev identities: no analytic estimate or triangle inequality has yet been used.

theorem AnalyticNumberTheory.Sieve.abs_panSignedCorrectionSum_le (y X q l : ℕ) (f : ℕ → ℝ) : |panSignedCorrectionSum y X q l f| ≤ panSignedCorrectionBound y X q l f

The signed prime-power correction is bounded by its separate nonnegative majorant.

theorem AnalyticNumberTheory.Sieve.abs_panDistributionSum_le_sourceFaithfulSigned (y X q l : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : |panDistributionSum y X q l f| ≤ |panPieceSum y X q l f fun (y q l : ℕ) => apV1 y q l u / Real.log ↑y| + |panPieceSum y X q l f fun (y q l : ℕ) => apV3 y q l u v / Real.log ↑y| + (|panSignedMainSum y X q l f u v| + panSignedCorrectionBound y X q l f)

Pointwise triangle form of the exact signed decomposition.

noncomputable def AnalyticNumberTheory.Sieve.panSignedResidualMaxY (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : ℝ

The double maximum of the concrete signed main plus its separate prime-power correction.

Equations

• AnalyticNumberTheory.Sieve.panSignedResidualMaxY X q x f u v = AnalyticNumberTheory.Sieve.panScoreMaxY✝ q x fun (y l : ℕ) => |AnalyticNumberTheory.Sieve.panSignedMainSum y X q l f u v| + AnalyticNumberTheory.Sieve.panSignedCorrectionBound y X q l f

@[simp]

theorem AnalyticNumberTheory.Sieve.panSignedResidualMaxY_zero (X x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : panSignedResidualMaxY X 0 x f u v = 0

theorem AnalyticNumberTheory.Sieve.panSignedResidualMaxY_one (X x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : panSignedResidualMaxY X 1 x f u v = (Finset.image (fun (y : ℕ) => |panSignedMainSum y X 1 0 f u v| + panSignedCorrectionBound y X 1 0 f) (Finset.range (x + 1))).max' ⋯

theorem AnalyticNumberTheory.Sieve.panSignedResidualMaxY_nonneg (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) : 0 ≤ panSignedResidualMaxY X q x f u v

The concrete residual double maximum is nonnegative.

theorem AnalyticNumberTheory.Sieve.panMaxY_le_sourceFaithfulSigned (X q x : ℕ) (f : ℕ → ℝ) (u v : ℕ) (hf0 : f 0 = 0) : panMaxY X q x f ≤ ((panPieceMaxY X q x f fun (y q l : ℕ) => apV1 y q l u / Real.log ↑y) + panPieceMaxY X q x f fun (y q l : ℕ) => apV3 y q l u v / Real.log ↑y) + panSignedResidualMaxY X q x f u v

Finite max bridge from the exact pointwise identity to the concrete source-faithful signed kernels.

def AnalyticNumberTheory.Sieve.PanSourceFaithfulSignedMainBound (x f : ℕ → ℝ) (u v : ℕ) : Prop

The exact inverse-log paper input remaining after all finite identities, maxima, and conversion residuals have been made explicit. Its quantifiers match Liu, Theorem 2 (PDF p.2); the main/error separation is eqn-m1 and eqn-r (PDF p.5).

Equations

• AnalyticNumberTheory.Sieve.PanSourceFaithfulSignedMainBound x f u v = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panSignedResidualMaxY X q ⌊x X⌋₊ f u v ≤ C * x X / Real.log (x X) ^ A

theorem AnalyticNumberTheory.Sieve.PanMeanValueUniform.of_sourceFaithfulSignedInputs {x f : ℕ → ℝ} {u v : ℕ} (hI : PanTypeICharacterMeanValue x f u) (hII : PanTypeIICharacterMeanValue x f u v) (hM : PanSourceFaithfulSignedMainBound x f u v) (hfin : PanLogEventuallyLarge x) (hf0 : f 0 = 0) : PanMeanValueUniform x f

Conditional finite assembly using the concrete source-faithful residual. Unlike PanMeanValueUniform.of_signedAnalyticInputs, this theorem constructs the pointwise signed split from Vaughan's exact identity; its only signed-main hypothesis is the narrow inverse-log paper input above.