HadamardGenusOneStatus
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove that completedRiemannZeta₀ has order ≤1.
- Does not prove summability of 1/‖ρ_n‖² for the zeros of ξ₀.
- Does not establish the Hadamard product identification for ξ₀.
- Does not derive the constants A and B in the exponential prefactor.
- Does not address functions of order >1 or higher-genus factorizations.
formal statement (Lean)
215structure HadamardGenusOneStatus where
216 per_factor_estimate :
217 ∀ z : ℂ, ‖z‖ ≤ 1 → ‖E1 z - 1‖ ≤ 3 * ‖z‖ ^ 2
218 summability_from_sq :
219 ∀ z : ℕ → ℂ, (∀ n, ‖z n‖ ≤ 1) →
220 Summable (fun n => ‖z n‖ ^ 2) →
221 Summable (fun n => E1 (z n) - 1)
222 multipliability_from_sq :
223 ∀ z : ℕ → ℂ, (∀ n, ‖z n‖ ≤ 1) →
224 Summable (fun n => ‖z n‖ ^ 2) →
225 Multipliable (fun n => E1 (z n))
226 open_xi_identification : XiHadamardIdentification → Prop
227