HadamardFactorizationStatus
plain-language theorem explainer
The HadamardFactorizationStatus structure packages the differentiability of the pole-removed completed Riemann zeta function, its functional equation, and the Hadamard product representation using data from CompletedZetaHadamardProduct. Number theorists working on explicit formulas within the Recognition Science RH closure plan cite this bundle. It is introduced as a structure definition that directly assembles the Mathlib-supplied facts with the open product interface.
Claim. Let $ζ_0(s)$ denote the pole-removed completed Riemann zeta function. The Hadamard factorization status is the structure asserting that $ζ_0$ is differentiable over $ℂ$, that $ζ_0(s)=ζ_0(1-s)$ for all complex $s$, and that for any data record consisting of a sequence of nonzero zeros, constants $A$ and $B$, and a product limit function, the equality $ζ_0(s)=exp(A+Bs)⋅productLimit(s)$ holds.
background
The HadamardFactorization module implements Track D of the RH unconditional-closure plan. Mathlib supplies the completed zeta function completedRiemannZeta₀ together with its differentiability and the functional equation, but does not provide a Hadamard product. The module therefore introduces the genus-one primary factor and finite partial products, then defines the exact data required to match their limit to completedRiemannZeta₀.
proof idea
The declaration is a structure definition with an empty proof body. It simply declares the three fields: the differentiability of completedRiemannZeta₀ drawn from completedZeta0_differentiable, the functional equation from completedZeta0_functional_equation, and the representation condition phrased directly in terms of the CompletedZetaHadamardProduct data record.
why it matters
This structure earns its place by serving as the practical bundle for Track D, instantiated directly in the definition of hadamardFactorizationStatus which supplies the specific proved components and the Hadamard product map. It bridges Mathlib analytic facts to the missing proof that completedRiemannZeta₀ admits a genus-one Hadamard factorization. In the Recognition Science framework it supports the unconditional closure path for the Riemann Hypothesis by providing the product data type required for explicit formulas, without yet resolving the order or convergence questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.