Jcost_exp
plain-language theorem explainer
Recognition Science defines the J-cost to quantify deviation from self-similarity. The lemma equates Jcost applied to exp t with (exp t + exp(-t))/2 - 1. Analysts of cost structures cite it when shifting to logarithmic coordinates or linking to hyperbolic forms. The proof is a short tactic sequence that records the reciprocal identity for the exponential and substitutes into the Jcost definition.
Claim. For every real number $t$, $Jcost(e^t) = (e^t + e^{-t})/2 - 1$.
background
The Jcost function is defined in the Cost module by Jcost(x) := (x + x^{-1})/2 - 1. This supplies the base defect measure consistent with J-uniqueness from the forcing chain. The lemma sits in the Cost module and depends on the core implementation in JcostCore, which supplies the identical identity for use in averaging constructions and existence laws.
proof idea
The tactic proof first records an auxiliary equality showing that the reciprocal of exp t equals exp(-t) via symmetry and the standard negation rule. It then applies simplification using the Jcost definition together with this auxiliary fact.
why it matters
The result is invoked inside the JensenSketch class to supply the explicit axis values needed for averaging bounds. It directly enables the rewrite to cosh t - 1 in the XiJBridge module, aligning with T5 J-uniqueness. It also supports the normalized second-derivative hook at zero in the Law of Existence module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.