hadamardE1_zero
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 in Recognition Science
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.
scope and limits
- Does not establish convergence of the infinite product.
- Does not invoke the functional equation of the completed zeta function.
- Does not address the distribution or multiplicity of zeros.
formal statement (Lean)
45@[simp] theorem hadamardE1_zero : hadamardE1 0 = 1 := by
proof body
Term-mode proof.
46 simp [hadamardE1]
47
48/-- The finite genus-one product over the first `N` listed zeros. -/