chebyshev_sign_change.toml

id = "chebyshev_sign_change"
title = "Hardy–Littlewood sign-change for the prime race mod 4"
test = false
module = "LeanEval.NumberTheory.ChebyshevSignChange"
holes = ["chebyshev_sign_change"]
submitter = "Kim Morrison"
notes = "The difference π₃(n) − π₁(n), where πᵢ(n) counts primes ≤ n congruent to i mod 4, takes both positive and negative values infinitely often. Chebyshev (1853) observed the empirical bias toward π₃(n) > π₁(n); Hardy and Littlewood (1914) proved unconditionally that π₁ nevertheless overtakes π₃ infinitely often, and the reverse direction is the typical Chebyshev-bias inequality. §106 of Knill's *Some Fundamental Theorems in Mathematics* lists this under the metamathematical 'strong law of small numbers'; the formalised theorem here is the Hardy–Littlewood sign-change theorem."
source = "G.H. Hardy and J.E. Littlewood, 'Contributions to the theory of the Riemann zeta-function and the theory of the distribution of primes', Acta Math. 41 (1916) 119–196 (announced 1914). Chebyshev's original observation: P. Chebyshev, letter to M. Fuss, 1853, in *Œuvres de P.L. Tchebychef*, vol. I (Saint Petersburg, 1899). Listed as §106 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
informal_solution = "This is an analytic-number-theory theorem of Hardy and Littlewood. The modern argument studies the difference π₃(x) − π₁(x) via the non-trivial real Dirichlet character χ modulo 4 and explicit-formula methods for the Dirichlet L-function L(s, χ): the functional equation, the non-vanishing of L(s, χ) for Re(s) ≥ 1, and an oscillation contribution from the non-trivial zeros together force the difference to take both signs infinitely often. The result is unconditional, but the analytic machinery — Riemann's explicit formula and quantitative prime-counting in arithmetic progressions — is well beyond mathlib v4.30.0. Mathlib has the elementary infrastructure used in the *statement* (`Nat.Prime`, `ZMod`, `Nat.primeCounting`, `Filter.limsup`/`liminf`, and Dirichlet's existence theorem for primes in arithmetic progressions via `Mathlib/NumberTheory/LSeries/PrimesInAP.lean`), but no Hardy–Littlewood sign-change framework; the `PrimeNumberTheoremAnd` external project still has PNT itself sorried."