mellin_pullback_certificate
plain-language theorem explainer
The theorem certifies that the Recognition cost function J satisfies reciprocal symmetry J(x) = J(1/x) for x > 0, evenness J(e^t) = J(e^{-t}) in logarithmic coordinates, the Mellin kernel transformation (x^{-1})^{s-1} = x^{1-s}, and the induced integrand symmetry for any reciprocally symmetric f. Researchers deriving the zeta functional equation from cost symmetries in Recognition Science would cite this certificate as the abstract structural foundation. The proof is a term-mode assembly of four supporting lemmas that separately establish each
Claim. Let J be the Recognition cost function. Then J is reciprocally symmetric: J(x) = J(x^{-1}) for all x > 0; J(e^t) = J(e^{-t}) for all real t; the substitution x to x^{-1} maps the Mellin kernel by (x^{-1})^{s-1} = x^{1-s} for x > 0; and for any reciprocally symmetric f the Mellin integrand satisfies f(x) x^{s-1} = f(x^{-1}) x^{s-1} for x > 0.
background
The module formalizes the abstract Mellin pullback of reciprocal symmetry for the Recognition cost function. A function f : R to R is reciprocally symmetric when f(x) = f(1/x) for every positive x, per the predicate ReciprocalSymmetric. The central claim is that the zeta functional equation xi(s) = xi(1-s) arises as the Mellin pullback of J(x) = J(1/x).
proof idea
The proof is a term-mode construction that directly assembles the four-tuple of lemmas Jcost_reciprocal_symmetric, Jcost_log_even, mellin_reflection_via_substitution, and mellin_pullback_pointwise. Each lemma verifies one clause of the certificate; the wrapper simply packages them without further reduction.
why it matters
This declaration supplies the structural certificate required for the Mellin pullback argument in the Recognition Science program. It directly supports the module goal of showing how reciprocal symmetry of J induces reflection symmetry in the Mellin transform, the abstract precursor to the zeta functional equation. The full identification of the Mellin transform of Theta_J with the completed zeta xi requires complex analysis beyond this module. It touches the open question of completing that identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.