mellinIntegrand_after_inversion
plain-language theorem explainer
The theorem shows that reciprocal symmetry of f implies the Mellin integrand after argument inversion obeys f(1/x) times the kernel at 1/x equals f(x) times x to the reflected parameter. Researchers building the RS-native zeta transform would cite it as the post-inversion kernel identity in Phase 3. The term-mode proof reduces the claim by substituting the symmetry equality then invoking a substitution lemma for the kernel reflection.
Claim. Let $f : (0,∞) → ℝ$ satisfy reciprocal symmetry, i.e., $f(x^{-1}) = f(x)$ for all $x > 0$. For real $s$ and $x > 0$, $f(x^{-1}) · K(s, x^{-1}) = f(x) · x^{R(s)}$, where $K$ is the Mellin kernel function and $R$ is the reflection map on the Mellin parameter.
background
The module MellinTransform.lean forms Phase 3 of the RS-native zeta program. It supplies a formal Mellin-transform interface whose reflection theorem is derived from reciprocal symmetry, deliberately separating the algebraic/RS content (reciprocal symmetry and kernel substitution) from analytic questions of integral existence and change-of-variable validity. The result is not yet the theta/zeta functional equation but the transform-level bridge that Phase 4 will instantiate with a theta kernel.
proof idea
The term proof first obtains f(x^{-1}) = f(x) directly from the reciprocal-symmetry hypothesis. It rewrites the left-hand side, unfolds the definitions of mellinKernel and mellinReflect, and finishes by applying the congruence that follows from the substitution identity mellin_reflection_via_substitution.
why it matters
This supplies the kernel form of the reflection after inversion and advances the RS-native zeta program by furnishing the algebraic bridge required for later reflection theorems. It sits inside the module that separates reciprocal-symmetry properties from analytic Mellin content, connecting to the broader Recognition framework through the same symmetry structures that appear in the Recognition Composition Law and the self-similar fixed-point constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.