Jcost_mellin_reciprocal
plain-language theorem explainer
The theorem establishes that the Recognition Science J-cost function satisfies reciprocal symmetry. Researchers assembling the Mellin-transform interface for the RS-native zeta program would cite this result as the algebraic input to the phase-3 certificate. The proof is a direct one-line application of the reciprocal-symmetry theorem already established for the J-cost in the pullback module.
Claim. Let $J$ denote the Recognition Science cost function. Then $J$ is reciprocally symmetric: $J(x) = J(x^{-1})$ for every $x > 0$.
background
The module implements Phase 3 of the RS-native zeta program. It deliberately separates the algebraic/RS content (reciprocal symmetry and kernel substitution) from the analytic content (existence of the integral transform and validity of the $xmapsto x^{-1}$ change of variables). The result is not yet the theta/zeta functional equation; it is the transform-level bridge that Phase 4 will instantiate with a theta kernel.
proof idea
The proof is a one-line wrapper that applies the theorem Jcost_reciprocal_symmetric from the MellinPullback module, which itself reduces to the evenness of the shifted cost $H(t) = J(e^t) + 1$ in logarithmic coordinates.
why it matters
This supplies the reciprocal-symmetry component of the MellinPhase3Cert certificate. It thereby provides the algebraic half of the reflection theorem for the Mellin transform. The construction aligns with the J-uniqueness property in the forcing chain, since the explicit form of J is invariant under inversion. It feeds directly into the phase-3 certificate that bundles reciprocal symmetry with kernel inversion and reflection from admissibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.