JCostMellinBridge
plain-language theorem explainer
JCostMellinBridge packages the Mellin admissibility conditions for the recognition cost J, supplying the exact analytic assumptions that convert J's reciprocal symmetry into an s to 1-s symmetry for the transform M. Researchers on the RS-native zeta program cite this structure as the interface separating algebraic symmetry from analytic substitution. It is realized as a one-line structure definition that instantiates MellinAdmissibleKernel on Cost.Jcost.
Claim. Let $J$ be the recognition cost function. The structure $JCostMellinBridge$ consists of a single field $pkg$ of type $MellinAdmissibleKernel(J)$, where the package records a map $M$ such that $M(s) = M(1-s)$ whenever the reciprocal symmetry of $J$ holds.
background
In the MellinTransform module, Phase 3 of the RS-native zeta program, the MellinAdmissibleKernel structure records the analytic assumptions an integral Mellin transform must satisfy without defining the integral itself. It requires a function $f$ that is reciprocally symmetric together with a map $M$ obeying the substitution rule $M(s) = M(mellinReflect s)$ for all real $s$ (where mellinReflect sends $s$ to $1-s$ under the $x$ to $x^{-1}$ change of variables). The upstream Cost abbreviation from RSNative.Core denotes the RS-native quantity whose J-cost component is the recognition cost derived from J-uniqueness. The module deliberately isolates the algebraic/RS reciprocal symmetry from the analytic validity of the substitution, producing a transform-level bridge rather than the full theta or zeta functional equation.
proof idea
The declaration is a structure definition with an empty proof body. It constructs the package by direct application of MellinAdmissibleKernel to Cost.Jcost, inheriting the reciprocal and substitution fields already present in the kernel definition.
why it matters
JCostMellinBridge supplies the typed input to the downstream theorem Jcost_mellin_reflection, which immediately yields the reflection property for the J-cost Mellin transform. It occupies the precise slot in Phase 3 that prepares the algebraic reciprocal symmetry of J (from T5 J-uniqueness and the Recognition Composition Law) for the analytic Mellin reflection needed before Phase 4 instantiates a theta kernel. The structure therefore closes the gap between the forcing-chain landmarks and the complex-analytic substrate without yet addressing convergence or the full zeta equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.