hadamardPartialProduct_zero
plain-language theorem explainer
The base case of the genus-one partial Hadamard product over a sequence of complex zeros evaluates to unity when the factor count is zero. Researchers constructing explicit formulas or closing the Riemann hypothesis via Hadamard representations would cite this identity to anchor inductive arguments on finite products. The proof is a direct simplification that unfolds the definition of the partial product at the zero-factor index.
Claim. Let $(z_n)_{n=0}^N$ be any sequence of complex numbers and let $N$ be a natural number. The genus-one partial Hadamard product with zero factors equals $1$.
background
This module supplies the product interface for Track D of the unconditional RH closure plan. Mathlib already provides the completed zeta function, its differentiability, and functional equation, but no Hadamard product for the pole-removed version completedRiemannZeta₀. The module therefore defines the genus-one primary factor together with its finite partial products so that later explicit-formula work can identify their limit with completedRiemannZeta₀ up to an exponential factor exp(A + B s).
proof idea
The proof is a one-line wrapper that applies simp to the definition of the partial product, which returns the empty product (equal to 1) when the factor index is zero.
why it matters
The identity supplies the base case required for any inductive construction of the Hadamard product in the explicit-formula program. It directly supports the eventual statement that the partial products converge to the pole-removed completed zeta (see sibling completedRiemannZeta0_hadamard_product). The declaration fills the initial data point in Track D, where the remaining analytic work is to prove that completedRiemannZeta₀ has order at most one and that the genus-one product converges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.