mellinIntegrand
plain-language theorem explainer
Mellin integrand multiplies a real function f by the kernel x to the power s minus one. Phase 3 workers on the RS-native zeta program cite the definition when assembling the integral transform prior to reflection. It is implemented as the direct product of the function value at x and the kernel evaluated at s and x.
Claim. The Mellin integrand for a real function $f$ at parameters $s$ and $x$ is the product $f(x) · x^{s-1}$.
background
The MellinTransform module implements Phase 3 of the RS-native zeta program. It supplies a formal Mellin-transform interface whose reflection theorem is derived from reciprocal symmetry. The module deliberately separates algebraic and RS content (reciprocal symmetry and kernel substitution) from analytic content (integral existence and the $x ↦ x^{-1}$ substitution).
proof idea
One-line definition that multiplies the input function value f x by the upstream kernel mellinKernel s x.
why it matters
This definition supplies the integrand for the pointwise reflection theorem mellinIntegrand_reflect_pointwise, which identifies the integrand before and after inversion under reciprocal symmetry of f. It therefore forms the transform-level bridge that Phase 4 will instantiate with a theta kernel to reach the functional equation. The construction remains real-valued to isolate the RS reciprocal symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.