If \(\zeta (\rho ) = 0\) with \(\mathrm{Re}(\rho ) \neq \tfrac {1}{2}\), there exist at least two distinct zeros with \(\mathrm{Im}(s) = \mathrm{Im}(\rho )\). (Zero sorries, zero axioms.)

\(e^{au}\) defines a tempered distribution on \(\mathbb {R}\) iff \(a=0\). Two sorries: requires SchwartzMap.tsum not yet in Mathlib.

If the Weil/Yakaboylu paired form is positive semidefinite on every finite subset of the nontrivial zero set, then every non-trivial zero of \(\zeta (s)\) satisfies \(\mathrm{Re}(s) = \tfrac {1}{2}\).

Status: the former arithmetic_admissibility axiom (which asserted RH verbatim) is retired. The conditional above is proved with no axioms beyond Mathlib’s built-ins; the open analytic content is the positivity hypothesis (explicit formula / operator compression).