Jcost_log_even
plain-language theorem explainer
The theorem establishes that the Recognition cost function satisfies J(exp t) = J(exp (-t)) for every real t. Researchers deriving the Mellin reflection property for the cost spectrum cite this log-coordinate evenness as the direct translation of reciprocal symmetry. The proof is a short tactic sequence that applies the base symmetry lemma Jcost_symm to the positive exponential and rewrites the multiplicative inverse via exp(-t).
Claim. For every real number $t$, $J(e^{t}) = J(e^{-t})$, where $J$ denotes the Recognition Science cost function on the positive reals.
background
The module develops the abstract Mellin pullback of reciprocal symmetry for the Recognition Cost Spectrum. The predicate ReciprocalSymmetric f asserts that f(x) = f(1/x) for all x > 0. The cost function Jcost satisfies this by the upstream lemma Jcost_symm, which states that Jcost x = Jcost x^{-1} whenever x > 0. The shifted cost H(t) = J(e^t) + 1 is therefore even, providing the log-variable form of the symmetry needed for the Mellin transform to inherit reflection symmetry s ↔ 1-s.
proof idea
The proof begins by establishing positivity of exp t. It then rewrites using the lemma Jcost_symm, which equates Jcost x to Jcost of its inverse for positive x. A separate calculation shows that the inverse of exp t is exp (-t), completing the equality by substitution.
why it matters
This result supplies the log-evenness clause inside the mellin_pullback_certificate theorem, which assembles the structural facts required for the abstract Mellin pullback. It directly supports the module's claim that reciprocal symmetry of J pulls back to reflection symmetry under the Mellin transform, a step toward identifying the completed zeta function with the Mellin transform of the cost theta function. The declaration sits in the chain from T5 J-uniqueness through reciprocal symmetry, though the full zeta identification remains outside this module's scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.