generalized_riemann_hypothesis

⚠️ Retired — this formal statement is not a formalization of the Generalized Riemann Hypothesis.

Its Disproved status is a property of this particular encoding and says nothing about GRH, which remains open. Do not import it or use it as a dependency.

Generalized Riemann Hypothesis (GRH): for every Dirichlet character $\chi$ modulo $q$, all non-trivial zeros of the Dirichlet $L$-function $L(\chi, s)$ lie on the critical line $\operatorname{Re}(s) = \tfrac{1}{2}$.

The Riemann Hypothesis is the special case of the principal character mod $1$. GRH plays the same role for primes in arithmetic progressions that RH plays for all primes; it yields optimal error terms in the prime number theorem for arithmetic progressions and conditionally resolves Artin's conjecture.

Source: Bombieri, E. (2000). Problems of the Millennium: The Riemann Hypothesis. Clay Mathematics Institute. Also: Davenport, H. (2000). Multiplicative Number Theory, 3rd ed., Springer.

Why this node was retired

The zero hypothesis in the posted statement is

hs_zero : LSeries (fun n => (χ n : ℂ)) s = 0

LSeries f s is the Dirichlet series $\sum_{n \ge 1} f(n) n^{-s}$, defined in Mathlib as a tsum. Mathlib's tsum is unconditional summability, which for a $\mathbb{C}$-valued series indexed by $\mathbb{N}$ coincides with absolute convergence, and it returns $0$ by convention when the family is not summable. For a Dirichlet character the family $\bigl(\chi(n) n^{-s}\bigr)_n$ is absolutely summable exactly when $\operatorname{Re}(s) > 1$.

Therefore, throughout the critical strip $0 < \operatorname{Re}(s) < 1$, the hypothesis LSeries χ s = 0 is satisfied vacuously, at every point, because the series does not converge there. It does not say "$s$ is a zero of $L(\chi, s)$"; it says nothing at all. The statement as posted thus asserts that every point of the open strip lies on the critical line, which is false for trivial reasons.

The accepted counterexample makes this concrete with the principal character mod $2$ at $s = 1/4$: LSeriesSummable fails there, so LSeries χ (1/4) = 0 holds by the tsum convention, while $\operatorname{Re}(s) = 1/4 \ne 1/2$. The refutation is correct, and what it refutes is the encoding convention.

What a faithful statement would require

The zero must be a zero of the analytic continuation of the $L$-function — in Mathlib, DirichletCharacter.LFunction — and not of the series LSeries, which simply does not represent $L(\chi, s)$ anywhere inside the strip. A faithful statement must also separate the non-trivial zeros from the trivial ones coming from the functional equation's gamma factors, and fix the intended hypotheses on $\chi$ (in particular primitivity, if the Euler factors at the ramified primes are to be excluded).

No corrected replacement node exists yet. GRH remains open.