XiZeroSummability
plain-language theorem explainer
XiZeroSummability defines the proposition that the non-zero zeros of the completed Riemann zeta function ξ₀ admit an enumeration ρ_n such that the series ∑ 1/‖ρ_n‖² converges. Analysts preparing the genus-one Hadamard factorization for entire functions of order ≤1 would cite this as a required hypothesis on zero distribution. The declaration is a direct definition that encodes the classical consequence of Jensen's formula without applying auxiliary lemmas.
Claim. Let ξ₀ denote the completed Riemann zeta function. The proposition asserts that there exists a sequence (ρ_n)_{n∈ℕ} of non-zero complex numbers such that ξ₀(ρ_n)=0 for all n and ∑_{n=1}^∞ 1/‖ρ_n‖² < ∞.
background
The module NumberTheory.HadamardGenusOne supplies analytic prerequisites for the genus-one Hadamard factorization of ξ₀. It develops norm bounds and summability properties for the Weierstrass factor E₁(z)=(1-z)exp(z) under the assumption that zero moduli satisfy suitable decay. XiZeroSummability isolates the concrete summability condition on the inverse squares of the zero moduli, which follows from Jensen's formula plus zero counting but is not yet packaged in Mathlib for this function. The local setting is the concrete substrate needed before the full product identification can be stated.
proof idea
The declaration is a direct definition of the Prop. It packages the existence of an enumeration of the zeros of ξ₀ together with the summability of 1/‖ρ_n‖², using only the standard Mathlib notions of Summable and the zero predicate.
why it matters
This definition is one of the three open scaffolding items listed in the module documentation, alongside XiOrderBound (growth order ≤1) and XiHadamardIdentification (product equality). It is referenced by the sibling declaration XiOrderBound and supplies the zero-distribution hypothesis required for the partial products of E₁(s/ρ_n) to converge. In the Recognition Science framework the zero structure of ξ₀ supports the functional equation that forces the constants c=1, ħ=φ^{-5} and the phi-ladder mass formula, though the link remains indirect through number-theoretic input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.