Li Curvature Criterion

Abstract

Toeplitz positivity of every Li-curvature section is equivalent to the Riemann hypothesis under the stated representation interfaces.

Theorem 1.1 (Li curvature criterion).

$$\forall c\in \mathrm{Integer}\left(\right)\to \mathrm{Complex}\left(\right),lambda\in \mathrm{Natural}\left(\right)\to \mathrm{Real}\left(\right),\left(\left(\left(\left(\left(\left(\mathrm{RiemannHypothesis}\left(\right)\iff \left(\forall n\in \mathrm{Natural}\left(\right),0\le lambda\left(n\right)\right)\right)\wedge lambda\left(0\right)=0\right)\wedge 0\le lambda\left(1\right)\right)\wedge \left(\forall n\in \mathrm{Natural}\left(\right),1\le n\Rightarrow lambda\left(n+1\right)-2\cdot lambda\left(n\right)+lambda\left(n-1\right)=2\cdot lambda\left(1\right)\cdot \mathrm{realPart}\left(c\left(n\right)\right)\right)\right)\wedge \left(\mathrm{RiemannHypothesis}\left(\right)\Rightarrow \left(\exists mu\in \mathrm{Measure}\left(\mathrm{Circle}\left(\right)\right),\mathrm{IsProbabilityMeasure}\left(mu\right)\wedge \left(\forall k\in \mathrm{Integer}\left(\right),c\left(k\right)=\mathrm{circleMoment}\left(mu,k\right)\right)\right)\right)\right)\wedge \left(\left(\forall N\in \mathrm{Natural}\left(\right),\mathrm{PosSemidef}\left(\mathrm{toeplitzMatrix}\left(c,N\right)\right)\right)\Rightarrow \left(\exists mu\in \mathrm{Measure}\left(\mathrm{Circle}\left(\right)\right),\mathrm{IsProbabilityMeasure}\left(mu\right)\wedge \left(\forall k\in \mathrm{Integer}\left(\right),c\left(k\right)=\mathrm{circleMoment}\left(mu,k\right)\right)\right)\right)\right)\Rightarrow \left(\mathrm{RiemannHypothesis}\left(\right)\iff \left(\forall N\in \mathrm{Natural}\left(\right),\mathrm{PosSemidef}\left(\mathrm{toeplitzMatrix}\left(c,N\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/LiCurvatureCriterion.li_curvature_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The statement keeps the Li criterion, the canonical initial data and curvature recurrence, and the two common probability-measure representations as explicit interfaces. These are the ingredients not supplied together by the pinned library.

For the forward direction, the circle-moment representation turns each Toeplitz quadratic form into the integral of the squared modulus of its analytic coefficient polynomial.

For the reverse direction, the finite geometric polynomial has empty sum at zero. Its squared modulus reconstructs a nonnegative Li sequence with the prescribed first two values and second differences. Two-step recurrence uniqueness identifies it with the supplied Li sequence, after which the Li criterion applies.

References

• Truth anchor: D5/S3/Weil/TestFunctions/LiCurvatureCriterion.li_curvature_criterion
• Dependency: D5/S3/Weil/TestFunctions/LiCurvatureFourierRepresentation