CompletedZetaHadamardProduct
plain-language theorem explainer
CompletedZetaHadamardProduct packages an enumeration of nonzero complex zeros together with constants A and B and a limit function for the genus-one partial products so that the pole-removed completed zeta equals exp(A + B s) times that limit. Analytic number theorists working on explicit formulas or the Riemann hypothesis would cite the structure as the precise data interface required for Track D. It is introduced as a bare structure definition whose fields record the convergence and identification conditions with no proof body.
Claim. A structure consisting of a sequence of nonzero complex numbers $(z_n)_{n∈ℕ}$, complex constants $A,B∈ℂ$, and a function $P:ℂ→ℂ$ such that the partial products formed from the zeros converge to $P(s)$ as the truncation index tends to infinity and the pole-removed completed zeta function satisfies $ζ_0(s)=exp(A+Bs)⋅P(s)$ for all $s∈ℂ$.
background
The HadamardFactorization module forms Track D of the RH unconditional-closure plan. Mathlib supplies the completed zeta function and the entire pole-removed function completedRiemannZeta₀ together with its differentiability and the functional equation completedRiemannZeta₀(s)=completedRiemannZeta₀(1−s), but does not provide a Hadamard product. The module therefore defines the genus-one primary factor and finite partial products, then packages the exact data needed to identify their limit with completedRiemannZeta₀ up to the exponential prefactor.
proof idea
This declaration is a structure definition with an empty proof body. It simply lists the seven fields that encode the zeros, the prefactor constants, the limit function, the convergence condition on the partial products, and the identification with completedRiemannZeta₀.
why it matters
The structure supplies the central data interface for the Hadamard factorization theorem completedRiemannZeta0_hadamard_product, which extracts the equality field to obtain the factorization, and appears in HadamardFactorizationStatus to bundle the Mathlib facts with this open data type. In the Recognition framework it closes the product interface for explicit-formula work in Track D once the order-at-most-one property and zero enumeration are established; it leaves open the analytic proof that the genus-one partial products converge to the completed zeta up to exp(A+Bs).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.