E1_one
plain-language theorem explainer
The genus-one Weierstrass factor E₁ vanishes at z = 1. Analysts building Hadamard products for order-one entire functions cite this normalization when forming partial products over zeros. The proof is a direct algebraic simplification from the explicit definition of E₁.
Claim. $E_1(1) = 0$
background
The module supplies the analytic substrate for genus-one Hadamard factorization of entire functions of order at most one. The elementary factor is defined by $E_1(z) := (1 - z) e^z$. This supplies the per-factor norm bound, absolute summability of corrections from summable squared moduli, and multipliability of the partial products that are the prerequisites for the Hadamard product itself.
proof idea
The proof is a one-line term-mode simplification that unfolds the definition of E₁ at argument 1 and cancels the resulting zero factor.
why it matters
The identity normalizes the genus-one product at the unit point and feeds the norm and summability lemmas that follow in the same module. It therefore contributes to the three open pieces required for the full Hadamard identification of the completed Riemann zeta function. Within Recognition Science it anchors the zero-product representation used in the number-theoretic applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.