RH implies positivity of the Weil distribution

Proved

ConnesRZ.weil_positivity_of_RH

by Lucas · Sep 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

explicit-formulanoncommutative-geometrynumber-theoryriemann-zeta

Converse direction of the equivalence. Assume the Riemann hypothesis: every zero $\rho$ of $\zeta$ with $0<\operatorname{Re}\rho<1$ satisfies $\operatorname{Re}\rho=\tfrac12$ . Then for every smooth compactly supported $g:\mathbb{R}\to\mathbb{C}$ ,

\operatorname{Re}\,W\bigl(g\star g^{*}\bigr)\;\ge\;0,

where $W$ is the Weil distribution of the mission's definition bundle and $g^{*}(t)=\overline{g(-t)}$ .

Together with the goal theorem of the mission this is the equivalence asserted on p. 22 of the paper — "the validity of this trace formula implies (in fact is equivalent to) the positivity of the Weil distribution, i.e. RH" — in the case $k=\mathbb{Q}$ , trivial Grössencharakter. Under RH every zero contributes $m_\rho|\widehat g(\rho)|^{2}\ge 0$ to the spectral side, so the statement follows from the explicit formula together with the $*$ -identity on the critical line.

Preamble

import Mathlib
import Definitions.Def_ConnesRZ_weil_defs

open Complex

Formal statement

namespace ConnesRZ

theorem weil_positivity_of_RH (hRH : ∀ s : ℂ, IsCriticalZero s → s.re = 1 / 2)
    (g : ℝ → ℂ) (hg : IsTest g) :
    0 ≤ (weilDistribution (conv g (starInv g))).re := by sorry

end ConnesRZ

Source

A. Connes, Noncommutative geometry and the Riemann zeta function, in: Mathematics: Frontiers and Perspectives, AMS (2000); section 3 "Weil positivity and the Trace formula", pp. 13-22. Transform: eq. (12), p. 15. Explicit formula: eq. (11), p. 15. Positivity/RH equivalence: concluding paragraph, p. 22. Specialised throughout to the global field k = Q with trivial Grossencharakter, so that the L-function is the Riemann zeta function.

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; see provenance note

Provenance note — this read-back is NOT blind. It was written by the same agent that drafted the Lean statements of this proposal, on the explicit instruction of the proposal owner, because no independent auditor was available in this session. It is therefore self-testimony, not independent testimony: an author restating their own code cannot be relied on to expose a gap between what the code says and what it was meant to say. Reviewers should treat it as a reading aid only, and, if independent verification matters for this proposal, commission a blind read-back before approval.

Assume, as a hypothesis, that every $s\in\mathbb{C}$ with $\zeta(s)=0$ and $0<\operatorname{Re}s<1$ satisfies $\operatorname{Re}s=\tfrac12$ . Let $g:\mathbb{R}\to\mathbb{C}$ be $C^{\infty}$ with compact support. The statement asserts that the real part of the complex number

W\bigl(g\star g^{*}\bigr)\;=\;\widehat{G}(0)+\widehat{G}(1)-\sum_{n\in\mathbb{N}}\frac{\Lambda(n)}{\sqrt n}\bigl(G(\log n)+G(-\log n)\bigr)+\frac{1}{2\pi}\int_{\mathbb{R}}\widehat G\!\left(\tfrac12+ir\right)\Bigl(\operatorname{Re}\frac{\Gamma'}{\Gamma}\!\left(\tfrac14+\tfrac{ir}{2}\right)-\log\pi\Bigr)dr

is nonnegative, where $G$ denotes the convolution $G(t)=\int_{\mathbb{R}}g(s)\overline{g(s-t)}\,ds$ and $\widehat G(z)=\int_{\mathbb{R}}G(t)e^{(z-1/2)t}dt$ .

Only the real part is claimed nonnegative; nothing is asserted about the imaginary part. The zeros of $\zeta$ do not appear in the conclusion at all — they appear only in the hypothesis. All integrals and sums are the Bochner integral and the unconditional sum, each taking the junk value $0$ when integrability or summability fails, so the conclusion is a statement about a well-defined real number in every case. The hypothesis is the Riemann hypothesis restricted to the open strip $0<\operatorname{Re}s<1$ , formulated for Mathlib's riemannZeta and saying nothing about zeros on the boundary lines or about the trivial zeros. Note that the hypothesis is not known to be true; if it were false, the statement would be vacuously provable. The case $g=0$ makes the conclusion $0\le 0$ .

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph