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\). Fully proved, no sorry and no axiom (the growth direction is ExpNotTempered.exp_growth_not_tempered). This is a fact about a single exponential; it says nothing by itself about the zeros of \(\zeta \).

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). That hypothesis is open and is not established anywhere in this tree, so this theorem does not prove RH.