logic_completed_zeta_functional_equation_from_theta
plain-language theorem explainer
Supplying a recovered-complex theta/zeta bridge makes the completed zeta function on LogicComplex inputs obey the functional equation relating its value at s to the value at 1 minus s. Researchers extending the Recognition Science zeta program would cite this when linking the theta kernel to the Riemann zeta. The argument is a direct reduction to the Mellin-derived equation followed by simplification with the zeta definition.
Claim. Given a theta/zeta Mellin bridge package and a recovered complex number $s$, the completed Riemann zeta function transported to the recovered complex line satisfies the reflection formula $Z(s) = Z(1-s)$.
background
The module develops Phase 4 of the RS-native zeta program by connecting the Recognition Theta kernel to the completed zeta functional equation via a theta-style Mellin transform. It isolates the exact bridge without claiming a full analytic proof. The LogicThetaZetaBridge structure packages an analytic substrate certificate together with a ThetaCompletedZetaBridge. The logicCompletedRiemannZeta function is defined by transporting a recovered complex input to the classical line and applying the standard completed Riemann zeta there. Upstream transport lemmas fromComplex and toComplex move values between the recovered and classical complex lines, while the sibling Mellin-derived equation supplies the core reflection property.
proof idea
The proof applies the completed_zeta_functional_equation_from_mellin lemma to the theta_bridge component of the supplied bridge evaluated at the transported value toComplex s. It then simplifies the resulting equality using the definition of logicCompletedRiemannZeta.
why it matters
This result supplies the recovered-complex version of the zeta functional equation inside the Phase 4 effort of the Recognition Science zeta program. It relies on the theta/Mellin bridge to recover the classical reflection formula without re-proving analytic continuation. The declaration isolates the precise interface that would allow the Recognition Theta kernel to generate the functional equation natively under the recovered-complex substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.