mellinPhase3Cert
plain-language theorem explainer
This definition assembles the Phase 3 Mellin certificate by direct record instantiation, supplying reciprocal symmetry of the J-cost, the explicit kernel inversion under x to x^{-1}, and the induced reflection property for admissible kernels. Researchers advancing the RS-native zeta program cite it as the formal bridge separating algebraic reciprocity from the analytic transform interface. The construction is a one-line record builder that wires three upstream theorems into the MellinPhase3Cert structure.
Claim. The Phase 3 Mellin certificate is the structure whose fields are the reciprocal symmetry $J(x)=J(x^{-1})$ for the cost function, the kernel inversion law $K(s,x^{-1})=x^{R(s)}$ for all $s,x>0$ where $R$ denotes the reflection map, and the reflection property that any admissible kernel package satisfies $M(s)=M(R(s))$.
background
The module implements Phase 3 of the RS-native zeta program by furnishing a Mellin-transform interface whose reflection theorem follows from reciprocal symmetry. It isolates the algebraic/RS content (reciprocal symmetry of the input and kernel substitution) from the analytic content (existence of the integral transform and validity of the change of variables). The result supplies the transform-level bridge that Phase 4 will instantiate with a theta kernel.
proof idea
The definition is a direct record constructor. It assigns the J_reciprocal field from Jcost_mellin_reciprocal, the kernel_inversion field from mellinKernel_inversion, and the reflection_from_admissibility field from mellin_reciprocal_reflection applied to an admissible package.
why it matters
This certificate supplies the transform-level bridge in the RS-native zeta program, as stated in the module documentation. It prepares instantiation with a theta kernel in Phase 4 to reach the functional equation. The construction rests on reciprocal symmetry of the J-cost, which encodes the double-entry property from the foundational algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.