mellinIntegrand_reflect_pointwise
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove convergence of the Mellin integral.
- Does not derive the full functional equation for any zeta function.
- Does not perform analytic continuation.
- Does not instantiate the kernel with a theta function or connect to specific RS constants.
formal statement (Lean)
79theorem mellinIntegrand_reflect_pointwise
80 {f : ℝ → ℝ} (hf : ReciprocalSymmetric f)
81 (s x : ℝ) (hx : 0 < x) :
82 mellinIntegrand f s x =
83 f x⁻¹ * mellinKernel s x := by
proof body
Term-mode proof.
84 unfold mellinIntegrand
85 exact mellin_pullback_pointwise hf s x hx
86
87/-- Kernel form of the reflection after inversion. -/