completed_zeta_functional_equation_from_cert
plain-language theorem explainer
Any certificate asserting that an auxiliary Mellin transform matches the completed Riemann zeta function and obeys the reflection property immediately yields the functional equation for the completed zeta. Researchers formalizing the Recognition Theta to zeta bridge in the RS-native program would cite this when isolating the Mellin step. The proof is a direct term-mode rewriting that substitutes the three certificate properties.
Claim. Let $f : ℂ → ℂ$ be any function such that $f(s) = ζ^*(s)$ for all $s ∈ ℂ$ and $f(s) = f(1-s)$ for all $s ∈ ℂ$, where $ζ^*$ denotes the completed Riemann zeta function. Then $ζ^*(s) = ζ^*(1-s)$ for all $s ∈ ℂ$.
background
This theorem resides in the ZetaFromTheta module, phase 4 of the RS-native zeta program. The module isolates the precise bridge between a theta-style Mellin transform and the completed zeta functional equation, without claiming a full analytic formalization. The central object is the certificate structure CompletedZetaFunctionalEquationCert, which packages a function completedMellin together with the two properties that it matches completedRiemannZeta pointwise and satisfies the reflection completedMellin s = completedMellin (1-s).
proof idea
The proof is a one-line term-mode wrapper. It obtains the matching equality for the input s, the reflection equality, and the matching equality for 1-s directly from the certificate fields, then rewrites the left-hand side through these three equalities.
why it matters
The declaration supplies the final logical step that turns any valid Mellin bridge certificate into the functional equation itself, supporting the Recognition Theta program. It sits immediately downstream of the CompletedZetaFunctionalEquationCert structure and records the exact point at which the theta/Mellin bridge would render the completed zeta equation RS-native. The module explicitly notes that the unconditional equation remains Mathlib's completedRiemannZeta_one_sub while this result isolates the RS-native route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.