mellin_pullback_pointwise
plain-language theorem explainer
Reciprocal symmetry of f implies that the Mellin integrand f(x) x^{s-1} takes the same value at x and at 1/x. Analysts deriving reflection formulas for Mellin transforms cite this as the base equality before measure adjustments. A single application of the symmetry hypothesis completes the proof.
Claim. If $f : ℝ → ℝ$ satisfies $f(x) = f(1/x)$ for all $x > 0$, then for any real $s$ and $x > 0$, $f(x) x^{s-1} = f(x^{-1}) x^{s-1}$.
background
ReciprocalSymmetric f is the predicate that f(x) equals f(1/x) for every positive real x. This module develops the Mellin pullback of such symmetry, showing how it induces reflection symmetry s ↔ 1-s in the transformed function. The upstream result ReciprocalSymmetric is used directly here, and related kernels from BITKernelFamilies and ILG.Kernel provide context for cost functions in the Recognition framework.
proof idea
The term proof consists of a single rewrite that substitutes the reciprocal symmetry hypothesis hf at the given x.
why it matters
This lemma supports the mellin_pullback_certificate theorem, which collects the structural facts needed to identify the Mellin transform of the Recognition cost function J with the completed zeta function ξ(s). It fills the pointwise step in the abstract Mellin reflection result, connecting to the Recognition Science claim that reciprocal symmetry of J forces the functional equation ξ(s) = ξ(1-s). The full complex-analytic identification remains open beyond this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.