HadamardGenusOneStatus
plain-language theorem explainer
HadamardGenusOneStatus bundles the unconditional norm estimate, summability implication, and multipliability implication for the Weierstrass factor E₁(z) = (1-z)exp(z) together with a placeholder for the open Hadamard identification of completedRiemannZeta₀. Analysts formalizing genus-one products cite this bundle to separate proved estimates from the remaining order bound and zero summability gaps. The declaration is a structure definition that records three proved lemmas and one open hypothesis without derivation.
Claim. A structure HadamardGenusOneStatus with fields: per_factor_estimate asserting ∀ z ∈ ℂ with |z| ≤ 1 we have ‖E₁(z) - 1‖ ≤ 3 |z|² where E₁(z) = (1-z)exp(z); summability_from_sq asserting that for any sequence z:ℕ→ℂ with |z_n|≤1 ∀n, if ∑|z_n|² converges then ∑(E₁(z_n)-1) converges; multipliability_from_sq asserting the same hypotheses imply the infinite product ∏ E₁(z_n) converges; and open_xi_identification mapping any XiHadamardIdentification (zeros ρ_n ≠0, ∑1/|ρ_n|² <∞, constants A,B, and the equality ξ₀(s)=exp(A+Bs)∏E₁(s/ρ_n)) to a proposition.
background
The module supplies the analytic substrate for the genus-one Hadamard factorization of the completed Riemann zeta function ξ₀. The elementary factor is defined by E1(z) := (1-z)·exp(z). XiHadamardIdentification is the target structure that will encode the full product once the order bound, zero summability, and identification are available: ξ₀(s) = exp(A + B s) · ∏ E₁(s/ρ_n) with ∑ 1/‖ρ_n‖² < ∞.
proof idea
This is a structure definition with no proof body. It packages four fields directly. The concrete lemmas norm_E1_sub_one_le, summable_E1_sub_one_of_summable_sq, and multipliable_E1_of_summable_sq are later inserted into an instance of the structure; the open_xi_identification field is filled with the trivial implication fun _ => True.
why it matters
HadamardGenusOneStatus records the Track-D status bundle for the genus-one Hadamard factorization of completedRiemannZeta₀. It is instantiated by hadamardGenusOneStatus, which populates the three proved fields from sibling lemmas while leaving the identification open. The bundle isolates the unconditional results for E₁ from the three open pieces (order bound, zero summability, and identification) required before the factorization ξ₀(s) = exp(A + B s) ∏ E₁(s/ρ_n) can be used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.