mellinKernel
plain-language theorem explainer
The Mellin kernel supplies the real power-law factor x raised to (s minus 1) as the base object for Phase 3 of the RS-native zeta program. Researchers constructing reciprocal-symmetric Mellin interfaces cite this definition when forming integrands and substitution laws. It deliberately isolates algebraic kernel behavior from analytic integral questions. The body is a direct exponentiation with no auxiliary computation or lemmas.
Claim. The Mellin kernel is the real-valued function defined by $K(s,x) := x^{s-1}$ for parameters $s,x$ in the reals.
background
This 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, deliberately separating algebraic/RS content (reciprocal symmetry and kernel substitution) from analytic content (existence of the integral transform and validity of the $x mapsto x^{-1}$ change of variables). 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 declaration is a direct definition that sets the kernel to the real power $x^{(s-1)}$. No lemmas or tactics are invoked; it serves as the primitive building block referenced by the integrand and inversion statements in the same module.
why it matters
This definition is the foundation for mellinIntegrand and the inversion theorems mellinKernel_inversion and mellinIntegrand_reflect_pointwise. It is referenced inside the MellinPhase3Cert structure, which records that reciprocal symmetry plus a valid Mellin substitution law forces $s mapsto 1-s$ reflection at the transform level. In the Recognition framework it supplies the real kernel for the Phase 3 bridge toward the completed zeta functional equation, prior to complex-parameter recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.