Prime-Archimedean Poincare Criterion

Abstract

Relative to supplied zero data, RH is equivalent to the Prime-Archimedean Poincare inequality at every support radius and at some support radius.

Theorem 1.1 (RH is equivalent to every-radius Prime-Archimedean Poincare).

$$\forall Z\in ZeroData,\mathrm{RiemannHypothesis}\iff \left(\forall f\in WeilTestFunction,L\in \mathbb{R},\mathrm{tsupport}\left(f\right)\subseteq [-L,L]\Rightarrow \left(2\cdot \mathrm{totalPrimeWeight}\left(L\right)-\mathrm{archimedeanConstant}\right)\cdot l2Mass\left(f\right)\le 2|{\int }_{\mathbb{R}}\exp \left(\frac{x}{2}\right)f\left(x\right)dx{|}^2+\mathrm{archimedeanJumpEnergy}\left(f\right)+\mathrm{arithmeticJumpEnergy}\left(L,f\right)\right)$$

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

Source. Repository-derived.

Commentary.

The energy decomposition is the frozen theorem PrimeArchimedeanEnergyIdentity proved by another driver and is only bound here; no part of that identity is reproved.

Both criteria are relative to a ZeroData only. Existence of ZeroData is not asserted, M1-b remains open, and these equivalences are not a proof of RH.

The quantified test functions are this repository’s WeilTestFunction. The support radius L is any real satisfying tsupport f subset [-L,L]. The existential-radius criterion records that, through the frozen identity, the inequality’s truth is independent of which valid radius is chosen.

The left side is the coherent prime mass minus the Archimedean constant, multiplied by the L2 mass. The right side is twice the squared boundary readout plus the Archimedean and arithmetic jump energies.

Theorem 1.2 (RH is equivalent to existential-radius Prime-Archimedean Poincare).

$$\forall Z\in ZeroData,\mathrm{RiemannHypothesis}\iff \left(\forall f\in WeilTestFunction,\exists L\in \mathbb{R},\mathrm{tsupport}\left(f\right)\subseteq [-L,L]\wedge \left(2\cdot \mathrm{totalPrimeWeight}\left(L\right)-\mathrm{archimedeanConstant}\right)\cdot l2Mass\left(f\right)\le 2|{\int }_{\mathbb{R}}\exp \left(\frac{x}{2}\right)f\left(x\right)dx{|}^2+\mathrm{archimedeanJumpEnergy}\left(f\right)+\mathrm{arithmeticJumpEnergy}\left(L,f\right)\right)$$

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

Source. Repository-derived.

Commentary.

The energy decomposition is the frozen theorem PrimeArchimedeanEnergyIdentity proved by another driver and is only bound here; no part of that identity is reproved.

Both criteria are relative to a ZeroData only. Existence of ZeroData is not asserted, M1-b remains open, and these equivalences are not a proof of RH.

The quantified test functions are this repository’s WeilTestFunction. The support radius L is any real satisfying tsupport f subset [-L,L]. The existential-radius criterion records that, through the frozen identity, the inequality’s truth is independent of which valid radius is chosen.

The left side is the coherent prime mass minus the Archimedean constant, multiplied by the L2 mass. The right side is twice the squared boundary readout plus the Archimedean and arithmetic jump energies.

References

• Truth anchor: D5/S3/Weil/Separator/PrimeArchimedeanPoincareCriterion.rh_iff_exists_supportRadius_primeArchimedeanPoincare
• Truth anchor: D5/S3/Weil/Separator/PrimeArchimedeanPoincareCriterion.rh_iff_primeArchimedeanPoincare
• Dependency: D5/S3/Weil/Separator/ArchimedeanConvergence
• Dependency: D5/S3/Weil/Separator/WeilSquarePositivityCriterion
• Dependency: D5/S3/Weil/ZetaBridge/PrimeArchimedeanEnergyIdentity
• Dependency: D5/S3/Weil/ZetaBridge/SymmetricConvergentOfZetaSummable