XiZeroSummability
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.
claimLet ξ₀ 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 in Recognition Science
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.
scope and limits
- Does not prove that the zeros of ξ₀ satisfy the summability condition.
- Does not construct or verify the Hadamard product representation.
- Does not supply the order bound or any growth estimates for ξ₀.
formal statement (Lean)
177def XiZeroSummability : Prop :=
proof body
Definition body.
178 ∃ ρ : ℕ → ℂ,
179 (∀ n, completedRiemannZeta₀ (ρ n) = 0) ∧
180 (∀ n, ρ n ≠ 0) ∧
181 Summable (fun n => 1 / ‖ρ n‖ ^ 2)
182
183/-- `XiHadamardIdentification`: the genus-one Hadamard factorization of
184`completedRiemannZeta₀`.
185
186Once supplied, `ξ₀(s) = exp(A + B s) · ∏ E₁(s/ρ_n)`. The actual analytic
187proof of this identification is the classical Hadamard theorem, not yet in
188Mathlib. -/