Positive Torus Carrier Criterion

Abstract

A nonnegative weighted torus period whose nontrivial zeros are critical and whose auxiliary factor is regular forces all nontrivial zeta zeros onto the midline.

Theorem 1.1 (A regular positive torus carrier implies the critical-line criterion).

$$\begin{array}{r}\forall Index,Torus\in \mathrm{Type}\left(\right),\mathrm{MeasurableSpace}\left(Torus\right)\\ a:Index\to \mathrm{NNReal}\left(\right),muD:Index\to \mathrm{Measure}\left(Torus\right)\\ EStar:Torus\to \left(\mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right)\right),e,twistedCompleted:Index\to \left(\mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right)\right)\\ mu:=\mathrm{measureSum}\left((i\mapsto \mathrm{toENNReal}\left(a\left(i\right)\right)\cdot muD\left(i\right))\right)\\ Fmu:=(s\mapsto \mathrm{integral}\left((z\mapsto EStar\left(z\right)\left(s\right)),mu\right))\\ Gmu:=(s\mapsto \mathrm{tsum}\left((i\mapsto \mathrm{toComplex}\left(a\left(i\right)\right)\times e\left(i\right)\left(s\right)\times twistedCompleted\left(i\right)\left(s\right))\right))\\ Hplus:=\left\{\frac{1}{2}<\mathrm{re}\left(s\right)\mid s\in \mathrm{Complex}\left(\right)\right\}\\ ((\forall s\in \mathrm{Complex}\left(\right),\left(\mathrm{AnalyticAt}\left(\mathrm{Complex}\left(\right),Gmu,s\right)\wedge Gmu\left(s\right)\ne 0\right)\Rightarrow Fmu\left(s\right)=\mathrm{completedRiemannZeta}\left(s\right)\times Gmu\left(s\right))\wedge (\forall s\in \mathrm{Complex}\left(\right),\left(Fmu\left(s\right)=0\wedge \left(0<\mathrm{re}\left(s\right)\wedge \mathrm{re}\left(s\right)<1\right)\right)\Rightarrow \mathrm{re}\left(s\right)=\frac{1}{2})\wedge \mathrm{AnalyticOnNhd}\left(\mathrm{Complex}\left(\right),Gmu,Hplus\right)\wedge (\forall s\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(s,Hplus\right)\Rightarrow Gmu\left(s\right)\ne 0))\Rightarrow \forall rho\in \mathrm{Complex}\left(\right),\mathrm{IsNontrivialZero}\left(rho\right)\Rightarrow \mathrm{re}\left(rho\right)=\frac{1}{2}.\end{array}$$

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

Source. Repository-derived.

Commentary.

The measure mu is the literal Measure.sum of the supplied period measures scaled by NNReal weights. The period Fmu is the Bochner integral of the supplied Eisenstein family against mu. The auxiliary factor Gmu is the literal weighted tsum of the local and twisted-completion factors.

The Hecke factorization is required whenever Gmu is analytic and nonzero at the evaluation point. The two source regularity clauses provide exactly those facts on the open right half-plane, so every right-half completed-zeta zero becomes a zero of Fmu and hence lies on the midline by the period-zero premise.

The frozen completed-zeta zero theorem supplies the canonical nontrivial zeta carrier. Frozen conjugate reflection transports any left-half zero to the right half and completes the global conclusion.

References

• Truth anchor: D5/S3/Analytic/Adelic/PositiveTorusCarrierCriterion.positive_torus_carrier_condition