Relative Curvature Support Criterion

Abstract

The multiplicity-weighted curvature measure of the canonical nontrivial zeta zeros is supported on the critical line exactly when every such zero is critical.

Theorem 1.1 (Relative curvature is critical exactly under the zeta criterion).

$$\begin{array}{r}Z:=\left\{\mathrm{IsNontrivialZero}\left(s\right)\mid s\in \mathrm{Complex}\left(\right)\right\}\\ curvature:=\mathrm{measureSum}\left((rho:\mathrm{Subtype}\left(Z\right)\mapsto \mathrm{toENNReal}\left(\mathrm{zeroMult}\left(\mathrm{val}\left(rho\right)\right)\right)\cdot \mathrm{dirac}\left(\mathrm{val}\left(rho\right)\right))\right)\\ S:=\left\{0<\mathrm{re}\left(s\right)\wedge \mathrm{re}\left(s\right)<1\mid s\in \mathrm{Complex}\left(\right)\right\}\\ L:=\left\{\mathrm{re}\left(s\right)=\frac{1}{2}\mid s\in \mathrm{Complex}\left(\right)\right\}\\ \left(\forall s\in \mathrm{Complex}\left(\right),\mathrm{IsNontrivialZero}\left(s\right)\Rightarrow \mathrm{mem}\left(s,L\right)\right)\iff \mathrm{inter}\left(\mathrm{support}\left(curvature\right),S\right)\subseteq L.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Adelic/RelativeCurvatureSupportCriterion.relative_curvature_support_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The zero carrier is the repository’s canonical IsNontrivialZero set. Relative curvature is constructed as the Measure.sum of Dirac masses weighted by the canonical analytic multiplicity zeroMult; its support is not installed by definition.

The local proof identifies this carrier with the closed zero locus of the entire xiReading and proves from the measure API that every positive weighted atom, and only such an atom, lies in the support.

Since IsNontrivialZero already records the open critical-strip bounds, the resulting support inclusion is equivalent to the universal critical-line assertion.

References

• Truth anchor: D5/S3/Analytic/Adelic/RelativeCurvatureSupportCriterion.relative_curvature_support_criterion
• Dependency: D5/S3/Zeros/CompletedZeta