CompletedZetaFunctionalEquationCert
plain-language theorem explainer
CompletedZetaFunctionalEquationCert packages a map from the complex plane to itself that coincides with the completed Riemann zeta function and obeys the reflection symmetry sending s to 1-s. Researchers tracing the Recognition Science zeta program cite it to obtain an unconditional functional equation while the full theta-Mellin bridge remains open. The declaration is a bare structure definition that records the two properties with no further computation.
Claim. A structure consisting of a function $f : ℂ → ℂ$ together with the statements that $f(s)$ equals the completed Riemann zeta function for every complex $s$ and that $f(s) = f(1-s)$ for every complex $s$.
background
The structure sits in the ZetaFromTheta module, Phase 4 of the RS-native zeta program. That module isolates a theta-style Mellin transform compatible with the completed zeta function without claiming a full analytic proof; the unconditional functional equation is still supplied by Mathlib. ThetaCompletedZetaBridge records an analytic bridge in which a completed Mellin transform agrees with the completed Riemann zeta and inherits reflection symmetry from the Mellin transform. LogicThetaZetaBridge further packages this bridge with a recovered-complex substrate. The upstream arithmetic zeta function is the constant-1 function on positive integers.
proof idea
The declaration is a structure definition with an empty proof body. It simply declares the three fields: the completed Mellin map, the pointwise agreement with the completed Riemann zeta, and the reflection property.
why it matters
The certificate is inhabited unconditionally by the downstream definition completedZetaFunctionalEquationCert, which takes the completed Riemann zeta itself. It is also produced from any ThetaCompletedZetaBridge and is consumed by the theorem completed_zeta_functional_equation_from_cert that extracts the functional equation. In the Recognition framework it supplies the Phase 4 bridge to the functional equation while the stronger ThetaCompletedZetaBridge (requiring the Recognition Theta modular identity) stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.