jcost_exp_eq
plain-language theorem explainer
J(e^ε) equals (e^ε + e^{-ε})/2 - 1 for real ε. Researchers deriving log-domain properties of the reciprocal cost in Recognition Science foundations cite this identity when moving between multiplicative and additive forms. The proof is a direct simplification that unfolds the Jcost definition and applies the exponential negation rule.
Claim. For every real number ε, $J(e^ε) = (e^ε + e^{-ε})/2 - 1$.
background
The module develops the log-domain geometry of the canonical reciprocal cost J(x) = ½(x + x^{-1}) - 1. This identity supplies the explicit half-sum form that converts the multiplicative argument into an additive deviation ε. The surrounding results in the module establish that the geometric mean minimizes total bond cost and that simultaneous descent differs from sequential descent.
proof idea
The proof is a one-line wrapper that applies simplification using the definition of Jcost together with the negation property of the real exponential.
why it matters
This supplies F1.1.7 in the foundation paper on log-domain J-cost geometry. It supplies the cosh form required for the J-uniqueness step in the forcing chain and for constructions on the phi-ladder. The identity is used downstream in proofs of geometric-mean optimality and in the comparison of simultaneous versus sequential descent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.