pith. machine review for the scientific record. sign in
theorem proved term proof high

Jcost_mellin_reciprocal

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  67theorem Jcost_mellin_reciprocal : ReciprocalSymmetric Cost.Jcost :=

proof body

Term-mode proof.

  68  Jcost_reciprocal_symmetric
  69
  70/-- The Mellin kernel transforms under inversion exactly as the reflected
  71parameter requires. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.