ThetaMellinAdmissible
plain-language theorem explainer
ThetaMellinAdmissible packages a Mellin-admissible kernel for the Recognition Theta function. Researchers formalizing the Recognition Science zeta program cite it when bridging theta transforms to the completed zeta function. The definition is a direct structure that instantiates MellinAdmissibleKernel on thetaKernel.
Claim. A structure consisting of a field $pkg$ of type MellinAdmissibleKernel applied to the Recognition Theta kernel, where the kernel supplies a transform map $M$ satisfying the substitution $M(s) = M(1-s)$ under reciprocal symmetry.
background
The module ZetaFromTheta forms Phase 4 of the RS-native zeta program. It connects the Recognition Theta program to the completed zeta functional equation by isolating the exact theta-style Mellin transform bridge rather than claiming a full analytic formalization. The unconditional functional equation remains Mathlib's completedRiemannZeta_one_sub while this module records the RS-native bridge that would recover it.
proof idea
The declaration is a direct structure definition that packages the MellinAdmissibleKernel instance for thetaKernel. It relies on the upstream definition of thetaKernel as recognitionTheta together with the structure MellinAdmissibleKernel that records the required substitution property.
why it matters
ThetaMellinAdmissible supplies the theta input required by StrongRecognitionThetaMellinFactor and ThetaCompletedZetaBridge. These downstream structures equate the completed Mellin transform with completedRiemannZeta and transport the reflection symmetry. The module documentation states that this bridge would make the functional equation RS-native.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.