module module high

`IndisputableMonolith.NumberTheory.HadamardGenusOne`

This module defines the genus-one Weierstrass elementary factor E1(z) = (1 - z) exp(z) and records its algebraic values, norm bounds, and summability criteria. Analytic number theorists constructing Hadamard products for the xi function cite these results when isolating individual zero factors. The module consists of a central definition followed by short lemmas that apply direct substitution and Mathlib norm estimates.

claimThe genus-one elementary factor is $E_1(z) = (1 - z) e^z$.

background

Recognition Science expresses the xi function through a genus-one Hadamard product over its zeros. This module supplies the local factor E1(z) = (1 - z) exp(z) that appears once for each zero in the product. The factor satisfies E1(0) = 1 and E1(1) = 0 while the exponential term controls the linear growth required for order-one entire functions.

proof idea

This is a definition module. The central definition sets E1(z) = (1 - z) exp(z). The remaining declarations compute E1 at 0 and 1 by substitution, derive norm inequalities from the series for exp, and apply Mathlib summability and multipliability predicates to families indexed by the zeros.

why it matters in Recognition Science

HadamardRegularTail imports this module to split xi0 at any chosen zero index k into the local factor E1(s / zeros k) and the regular tail of the remaining product. The splitting supports the full Hadamard identification of the xi function and connects the zero set to the phi-ladder structure in the Recognition framework.

scope and limits

Does not establish convergence of the infinite product over all zeros.
Does not locate the zeros or connect them to the phi-ladder.
Does not include the exponential prefactor or constant term of the full factorization.
Does not treat higher-genus factors or order greater than one.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.HadamardRegularTail module_import

declarations in this module (17)

def E1 L38
theorem E1_zero L40
theorem E1_one L42
theorem E1_sub_one_eq L45
theorem norm_exp_sub_one_le_two_mul L55
theorem norm_E1_sub_one_le L75
theorem summable_norm_E1_sub_one_of_summable_sq L101
theorem summable_E1_sub_one_of_summable_sq L114
theorem multipliable_E1_of_summable_sub_one L124
theorem multipliable_E1_of_summable_sq L135
theorem norm_E1_sub_one_at_quotient_le L146
def XiOrderBound L169
def XiZeroSummability L177
structure XiHadamardIdentification L189
theorem completedRiemannZeta0_genus_one_factorization L204
structure HadamardGenusOneStatus L215
def hadamardGenusOneStatus L228