completed_zeta_functional_equation_from_mellin
plain-language theorem explainer
The theorem shows that once a bridge identifies the completed Mellin transform of the Recognition theta kernel with the completed Riemann zeta function and carries the Mellin reflection to the map s to 1-s, the completed zeta satisfies the functional equation. Phase 4 of the RS zeta program cites this result to transfer symmetry properties from the theta side. The proof is a direct term-mode rewriting that substitutes the bridge's matching and reflection axioms at s and at 1-s.
Claim. If a bridge supplies a completed Mellin transform $M$ such that $M(s)$ equals the completed Riemann zeta function at every complex $s$ and $M(s) = M(1-s)$ for all $s$, then the completed Riemann zeta at $s$ equals the completed Riemann zeta at $1-s$.
background
The ZetaFromTheta module forms Phase 4 of the RS-native zeta program. It isolates the precise bridge needed to identify a theta-style Mellin transform with the completed zeta function, without claiming to have formalized the full analytic theta/Mellin continuation. The ThetaCompletedZetaBridge records two properties: the complex-valued continuation of the theta Mellin transform agrees with the completed Riemann zeta, and the Mellin reflection symmetry transports directly to the complex reflection $s$ to $1-s$. The module recovers the functional equation under the recovered-complex substrate while still relying on Mathlib's completedRiemannZeta_one_sub as the unconditional source.
proof idea
The proof is a one-line term-mode rewriting that applies the bridge's completed_matches_zeta at $s$, inserts the completed_reflection_from_mellin, and applies completed_matches_zeta again at $1-s$.
why it matters
This result supplies the recovered-complex functional equation used by logic_completed_zeta_functional_equation_from_theta and by the Phase 4 certification zetaFromThetaPhase4Cert. It fills the Phase 4 requirement that theta Mellin data identified with completed zeta yields the functional equation. In the Recognition Science framework it links the theta program to the analytic continuation properties of zeta, paralleling the reflection symmetries that appear in the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.