logic_completed_zeta_functional_equation
plain-language theorem explainer
The declaration establishes the functional equation for the completed Riemann zeta function when its argument is drawn from the recovered complex numbers. Analysts extending the Recognition Science framework to number theory would cite this result to verify consistency with the classical continuation. The proof is a direct reduction to Mathlib's completed zeta functional equation after applying the transport from recovered to standard complexes.
Claim. Let $s$ be a recovered complex number. The completed Riemann zeta function on the recovered line satisfies $widehat{zeta}(s) = widehat{zeta}(1-s)$.
background
The module implements Phase 4 of the RS-native zeta program by linking the Recognition Theta construction to the completed zeta functional equation. It does not yet supply a full analytic proof from the theta kernel but records the exact compatibility condition under the recovered-complex substrate. LogicComplex consists of pairs of recovered reals for real and imaginary parts. The function logicCompletedRiemannZeta applies the standard completedRiemannZeta after transport via toComplex. The upstream complex transport functions fromComplex and toComplex, together with the Mathlib theorem completed_zeta_functional_equation_mathlib, supply the necessary infrastructure. This setting is described in the module documentation as isolating the theta/Mellin bridge while retaining the unconditional functional equation from Mathlib.
proof idea
The proof applies the Mathlib functional equation completed_zeta_functional_equation_mathlib to the image of s under toComplex. The simpa tactic then rewrites using the definition of logicCompletedRiemannZeta to obtain the desired equality on the recovered side.
why it matters
The result is referenced by the certificate zetaFromThetaPhase4Cert, which aggregates the theta kernel, the Mathlib equation, this recovered version, and the Mellin bridge implication. It supplies the recovered-complex instance of the functional equation required for Phase 4 of the zeta program in Recognition Science. The module documentation notes that a native derivation from the theta/Mellin transform remains future work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.