Positive Exact Realization Fiber

Abstract

A positive exact Cayley realization with nonzero exhaustive zero modes forces the Riemann hypothesis, and RH supplies the canonical realization.

Theorem 1.1 (A nonempty positive exact realization fiber forces RH).

$$\begin{array}{r}\forall Z:\mathrm{ZeroData},\\ \forall \rho \in \mathbb{C},\mathrm{riemannZeta}\left(\rho \right)=0\wedge \neg \exists n\in \mathbb{N},\rho =-2n+1\wedge \rho \ne 1\Rightarrow \exists n\in \mathbb{N},\mathrm{zero}\left(Z,n\right)=\rho \Rightarrow \mathrm{Nonempty}\left(\mathrm{PositiveExactRealization}\left(Z\right)\right)\Rightarrow \mathrm{RiemannHypothesis}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Midline/Cayley/PositiveExactRealizationFiber.positive_exact_realization_fiber_nonempty_implies_rh (✓ std3). ∎

Source. Repository-derived.

Commentary.

For ZeroData Z, a positive exact realization consists of a bounded operator C and a nonzero vector psi_v for every multiplicity coordinate v. Exactness is the eigenmode identity C psi_v = c_v psi_v, where c_v = (rho_v - 1) / rho_v; positivity is the Gram identity C* C = I.

The source proof silently needs every psi_v to be nonzero and its zero family to exhaust all nontrivial zeta zeros. The formal statement makes both requirements explicit. The exhaustiveness binder uses the same public bridge as ZeroHilbertCayleyUnitarity.

The Gram identity makes C an isometry. Applying norm preservation to a nonzero eigenmode forces |c_v| = 1, and the imported zero-Hilbert Cayley equivalence yields RH. No critical-line algebra is reproved.

The companion declaration canonicalPositiveExactRealization constructs C from the diagonal zeroCayleyOperator and psi_v from the canonical single-coordinate vector under RH. Thus the file also proves that the realization fiber is nonempty exactly when RH holds.

References

• Truth anchor: D5/S3/Midline/Cayley/PositiveExactRealizationFiber.positive_exact_realization_fiber_nonempty_implies_rh
• Dependency: D5/S3/Midline/Cayley/ZeroHilbertCayleyUnitarity