Helper results used by the Hadamard/Li development.

This file intentionally contains no global axioms: the deep factorization theorem itself is handled elsewhere; here we only record consequences and clean lemmas that downstream files use.

theorem Hadamard.weierstrass_E_zero' (w : ℂ) : weierstrassE 0 w = 1 - w

For genus 0, the Weierstrass elementary factor is just (1 - w).

Exponentials of linear functions

Basic.lean proves that a zero‑free entire function of finite order is an exponential of a polynomial; here we package the order‑≤1 case as an exponential of a linear function.

theorem Hadamard.polynomial_eval_eq_linear_of_natDegree_le_one (p : Polynomial ℂ) (hp : p.natDegree ≤ 1) : ∃ (a : ℂ) (b : ℂ), ∀ (z : ℂ), Polynomial.eval z p = a * z + b

theorem Hadamard.exp_constraint_from_symmetry (f P : ℂ → ℂ) (c a b : ℂ) (h_symm : ∀ (z : ℂ), f z = f (c - z)) (h_P_symm : ∀ (z : ℂ), P z = P (c - z)) (h_factored : ∀ (z : ℂ), f z = Complex.exp (a * z + b) * P z) (h_P_nonzero_0 : P 0 ≠ 0) : Complex.exp (a * c) = 1

Exponential constraint from symmetry

If f satisfies f(z) = f(c - z) for some c, and f = exp(az + b) * P(z) where P is a symmetric product (P(z) = P(c - z)), then exp(a * c) = 1.

This means a * c ∈ 2πiℤ. For real a and real c (as in the ξ function with c = 1), this forces a * c = 0 since the only real element of 2πiℤ is 0.

For ξ, we have ξ(s) = ξ(1-s) with c = 1. If a is real, then a = 0.

Reference: This is a consequence of comparing f(z) = f(c-z) with the factored form.

theorem Hadamard.linear_coeff_zero_of_real_symmetry (f P : ℂ → ℂ) (c a : ℝ) (b : ℂ) (h_symm : ∀ (z : ℂ), f z = f (↑c - z)) (h_P_symm : ∀ (z : ℂ), P z = P (↑c - z)) (h_factored : ∀ (z : ℂ), f z = Complex.exp (↑a * z + b) * P z) (h_P_nonzero_0 : P 0 ≠ 0) : a * c = 0

Linear coefficient vanishes for real symmetry

Corollary: If additionally a and c are real, then exp(ac) = 1 implies ac = 0. The only real number w with exp(w) = 1 is w = 0.