hadamardE1_zero
plain-language theorem explainer
The genus-one Hadamard factor evaluates to unity at the origin. Researchers building explicit formulas for the completed zeta function cite this normalization to anchor partial products. The proof reduces directly to the definition of the factor via a single simplification step.
Claim. $E_1(0) = 1$ where the genus-one elementary factor is given by $E_1(z) = (1 - z) e^z$.
background
The HadamardFactorization module develops the product representation needed for explicit-formula work on the completed Riemann zeta function, as part of tracking step D in the RH unconditional-closure plan. It introduces the genus-one primary factor whose definition is $E_1(z) = (1 - z) e^z$. Upstream results supply the unit elements in the integer and rational structures from logic, together with the spin-1 and phi-closed units, to support the algebraic reductions.
proof idea
The proof is a one-line simp tactic that unfolds the definition of hadamardE1 at argument zero and evaluates the resulting expression (1 - 0) * exp(0) to 1.
why it matters
This normalization fixes the constant term for the finite partial products and the eventual Hadamard product identification with completedRiemannZeta0. It supplies the base case required by the genus-one factorization interface in the Recognition Science framework, consistent with the overall plan to close the Riemann hypothesis unconditionally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.