completedZeta0_functional_equation
plain-language theorem explainer
The pole-removed completed Riemann zeta function satisfies the functional equation equating its value at any complex s with its value at 1 minus s. Number theorists building Hadamard products or explicit formulas cite this result to confirm symmetry of the entire function before taking limits of partial products. The proof is a one-line wrapper that applies symmetry to the known one-substitution lemma for completedRiemannZeta₀.
Claim. For every complex number $s$, the pole-removed completed Riemann zeta function satisfies completedRiemannZeta₀(s) = completedRiemannZeta₀(1 - s).
background
The module HadamardFactorization tracks part D of the Riemann hypothesis unconditional-closure plan. Mathlib supplies the completed Riemann zeta function together with its pole-removed version completedRiemannZeta₀, its differentiability, and its functional equation, but does not yet supply a Hadamard product. This declaration records the functional equation for the pole-removed function so that the limit of genus-one Hadamard partial products can later be identified with completedRiemannZeta₀.
proof idea
The proof is a one-line wrapper that invokes the upstream lemma completedRiemannZeta₀_one_sub at s and then applies symmetry to obtain the stated equality.
why it matters
This theorem supplies the functional-equation field to the HadamardFactorizationStatus record, which also collects the entire-function property and the Hadamard-product data. It advances the explicit-formula interface required by later Recognition Science work in the NumberTheory domain. The module sits inside the unconditional-closure plan for the Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.