XiHadamardIdentification
XiHadamardIdentification packages a sequence of nonzero complex zeros together with constants A and B such that the completed Riemann zeta function equals exp(A + B s) times the infinite product of genus-one Weierstrass factors E1(s over each zero). Analytic number theorists formalizing entire-function representations of zeta would cite the structure once the order bound and zero summability are supplied. The declaration itself is a bare structure definition whose analytic content is the classical Hadamard theorem, external to the current Mathl
claimA structure consisting of a sequence of nonzero complex numbers $ρ_n$, constants $A,B∈ℂ$, and the identity $ξ_0(s)=e^{A+Bs}∏'_n E_1(s/ρ_n)$ for all $s∈ℂ$, where $E_1(z)=(1-z)e^z$ and the product converges absolutely.
background
The module supplies the concrete analytic substrate for the genus-one Hadamard factorization of the completed Riemann zeta function. Mathlib does not package the Hadamard factorization theorem for entire functions of order ≤1, so the module proves only the unconditional prerequisites for the elementary Weierstrass factor E1(z)=(1-z)exp(z): the per-factor norm bound ‖E1(z)−1‖≤3‖z‖² for ‖z‖≤1, absolute summability of the corrections E1(z_n)−1 from summability of ‖z_n‖², and multipliability of the partial products. Three named pieces remain open: the order bound XiOrderBound, the inverse-square summability XiZeroSummability, and the identification XiHadamardIdentification itself.
proof idea
This declaration is a structure definition that collects the data and the identification equality; it contains no proof steps, tactics, or lemmas.
why it matters in Recognition Science
It is the third open analytic piece listed in the module documentation and is used directly by the theorem completedRiemannZeta0_genus_one_factorization to instantiate the factorization ξ₀(s)=exp(A+Bs)∏ E1(s/ρ_n). It also appears inside the status bundle HadamardGenusOneStatus. In the Recognition framework the structure supplies the zero-product representation required for further arguments about the zeta function once the missing order and summability hypotheses are discharged.
scope and limits
- Does not prove that completedRiemannZeta₀ has order at most one.
- Does not establish summability of 1/‖ρ_n‖² over the zeros.
- Does not contain the classical Hadamard factorization theorem.
- Does not compute explicit values for the constants A or B.
Lean usage
theorem completedRiemannZeta0_genus_one_factorization (H : XiHadamardIdentification) (s : ℂ) : completedRiemannZeta₀ s = Complex.exp (H.A + H.B * s) * ∏' n, E1 (s / H.zeros n) := H.identification sformal statement (Lean)
189structure XiHadamardIdentification where
190 zeros : ℕ → ℂ
191 zeros_ne_zero : ∀ n, zeros n ≠ 0
192 inv_sq_summable : Summable (fun n => 1 / ‖zeros n‖ ^ 2)
193 A : ℂ
194 B : ℂ
195 identification :
196 ∀ s : ℂ,
197 completedRiemannZeta₀ s =
198 Complex.exp (A + B * s) * ∏' n, E1 (s / zeros n)
199
200/-! ## 7. What the supplied data gives -/
201
202/-- Once `XiHadamardIdentification` is supplied, `completedRiemannZeta₀`
203factors as the genus-one product times an exponential. -/