IndisputableMonolith.NumberTheory.MellinTransform
This module supplies the real Mellin kernel x^{s-1} and supporting integrands as the Phase 3 real-valued layer for pulling back the J-cost reciprocal symmetry to the zeta functional equation. Researchers in Recognition Science analytic number theory cite it to isolate the explicit real Mellin construction before complex completion. The module organizes kernel definitions, reflection maps, and integrand lemmas that rest on the upstream MellinPullback symmetry and LogicComplexCompat substrate.
claimThe real Mellin kernel is $K(x,s) = x^{s-1}$ for $x > 0$. The associated Mellin transform of a suitable function $f$ is the integral against this kernel, with reflection properties under $s$ to $1-s$ induced by the reciprocal symmetry $J(x) = J(1/x)$ of the Recognition cost function.
background
Recognition Science derives the zeta functional equation from the Mellin pullback of the J-cost reciprocal symmetry J(x) = J(1/x), as set out in the MellinPullback module. This module supplies the concrete real-valued kernel and integrands for that construction in Phase 3. It adopts Mathlib's complex numbers via the LogicComplexCompat layer, which states the Phase 2 decision to use the existing analytic substrate without redefining holomorphy or contour integration.
proof idea
This is a definition module, no proofs. It assembles the real Mellin components by defining the kernel as x^{s-1}, the integrand as the product with a test function, and then states reflection properties that follow from the J-symmetry pullback established in the MellinPullback upstream module.
why it matters in Recognition Science
This module supplies the real Mellin infrastructure that feeds directly into the ZetaFromTheta module, which isolates the bridge to the completed zeta functional equation. It realizes the Phase 3 real layer of the RS-native zeta program, where the kernel enables the pullback of J(x) = J(1/x) to the functional equation ξ(s) = ξ(1-s) before the complex extension in Phase 4.
scope and limits
- Does not prove analytic continuation or the full zeta functional equation.
- Does not implement contour integration or residue calculus.
- Does not handle the completed complex zeta parameter s.
- Does not derive explicit theta-function identities.
- Does not address convergence domains beyond kernel definitions.
used by (1)
depends on (2)
declarations in this module (16)
-
def
mellinKernel -
def
mellinIntegrand -
def
mellinReflect -
structure
MellinAdmissibleKernel -
theorem
Jcost_mellin_reciprocal -
theorem
mellinKernel_inversion -
theorem
mellinIntegrand_reflect_pointwise -
theorem
mellinIntegrand_after_inversion -
theorem
mellin_reciprocal_reflection -
theorem
mellin_reflection_involutive -
structure
JCostMellinBridge -
theorem
Jcost_mellin_reflection -
structure
RecoveredComplexMellinBridge -
def
recoveredComplexMellinBridge_of_admissible -
structure
MellinPhase3Cert -
def
mellinPhase3Cert