Zero-Hilbert Cayley Unitarity

Abstract

The Cayley multiplier on the multiplicity-expanded zero Hilbert space has the exact star-unitarity defect, and its vanishing is equivalent to the Riemann hypothesis.

Theorem 1.1 (The Cayley defect and all of its unitarity characterizations).

$$\begin{array}{c}\forall Z:\mathrm{ZeroData},\\ \forall h:(\forall \rho \in \mathbb{C},(((\mathrm{riemannZeta}\left(\rho \right)=0)\wedge (\neg \exists n\in \mathbb{N},\rho =-2(n+1)))\wedge (\rho \ne 1))\Rightarrow (\exists n\in \mathbb{N},\mathrm{zero}\left(Z,n\right)=\rho )),\\ (\forall v\in \mathrm{ZeroCoordinate}\left(Z\right),\mathrm{let}{\delta }_v={\Vert \mathrm{cayleyCoefficient}\left(\mathrm{zero}\left(Z,\mathrm{fst}\left(v\right)\right)\right)\Vert }^2-1;\\ ((((\mathrm{zeroCayleyOperator}\left(Z\right)(\mathrm{single}\left(2,v,1\right))=\mathrm{cayleyCoefficient}\left(\mathrm{zero}\left(Z,\mathrm{fst}\left(v\right)\right)\right)\cdot \mathrm{single}\left(2,v,1\right))\wedge ((\mathrm{zeroCayleyOperator}{\left(Z\right)}^{\ast }\mathrm{zeroCayleyOperator}\left(Z\right)-I)(\mathrm{single}\left(2,v,1\right))={\delta }_v\cdot \mathrm{single}\left(2,v,1\right)))\wedge ({\delta }_v=\frac{1-2\Re (\mathrm{zero}\left(Z,\mathrm{fst}\left(v\right)\right))}{{\Vert \mathrm{zero}\left(Z,\mathrm{fst}\left(v\right)\right)\Vert }^2}))\wedge ((\Vert \mathrm{cayleyCoefficient}\left(\mathrm{zero}\left(Z,\mathrm{fst}\left(v\right)\right)\right)\Vert =1)⟺(\Re (\mathrm{zero}\left(Z,\mathrm{fst}\left(v\right)\right))=\frac{1}{2})))\wedge ((\Re (\mathrm{zero}\left(Z,\mathrm{fst}\left(v\right)\right))=\frac{1}{2})⟺(\Vert \mathrm{zeroCayleyOperator}\left(Z\right)(\mathrm{single}\left(2,v,1\right))\Vert =\Vert \mathrm{single}\left(2,v,1\right)\Vert )))\wedge \\ ((\mathrm{RiemannHypothesis})⟺(\forall v\in \mathrm{ZeroCoordinate}\left(Z\right),\Vert \mathrm{cayleyCoefficient}\left(\mathrm{zero}\left(Z,\mathrm{fst}\left(v\right)\right)\right)\Vert =1))\wedge \\ ((\mathrm{RiemannHypothesis})⟺(\mathrm{zeroCayleyOperator}{\left(Z\right)}^{\ast }\mathrm{zeroCayleyOperator}\left(Z\right)=I))\wedge \\ ((\mathrm{RiemannHypothesis})⟺(\mathrm{Unitary}\left(\mathrm{zeroCayleyOperator}\left(Z\right)\right)))\wedge \\ ((\forall v\in \mathrm{ZeroCoordinate}\left(Z\right),\Vert \mathrm{zeroCayleyOperator}\left(Z\right)(\mathrm{single}\left(2,v,1\right))\Vert =\Vert \mathrm{single}\left(2,v,1\right)\Vert )⟺(\mathrm{Unitary}\left(\mathrm{zeroCayleyOperator}\left(Z\right)\right))).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let I_Z be the dependent sum of Fin(multiplicity(n)) over the distinct zeros stored by Z, and let H_Z be ell squared on I_Z. The vector e_v is the canonical single-coordinate vector. The coefficient c_v is (Z.zero(v.1) - 1) / Z.zero(v.1), and C_Z is the repository’s bounded diagonal operator built from the full coefficient family.

The exhaustiveness binder states that Z covers every zeta zero in the domain quantified by Mathlib’s RiemannHypothesis. This is the public bridge from the source’s multiset of all nontrivial zeros to ZeroData, whose native exhaustive field covers zeros in the open strip.

For every multiplicity coordinate, the statement gives the diagonal action, the basis-vector star defect, both scalar formulas for the defect, and the two pointwise norm characterizations. It then identifies the Riemann hypothesis with coefficient norm one, the Gram identity, and standard unitary membership, and directly relates the latter to norm preservation on every canonical basis vector.

Boundedness follows from continuity and nonvanishing of zeta near zero, which gives a uniform lower bound for the norms of all supplied zeros. The result is conditional on supplied ZeroData and its explicit exhaustiveness bridge; it does not construct either object or prove the Riemann hypothesis.

References

• Truth anchor: D5/S3/Midline/Cayley/ZeroHilbertCayleyUnitarity.cayley_unitarity_defect_formula_on_zero_hilbert_space
• Dependency: D5/S3/Midline/Cayley/CayleyUnitarityDefect
• Dependency: D5/S3/Observer/Approximation/ReadoutUpdateCommutatorFactorization
• Dependency: D5/S3/Weil/ZetaBridge/RhLocatesZeroData