Compactified Squared-Distance Support

Abstract

A rational compactification separates nonnegative and negative squared distances and characterizes critical-line support.

Theorem 1.1 (Compactified squared-distance support criterion).

$$\forall a\in \mathrm{Real}\left(\right),x\in \mathrm{Real}\left(\right),delta\in \mathrm{Real}\left(\right),\left(\frac{1}{4}<a\wedge \left(0\le x\wedge \left(0<\mathrm{abs}\left(delta\right)\wedge delt{a}^2<\frac{1}{4}\right)\right)\right)\Rightarrow \mathrm{let}compactCoordinate=(y\mapsto \frac{y-a}{y+a}),\left(-1\le compactCoordinate\left(x\right)\wedge compactCoordinate\left(x\right)<1\right)\wedge \left(\left(compactCoordinate\left(-delt{a}^2\right)=-\frac{a+delt{a}^2}{a-delt{a}^2}\wedge compactCoordinate\left(-delt{a}^2\right)<-1\right)\wedge \left(\mathrm{RiemannHypothesis}\left(\right)\iff \left(\forall rho\in \mathrm{Complex}\left(\right),\left(\mathrm{riemannZeta}\left(rho\right)=0\wedge \left(\left(\neg \left(\exists n\in \mathrm{Nat}\left(\right),rho=-2\cdot \left(n+1\right)\right)\right)\wedge rho\ne 1\right)\right)\Rightarrow \mathrm{let}signedSquaredDistance=-{\left(\mathrm{re}\left(rho\right)-\frac{1}{2}\right)}^2,signedSquaredDistance+a\ne 0\wedge compactCoordinate\left(signedSquaredDistance\right)\in \mathrm{Icc}\left(-1,1\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/CayleyLaguerre/CompactifiedSquaredDistanceSupport.compactified_squared_distance_support_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The compact coordinate is the source rational map, constructed from the supplied scale. Nonnegative inputs land in the unit interval, while a genuine signed squared distance in the critical strip lands strictly below negative one.

For every Mathlib-nontrivial zeta zero, the observed signed squared distance is constructed from its real coordinate. Requiring the rational coordinate to be defined and supported in the closed unit interval is equivalent to the stated critical-line hypothesis.

References

• Truth anchor: D5/S3/Weil/CayleyLaguerre/CompactifiedSquaredDistanceSupport.compactified_squared_distance_support_criterion
• Dependency: D5/S3/Weil/CayleyLaguerre/ChebyshevSignedDistanceSeparator