theta_mellin_reflection
plain-language theorem explainer
Recognition Theta Mellin transforms satisfy reflection symmetry under the Mellin reflection map when packaged as ThetaMellinAdmissible. Researchers formalizing the RS-native zeta functional equation cite this result to transport the symmetry from the theta kernel to the completed zeta. The proof is a one-line term application of the reciprocal reflection property for Mellin-admissible kernels.
Claim. Let $M$ be the Mellin transform of an admissible package for the Recognition theta kernel. Then $M(s) = M(r(s))$ for every real $s$, where $r$ denotes the Mellin reflection map.
background
The ZetaFromTheta module forms Phase 4 of the RS-native zeta program. It isolates the exact bridge from the Recognition Theta Mellin transform to the completed zeta functional equation without claiming a full analytic proof. The module records that the unconditional functional equation remains Mathlib's completedRiemannZeta_one_sub while naming the theta/Mellin bridge under the recovered-complex substrate.
proof idea
The proof is a one-line term wrapper that applies mellin_reciprocal_reflection to the Mellin package extracted from the ThetaMellinAdmissible hypothesis.
why it matters
This theorem supplies the reflection symmetry needed to identify the theta Mellin transform with the completed zeta function. It feeds the completed_zeta_functional_equation_from_mellin and LogicThetaZetaBridge constructions in the same module. Within the Recognition Science framework it realizes the Phase 4 mathematical bite that connects the Recognition Theta program to the functional equation of the zeta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.