IndisputableMonolith.NumberTheory.HadamardFactorization
The HadamardFactorization module supplies the Weierstrass product form for the completed zeta function after pole removal. Number theorists working inside the Recognition Science zeta program cite it to access the explicit factorization and differentiability statements. The module consists of targeted definitions for the order-one exponential factor, finite partial products, and the assembled entire function, all resting on the upstream functional equation.
claimLet $Z(s)$ denote the completed zeta function with its poles removed. Then $Z$ is differentiable at every point of the complex plane, and admits the Hadamard product representation $Z(s) = e^{A+Bs} s^m (1-s) e^{s} P(s)$ where $P(s)$ is the canonical product over the non-trivial zeros.
background
This module belongs to the NumberTheory section of the Recognition Science development and imports only ZetaFromTheta. The upstream module isolates a theta-style Mellin transform that yields the completed zeta functional equation without claiming a full analytic proof of the Mellin inversion. The present module therefore works in the setting where the completed zeta is already known to satisfy the functional equation and proceeds to its Weierstrass factorization. Key objects introduced are the auxiliary entire function of order one (hadamardE1), the truncated products (hadamardPartialProduct), and the global factorization (CompletedZetaHadamardProduct).
proof idea
This is a definition module, no proofs. It declares the required auxiliary functions, states the differentiability claim for the pole-removed completed zeta, and assembles the Hadamard product from the upstream functional equation data.
why it matters in Recognition Science
The module supplies the explicit product representation required for zero-distribution arguments later in the RS zeta program. It completes the analytic bridge begun in ZetaFromTheta and prepares the ground for any subsequent counting or density statements that rely on the Hadamard form. No downstream declarations are recorded yet, but the factorization is the natural next step after the functional equation is in place.
scope and limits
- Does not locate or count the zeros of the completed zeta.
- Does not derive the functional equation from the theta function.
- Does not address convergence rates of the infinite product.
- Does not connect the factorization to the Riemann hypothesis.
depends on (1)
declarations in this module (10)
-
theorem
completedZeta0_differentiable -
theorem
completedZeta0_functional_equation -
def
hadamardE1 -
theorem
hadamardE1_zero -
def
hadamardPartialProduct -
theorem
hadamardPartialProduct_zero -
structure
CompletedZetaHadamardProduct -
theorem
completedRiemannZeta0_hadamard_product -
structure
HadamardFactorizationStatus -
def
hadamardFactorizationStatus