Global Logarithmic Gauge Criterion

Abstract

A global analytic logarithm of the shifted completed-zeta reading exists exactly when every nontrivial zero lies on the critical line.

Theorem 1.1 (Global analytic logarithms characterize the critical line).

$$\begin{array}{r}rightHalfPlane:\mathrm{Set}\left(\mathbb{C}\right)=\left\{0<\mathrm{re}\left(z\right)\mid z\in \mathbb{C}\right\}\\ shiftedXi:\mathbb{C}\to \mathbb{C}=(z\mapsto \mathrm{xiReading}\left(\frac{1}{2}+z\right))\\ criticalLineHypothesis:Prop=\forall s\in \mathbb{C},\mathrm{IsNontrivialZero}\left(s\right)\Rightarrow \mathrm{re}\left(s\right)=\frac{1}{2}\\ (\left(criticalLineHypothesis\iff \left(\exists L\in \mathbb{C}\to \mathbb{C},\mathrm{AnalyticOnNhd}\left(\mathbb{C},L,rightHalfPlane\right)\wedge \mathrm{EqOn}\left((z\mapsto \exp \left(L\left(z\right)\right)),shiftedXi,rightHalfPlane\right)\right)\right)\wedge \left(\left(criticalLineHypothesis\Rightarrow \left(\exists L\in \mathbb{C}\to \mathbb{C},\mathrm{AnalyticOnNhd}\left(\mathbb{C},L,rightHalfPlane\right)\wedge \left(\mathrm{EqOn}\left((z\mapsto \exp \left(L\left(z\right)\right)),shiftedXi,rightHalfPlane\right)\wedge \mathrm{ContinuousOn}\left((z\mapsto \mathrm{comp}\left(imCLM,\mathrm{restrictScalars}\left(\mathbb{R},\mathrm{fderiv}\left(\mathbb{C},L,z\right)\right)\right)),rightHalfPlane\right)\right)\right)\right)\wedge \left(\forall z0\in \mathbb{C},\left(z0\in rightHalfPlane\wedge shiftedXi\left(z0\right)=0\right)\Rightarrow \left(\left(\neg \left(\exists L\in \mathbb{C}\to \mathbb{C},\mathrm{AnalyticOnNhd}\left(\mathbb{C},L,rightHalfPlane\right)\wedge \mathrm{EqOn}\left((z\mapsto \exp \left(L\left(z\right)\right)),shiftedXi,rightHalfPlane\right)\right)\right)\wedge \left(\forall domain\in \mathrm{Set}\left(\mathbb{C}\right),L\in \mathbb{C}\to \mathbb{C},\mathrm{EqOn}\left((z\mapsto \exp \left(L\left(z\right)\right)),shiftedXi,domain\right)\Rightarrow \left(\neg z0\in domain\right)\right)\right)\right)\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

The displayed rightHalfPlane, shiftedXi, and criticalLineHypothesis are the three literal let-definitions in the Lean theorem. The shift uses the repository’s canonical completed-zeta reading.

The forward direction constructs the logarithm from a primitive of the logarithmic derivative on the open convex half-plane. The reverse direction uses nonvanishing of the complex exponential together with the canonical completed-zeta zero criterion and reflection.

The second conjunct exposes the imaginary real differential of the chosen analytic logarithm and proves it continuous on the whole right half-plane. The final conjunct states both obstructions: a zero rules out the global logarithm and cannot belong to any domain carrying an exponential lift of shiftedXi.

References

• Truth anchor: D5/S3/Analytic/Adelic/GlobalLogarithmicGaugeCriterion.global_logarithmic_gauge_criterion
• Dependency: D5/S3/Zeros/CompletedZeta
• Dependency: D5/S3/Zeros/Endpoints/XiEndpointValues