mellin_reciprocal_reflection
plain-language theorem explainer
The theorem states that any Mellin transform package satisfying the admissibility conditions for a reciprocally symmetric kernel obeys M(s) = M(1-s) for all real s. Researchers building the RS-native zeta program cite this result as the algebraic bridge from reciprocal symmetry to reflection invariance. The proof is a direct one-line application of the substitution field recorded inside the MellinAdmissibleKernel structure.
Claim. Let $f : ℝ → ℝ$ admit a Mellin transform package $M$ that records the reciprocal symmetry of $f$ together with the validity of the substitution $x ↦ x^{-1}$. Then $M(s) = M(1-s)$ holds for every real number $s$.
background
MellinAdmissibleKernel is a structure that packages an analytic Mellin transform $M$ for a function $f$, together with the assumption that $f$ is reciprocally symmetric and that the substitution $x ↦ x^{-1}$ is valid, yielding the reflection $M(s) = M(1-s)$. The module separates the algebraic/RS content (reciprocal symmetry and kernel substitution) from the analytic content (existence of the integral transform). mellinReflect is the definition that sends $s$ to $1-s$. Upstream results supply the ContinuumBridge identification of Laplacian action and the RecognitionStructure $M$ used in Cycle3.
proof idea
The proof is a one-line wrapper that applies the substitution field of the MellinAdmissibleKernel structure.
why it matters
This declaration supplies the reflection symmetry that Jcost_mellin_reflection, mellinPhase3Cert, recoveredComplexMellinBridge_of_admissible, and theta_mellin_reflection all invoke. It fills the transform-level bridge in Phase 3 of the RS-native zeta program; Phase 4 will instantiate the same symmetry with a theta kernel. The result sits between the algebraic reciprocal symmetry of the J-cost and the completed functional equation for zeta.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.