Weil-Square Positivity Criteria Under Infinitely Many Zeros

Abstract

Assuming infinitely many nontrivial zeros, the Riemann hypothesis is equivalent to repository Weil-square positivity for every ZeroData and for some ZeroData.

Theorem 1.1 (RH is equivalent to positivity for every ZeroData).

$$\mathrm{Infinite}\left(\{\rho \mid \mathrm{IsNontrivialZero}\left(\rho \right)\}\right)\Rightarrow \left(\mathrm{RiemannHypothesis}\iff \left(\forall Z\in ZeroData,\forall g\in WeilTestFunction,hZero\in \mathrm{SymmetricConvergent}\left(Z,\mathrm{convolutionSquare}\left(g\right)\right),0\le \Re (\mathrm{zeroSum}\left(Z,\mathrm{convolutionSquare}\left(g\right),hZero\right))\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/Separator/WeilSquarePositivityCriterionOfInfinite.rh_iff_forall_zeroData_weilSquarePositivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The hypothesis hInf is M1-b, infinitely many nontrivial zeros, and is not proved in this repository. The ZeroData construction used behind M1-a is noncomputable and depends on Classical.choice.

The right side is this repository’s Weil-square positivity for zeroSum and convolutionSquare. The results bind the frozen fixed-Z criterion and nonemptiness bridge; these conditional equivalences are not a proof of RH.

Theorem 1.2 (RH is equivalent to positivity for some ZeroData).

$$\mathrm{Infinite}\left(\{\rho \mid \mathrm{IsNontrivialZero}\left(\rho \right)\}\right)\Rightarrow \left(\mathrm{RiemannHypothesis}\iff \left(\exists Z\in ZeroData,\forall g\in WeilTestFunction,hZero\in \mathrm{SymmetricConvergent}\left(Z,\mathrm{convolutionSquare}\left(g\right)\right),0\le \Re (\mathrm{zeroSum}\left(Z,\mathrm{convolutionSquare}\left(g\right),hZero\right))\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/Separator/WeilSquarePositivityCriterionOfInfinite.rh_iff_exists_zeroData_weilSquarePositivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The hypothesis hInf is M1-b, infinitely many nontrivial zeros, and is not proved in this repository. The ZeroData construction used behind M1-a is noncomputable and depends on Classical.choice.

The right side is this repository’s Weil-square positivity for zeroSum and convolutionSquare. The results bind the frozen fixed-Z criterion and nonemptiness bridge; these conditional equivalences are not a proof of RH.

References

• Truth anchor: D5/S3/Weil/Separator/WeilSquarePositivityCriterionOfInfinite.rh_iff_exists_zeroData_weilSquarePositivity
• Truth anchor: D5/S3/Weil/Separator/WeilSquarePositivityCriterionOfInfinite.rh_iff_forall_zeroData_weilSquarePositivity
• Dependency: D5/S3/Weil/Separator/WeilSquarePositivityCriterion
• Dependency: D5/S3/Weil/ZetaBridge/ZeroDataNonemptyIffInfinite