hadamardFactorizationStatus
plain-language theorem explainer
The definition constructs the HadamardFactorizationStatus record by directly assigning the differentiability of completedRiemannZeta₀, its functional equation, and the Hadamard product representation to the three fields of the structure. Number theorists working on explicit formulas or Track D of the Riemann hypothesis closure plan would cite this bundle to obtain the genus-one factorization interface in one place. The construction is a record literal that references three upstream theorems in the same module with no additional reasoning.
Claim. The Hadamard factorization status is the record whose fields assert that the pole-removed completed zeta function $ζ_0$ is differentiable on $ℂ$, satisfies $ζ_0(s)=ζ_0(1-s)$ for all $s∈ℂ$, and equals the genus-one product $e^{A+Bs}⋅P(s)$ once a CompletedZetaHadamardProduct data record supplies the constants $A,B$ and the product limit $P$.
background
The HadamardFactorization module tracks Track D of the RH unconditional-closure plan. Mathlib already supplies the pole-removed completed zeta function completedRiemannZeta₀ together with its differentiability and functional equation, but does not yet provide a Hadamard product. The module therefore introduces the genus-one primary factor, finite partial products, and the exact data type needed to identify their limit with completedRiemannZeta₀. The referenced structure HadamardFactorizationStatus packages the two proved Mathlib properties with the open Hadamard product interface. Upstream theorems establish differentiability of completedRiemannZeta₀ everywhere and the symmetry completedRiemannZeta₀ s = completedRiemannZeta₀ (1-s).
proof idea
The definition is a direct record construction that populates the three fields of HadamardFactorizationStatus by assigning the theorems completedZeta0_differentiable, completedZeta0_functional_equation, and completedRiemannZeta0_hadamard_product to the corresponding slots.
why it matters
This definition supplies the practical bundle for Track D of the RH closure plan by packaging the Mathlib inputs with the interface for the genus-one Hadamard factorization. It serves as the entry point for later explicit-formula work that requires the product representation of completedRiemannZeta₀. No downstream uses are recorded yet, leaving the Hadamard product data as an open interface to be supplied by future theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.