Interior Curvature Criterion

Abstract

The source Riesz-curvature measure has no interior atom exactly when every canonical nontrivial zeta zero lies on the critical line.

Theorem 1.1 (Interior curvature vanishes exactly under the zeta criterion).

$$\begin{array}{r}Zplus:=\left\{\mathrm{IsNontrivialZero}\left(s\right)\wedge \frac{1}{2}<\mathrm{re}\left(s\right)\mid s\in \mathrm{Complex}\left(\right)\right\}\\ z:=(rho:\mathrm{Subtype}\left(Zplus\right)\mapsto -\mathrm{im}\left(\mathrm{val}\left(rho\right)\right)+i\cdot (\mathrm{re}\left(\mathrm{val}\left(rho\right)\right)-\frac{1}{2}))\\ curvatureInt:=\mathrm{measureSum}\left((rho:\mathrm{Subtype}\left(Zplus\right)\mapsto \mathrm{ofReal}\left(2\cdot pi\right)\cdot \mathrm{toENNReal}\left(\mathrm{zeroMult}\left(\mathrm{val}\left(rho\right)\right)\right)\cdot \mathrm{dirac}\left(z\left(rho\right)\right))\right)\\ \left(\forall s\in \mathrm{Complex}\left(\right),\mathrm{IsNontrivialZero}\left(s\right)\Rightarrow \mathrm{re}\left(s\right)=\frac{1}{2}\right)\iff curvatureInt=0.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Boundary/InteriorCurvatureCriterion.interior_curvature_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The right off-line carrier is cut directly from the canonical IsNontrivialZero predicate. Each zero is sent to the source upper-half-plane point with real coordinate minus its ordinate and imaginary coordinate its displacement from one half.

The interior curvature is the Measure.sum of Dirac masses with the source coefficient two pi times the analytic multiplicity. Its vanishing is proved from positivity of every indexed atom, not installed as a definition.

Reflection of a hypothetical left off-line zero produces a right off-line zero, completing the converse implication.

References

• Truth anchor: D5/S3/Analytic/Boundary/InteriorCurvatureCriterion.interior_curvature_criterion