completedZetaFunctionalEquationCert
plain-language theorem explainer
This definition supplies an unconditional certificate identifying the completed Riemann zeta function as the Mellin transform that satisfies the functional equation. Number theorists working inside the Recognition Science zeta program would cite it as the base case that holds before any theta bridge is introduced. The construction is a direct structure instantiation that delegates the reflection property to the imported Mathlib theorem.
Claim. Let $Z(s)$ denote the completed Riemann zeta function. Then $Z(s) = Z(1-s)$ for all $s$ in the complex plane, and the map $s |-> Z(s)$ furnishes a certificate whose Mellin component matches the completed zeta pointwise and obeys the reflection law.
background
The ZetaFromTheta module records Phase 4 of the RS-native zeta program. It isolates the exact bridge between a theta-style Mellin transform and the completed zeta functional equation while noting that the current unconditional version still rests on Mathlib. The local setting therefore treats the recovered-complex substrate as the carrier for the equation until a native theta/Mellin derivation is supplied.
proof idea
The definition builds the CompletedZetaFunctionalEquationCert structure by setting the completedMellin field to completedRiemannZeta. The pointwise matching clause is discharged by reflexivity, and the reflection clause is supplied directly by the upstream theorem completed_zeta_functional_equation_mathlib.
why it matters
This declaration supplies the unconditional base case that later theta-bridge constructions can strengthen. It fills the recovered-complex version of the completed zeta functional equation inside the Recognition framework and keeps the door open for replacing the Mathlib source with the native theta/Mellin bridge once that analytic step is formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.