thetaKernel
plain-language theorem explainer
This definition supplies the Recognition Theta function as the kernel for Mellin transforms in the RS-native zeta construction. Researchers assembling the phase-4 theta-Mellin bridge cite it when building admissible kernel packages. The implementation is a direct one-line alias to the upstream Recognition Theta declaration.
Claim. Let $K : ℝ → ℝ$ be the theta-style kernel for the Mellin transform. Then $K$ is defined to be the Recognition Theta function.
background
The ZetaFromTheta module forms phase 4 of the RS-native zeta program. It connects the Recognition Theta program to the completed zeta functional equation by isolating a theta-style Mellin transform compatible with the completed zeta function. The unconditional functional equation remains Mathlib's completedRiemannZeta_one_sub; the module records that result under the recovered-complex substrate and names the theta/Mellin bridge that would render it RS-native.
proof idea
The definition is a one-line wrapper that applies the Recognition Theta function from the imported RecognitionTheta module.
why it matters
This definition supplies the kernel required by ThetaMellinAdmissible and ZetaFromThetaPhase4Cert. The latter records that a supplied theta/zeta Mellin bridge yields the functional equation for recovered-complex completed zeta. It fills the exact bridge step in phase 4 of the RS-native zeta program while leaving the full analytic theta/Mellin proof for later work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.