mellin_reflection_involutive
plain-language theorem explainer
The theorem establishes that the Mellin reflection operator is involutive: applying it twice to the transform value returns the original for any admissible kernel. Researchers formalizing the Recognition Science zeta program would cite it as the algebraic foundation for the s to 1-s symmetry derived from reciprocal J-cost. The proof is a direct unfolding of the reflection definition followed by ring normalization.
Claim. Let $M$ be the transform recorded by an admissible Mellin kernel package for a real function $f$. Then $M(r(r(s))) = M(s)$ for every real $s$, where $r$ denotes the reflection map that implements the $s$ to $1-s$ substitution.
background
MellinAdmissibleKernel packages the exact analytic assumptions required for a Mellin transform $M$ of $f$: it records a reciprocal symmetry condition on $f$ together with a substitution property that validates the $x$ to $x^{-1}$ change of variables and maps the value at $s$ to the value at the reflected point. The module implements Phase 3 of the RS-native zeta program, deliberately separating algebraic reciprocal symmetry (inherited from J-cost) from analytic integral existence. Upstream, the reciprocal automorphism in CostAlgebra supplies the J-automorphism via positive inversion, while LedgerForcing and ObserverForcing supply the corresponding cost and recognition-event reciprocals that feed the kernel admissibility.
proof idea
One-line wrapper that unfolds the definition of mellinReflect and applies ring normalization to obtain the algebraic identity reflect(reflect(s)) = s.
why it matters
The result supplies the involutivity of the reflection operator and therefore the two-sided symmetry required for the transform-level bridge that Phase 4 will instantiate with a theta kernel. It sits inside the Recognition Science program that derives all physics from the single functional equation, using the reciprocal symmetry of J (T5) to force the s to 1-s map. No downstream uses are recorded yet; the declaration closes the algebraic half of the Mellin interface before analytic content is added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.