Auxiliary estimates for the all-character Type II audit

This module proves elementary identities and bounds used to examine the all-character predicate panTypeIICharSquareMeanBound at u = v = 1: the identity vaughanThird(n,1,1) = Lambda(n) - log n, interval and coprime counts, domination by the principal character, an L2 upper bound, and a lower bound for the principal-character mass.

Section 6 records a proposed counterexample assembly at m = Q^2, with its remaining counting and growth arguments stated in prose. The declarations in this module establish the individual auxiliary bounds listed above.

For the primitive-character large sieve, see Montgomery (1971), Chapter 1, Theorem 5.1, and Davenport, Chapter 27. Mathlib's Dirichlet-character library supplies conductor, primitivity and Gauss-sum infrastructure.

1. Algebraic identity: vaughanThird(n,1,1) = Lambda(n) - log n

theorem AnalyticNumberTheory.Sieve.vonMangoldt_zero : ArithmeticFunction.vonMangoldt 0 = 0

Lambda 0 = 0.

theorem AnalyticNumberTheory.Sieve.vaughanThird_one_one (n : ℕ) : vaughanThird n 1 1 = ArithmeticFunction.vonMangoldt n - Real.log ↑n

vaughanThird at (u,v) = (1,1): vaughanThird(n,1,1) = Lambda(n) - log n. From mu * log = Lambda (mathlib moebius_mul_log_eq_vonMangoldt) and Sum_{e|m} Lambda(e) = log m (vonMangoldt_sum).

2. Counterexample decomposition: the principal (trivial) character term

theorem AnalyticNumberTheory.Sieve.panTypeIICharSqSum_ge_trivial (q m : ℕ) : (∑ n ∈ Finset.range (m + 1) with n.Coprime q, vaughanThird n 1 1) ^ 2 ≤ panTypeIICharSqSum q m 1 1

The trivial-character square is <= the full character-square sum (one nonneg term).

3. Elementary analytic ingredients for the counterexample

theorem AnalyticNumberTheory.Sieve.card_multiples_Ioc (m d : ℕ) (hd : 1 ≤ d) : {n ∈ Finset.Ioc (m / 2) m | d ∣ n}.card = m / d - m / 2 / d

Count of multiples of d in the window (m/2, m]: #{n ∈ (m/2,m] : d | n} = m/d - (m/2)/d.

theorem AnalyticNumberTheory.Sieve.card_multiples_Ioc_ge (m d : ℕ) (hd : 1 ≤ d) : ↑m / (2 * ↑d) - 2 ≤ ↑{n ∈ Finset.Ioc (m / 2) m | d ∣ n}.card

Real lower bound: #{d|n in window} ≥ (m/2)/d - 2.

theorem AnalyticNumberTheory.Sieve.card_multiples_Ioc_le (m d : ℕ) (hd : 1 ≤ d) : ↑{n ∈ Finset.Ioc (m / 2) m | d ∣ n}.card ≤ ↑m / (2 * ↑d) + 3

Real upper bound: #{d|n in window} ≤ (m/2)/d + 2.

theorem AnalyticNumberTheory.Sieve.coprime_count_Ioc (m p₁ p₂ : ℕ) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hne : p₁ ≠ p₂) : ↑m / 8 - 8 ≤ ↑{n ∈ Finset.Ioc (m / 2) m | n.Coprime (p₁ * p₂)}.card

Count of n coprime to p1*p2 in the window (m/2, m]: >= m/8 - 8.

4. The counterexample: LHS grows like Q^5, RHS like Q^4 log^2 Q

theorem AnalyticNumberTheory.Sieve.v3_one_one_sq_sum_le (m : ℕ) : ∑ n ∈ Finset.range (m + 1), vaughanThird n 1 1 ^ 2 ≤ 4 * (↑m + 1) * Real.log (↑m + 2) ^ 2

RHS quadratic sum bound: Sum_{n<=m} vaughanThird(n,1,1)^2 <= 4 (m+1) log^2 (m+2).

theorem AnalyticNumberTheory.Sieve.vCharAbs_lower (m p₁ p₂ : ℕ) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hne : p₁ ≠ p₂) (hm : 32 * (Real.log 4 + 4) ≤ Real.log (↑m / 2)) (hm128 : 128 ≤ m) : ↑m / 32 * Real.log (↑m / 2) ≤ |∑ n ∈ Finset.range (m + 1) with n.Coprime (p₁ * p₂), vaughanThird n 1 1|

The trivial-character mass: for q = p1*p2 with distinct prime factors, |Sum_{(n,q)=1, n<=m} vaughanThird(n,1,1)| >= (m/32)*log(m/2) when log(m/2) >= 32(log4+4) and m >= 128.

6. Final assembly (documented route; remaining steps are mechanical counting)

The following chain completes the disproof of panTypeIICharSquareMeanBound 1 1. All the analytic content is already proven above (vCharAbs_lower, v3_one_one_sq_sum_le, panTypeIICharSqSum_ge_trivial, coprime_count_Ioc). The remaining steps are elementary counting + the unboundedness of Q/log^2 Q:

1. Semiprime count (Chebyshev): for Q large, #{q ≤ Q : ∃ p₁ p₂, p₁.Prime ∧ p₂.Prime ∧ p₁ < p₂ ∧ p₁*p₂ = q} ≥ c₃ · Q/log²Q. Route: inject the pairs {p₁ < p₂} of primes ≤ √Q via (p₁,p₂) ↦ p₁*p₂ (UFD injection, Finset.powersetCard 2 count = C(π(√Q),2)), and use mathlib Chebyshev.pi_ge (π(n) ≥ (n·log2 − log(n+1))/log n ≥ (log2/2)·n/log n for n ≥ 16).

2. LHS lower bound: for m = Q², each semiprime q = p₁p₂ ≤ Q contributes μ²(q)·3^{ω(q)}·panTypeIICharSqSum q m 1 1 ≥ 9·|Σ_{(n,q)=1,n≤m} vaughanThird(n,1,1)|² (panTypeIICharSqSum_ge_trivial, μ²(q)=1, ω(q)=2), and |Σ_{(n,q)=1,n≤m} vaughanThird(n,1,1)| ≥ (m/32)·log(m/2) (vCharAbs_lower, with log(Q²/2) ≥ 32(log4+4) for large Q). Hence LHS(Q, Q²) ≥ 9·|S|·(Q²·log(Q²/2)/32)² ≥ c₁·Q⁵.

3. RHS upper bound: C·(m+Q²)·Σ_{n≤m} vaughanThird(n,1,1)² ≤ C·2Q²·4(Q²+1)·log²(Q²+2) ≤ c₂·C·Q⁴·log²Q (v3_one_one_sq_sum_le).

4. Contradiction: the assumption gives c₁Q⁵ ≤ c₂·C·Q⁴·log²(Q+1), i.e. Q ≤ (c₂C/c₁)·log²(Q+1) for all large Q. Take Q = 2^k, k → ∞: 2^k ≥ k³ for k ≥ 10 (elementary) makes 2^k/(k+1)²·log²2 unbounded, contradicting the inequality for k large (Archimedean choice of k).

This yields panTypeIICharSquareMeanBound_one_one_false : ¬ panTypeIICharSquareMeanBound 1 1 (the four steps above are the complete formalization remaining; each is a routine finite verification on top of the lemmas already proven in this file).