jcost_exp_eq_cosh
plain-language theorem explainer
The identity equates the J-cost of an exponential argument to the hyperbolic cosine minus one. Researchers bridging the Riemann xi functional equation to J-cost symmetry via defect coordinates would cite this result when translating between exponential and hyperbolic expressions. The proof is a direct algebraic reduction using the exponential form of Jcost and the definition of cosh.
Claim. For all real $t$, the J-cost functional satisfies $Jcost(e^{t}) = cosh(t) - 1$.
background
The J-cost functional satisfies $Jcost(x) = (x + x^{-1})/2 - 1$ for positive $x$, coinciding with the defect functional. The upstream lemma Jcost_exp establishes $Jcost(Real.exp t) = ((Real.exp t) + (Real.exp (-t)))/2 - 1$. This module connects the completed Riemann xi functional equation $ξ(s) = ξ(1-s)$ to J-cost reciprocal symmetry $J(x) = J(1/x)$ through the defect-coordinate map $x = e^{2(σ - 1/2)}$ with $σ = Re(s)$, sending the critical line to the unique minimum of J at $x=1$.
proof idea
The proof is a one-line wrapper that rewrites the left-hand side via the lemma Jcost_exp and matches the right-hand side using the definition of cosh.
why it matters
This identity supports the parent theorem jcost_xiMap_eq_cosh, which rewrites J-cost on defect coordinates as $cosh(2η) - 1$ with $η = σ - 1/2$. It supplies the algebraic link between the xi functional equation and J-cost symmetry described in the module documentation, aligning with J-uniqueness (T5) and the self-similar fixed point in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.