Jcost_exp_cosh
plain-language theorem explainer
The identity equates J-cost at an exponential argument to cosh minus one. Researchers deriving hyperbolic forms for cost functions in Recognition Science cite it to simplify expressions with positive reals. Proof is a one-line wrapper applying the upstream Jlog_as_cosh lemma.
Claim. $J(e^t) = e^t + e^{-t})/2 - 1 = cosh(t) - 1$ for all real $t$, where $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$.
background
Jcost is defined by Jcost(x) := (x + x^{-1})/2 - 1. The Cost module develops this as the native cost measure for Recognition Science, building on ledger structures and phi-forcing. The upstream Jlog_as_cosh lemma proves the matching form for Jlog by unfolding both definitions, invoking cosh_eq, and simplifying with ring and exp_neg.
proof idea
One-line wrapper that applies Jlog_as_cosh t. The upstream result already expands Jlog as Jcost composed with exp and verifies the cosh identity, so the call discharges the goal immediately.
why it matters
This identity is invoked by Jmetric_exp_sinh to obtain the sinh metric, by JcostN_eq_cosh_logsum and JlogN_eq_cosh_sub_one for vector extensions, and by cosh_log_eq_jcost_rpow for power rescalings. It realizes the T5 J-uniqueness step in the forcing chain by exhibiting J(x) = cosh(log x) - 1, and supports cost stability in DAlembert and nonnegativity in simplicial ledgers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.