hadamardGenusOneStatus
plain-language theorem explainer
This definition assembles the HadamardGenusOneStatus record by supplying the proved norm bound on the genus-one factor E1(z), summability of the corrections E1(zn)-1, and multipliability of the product under square-summable bounded zeros. Analysts working on the Hadamard factorization of the completed Riemann zeta function cite this status bundle as the concrete analytic substrate. The construction is a direct structure record that references three upstream theorems for the filled fields while marking the identification step as trivial.
Claim. The Hadamard genus-one status is the record containing the estimate $||E_1(z)-1||≤3||z||^2$ for $||z||≤1$, the implication that square-summability of bounded $z_n$ yields summability of $E_1(z_n)-1$, and the implication that the same hypothesis yields multipliability of the product $∏E_1(z_n)$.
background
The module supplies the analytic substrate for the genus-one Hadamard factorization of entire functions of order ≤1. The elementary factor is E₁(z)=(1-z)exp(z). The HadamardGenusOneStatus structure bundles three proved properties: the per-factor norm estimate, summability of the corrections E₁(z_n)-1 from square-summability of the z_n, and multipliability of the partial products. Three steps remain open: the order bound on completedRiemannZeta₀, summability of the inverse-square moduli of its zeros, and identification of the product limit with the zeta function up to an exponential factor.
proof idea
The definition constructs the HadamardGenusOneStatus instance by assigning the per-factor estimate to norm_E1_sub_one_le, the summability field to summable_E1_sub_one_of_summable_sq, the multipliability field to multipliable_E1_of_summable_sq, and the open identification field to the constant-true function.
why it matters
This definition collects the unconditionally proved prerequisites for the genus-one Hadamard product in the Recognition Science framework. It feeds the open tasks of bounding the order of completedRiemannZeta₀, establishing zero summability, and performing the identification step. The module records that Mathlib lacks the general Hadamard theorem for order ≤1, so these concrete estimates for E₁ close the provable portion of the analytic substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.