IndisputableMonolith.NumberTheory.HadamardFactorization
The HadamardFactorization module supplies the infinite-product representation of the pole-removed completed zeta function inside the Recognition Science zeta program. It extends the theta-to-zeta bridge imported from ZetaFromTheta by adding the explicit factorization over zeros. Analytic number theorists working in the RS setting would cite it for the product form required in zero-distribution arguments. The module assembles auxiliary factors and invokes Mathlib entire-function machinery to reach the main product statement.
claimLet $\hat{\zeta}(s)$ be the completed zeta function with poles removed. Then $\hat{\zeta}(s)$ is entire of order one and equals $e^{A+Bs}\prod_{\rho}(1-s/\rho)e^{s/\rho}$, where the product runs over the zeros $\rho$.
background
The module belongs to Phase 4 of the RS-native zeta program and imports directly from ZetaFromTheta. That upstream module isolates the bridge between the Recognition Theta program and the completed zeta functional equation by means of a theta-style Mellin transform, without claiming a full analytic continuation proof. Local definitions include hadamardE1 (the exponential prefactor), hadamardPartialProduct (finite truncations), and CompletedZetaHadamardProduct (the assembled statement). The setting assumes the completed zeta satisfies the functional equation and is of finite order so that the classical Hadamard theorem applies.
proof idea
The module first records that the pole-removed completed zeta is differentiable everywhere (via Mathlib). It then defines the exponential factor hadamardE1 and the partial products, proves their zero sets coincide with those of the completed zeta, and assembles the infinite product in completedRiemannZeta0_hadamard_product. The argument is a sequence of lemmas that reduce the factorization claim to the standard Hadamard theorem for entire functions of order one.
why it matters in Recognition Science
This module supplies the explicit product form that the RS zeta program requires after the functional equation has been established in ZetaFromTheta. It therefore feeds any later zero-counting or distribution results inside the Recognition framework. The module closes the step from the theta-Mellin bridge to the Hadamard representation, enabling further Recognition Science applications that rely on the product over zeros.
scope and limits
- Does not locate the zeros or prove the Riemann hypothesis.
- Does not supply convergence estimates for the product beyond order-one entire functions.
- Does not connect the factorization to the phi-ladder or Recognition mass formula.
- Does not reproduce the full theta/Mellin analytic continuation.
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