mellinIntegrand_reflect_pointwise
plain-language theorem explainer
For a reciprocal-symmetric real function f, the Mellin integrand at s and positive x equals f at the reciprocal of x times the Mellin kernel at s and x. Workers on the Recognition Science zeta program in Phase 3 would cite this as the pointwise reflection identity that separates algebraic symmetry from analytic integral questions. The proof is a one-line term wrapper that unfolds the integrand definition and invokes the upstream pullback lemma for reciprocal symmetry.
Claim. Let $f:ℝ→ℝ$ satisfy reciprocal symmetry, i.e., $f(x)=f(x^{-1})$ for $x>0$. Then for real $s$ and $x>0$, the Mellin integrand of $f$ at $s,x$ equals $f(x^{-1})$ times the Mellin kernel at $s,x$.
background
This theorem lives in the MellinTransform module, Phase 3 of the RS-native zeta program. The module deliberately isolates algebraic/RS content (reciprocal symmetry and kernel substitution) from analytic content (existence of the integral transform and validity of the $x↦x^{-1}$ substitution). The result is positioned as the transform-level bridge that Phase 4 will later instantiate with a theta kernel. ReciprocalSymmetric f encodes invariance under inversion. The Mellin integrand is the product appearing inside the Mellin integral; the Mellin kernel is the standard factor in that transform. The key upstream lemma is mellin_pullback_pointwise, which supplies the pointwise identity under the symmetry hypothesis.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of mellinIntegrand and then applies the lemma mellin_pullback_pointwise (from MellinPullback) to the given reciprocal-symmetry hypothesis, the parameters s and x, and the positivity assumption on x.
why it matters
The declaration supplies the algebraic reflection step required for the RS-native Mellin interface in Phase 3 of the zeta program. It derives the kernel-substituted form directly from reciprocal symmetry, keeping the analytic questions (convergence, continuation) separate for later work. The module doc states that this is the bridge before Phase 4 instantiates a theta kernel; it therefore sits upstream of any eventual functional equation for the zeta function built inside Recognition Science. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.