Jcost_exp
plain-language theorem explainer
The lemma establishes the explicit evaluation of the J-cost function at exponential arguments. Researchers deriving bounds in the JensenSketch or normalizing derivatives in the LawOfExistence module cite this result. The tactic proof rewrites the reciprocal using the exponential negation property and then simplifies using the Jcost definition.
Claim. For the function $J(x) = \frac{x + x^{-1}}{2} - 1$, one has $J(e^{t}) = \frac{e^{t} + e^{-t}}{2} - 1$ for all real $t$.
background
The Jcost definition is Jcost(x) := (x + x^{-1})/2 - 1. This provides the value on the positive reals via the exponential map. The upstream lemma in JcostCore supplies the same identity, which is redeclared here with the simp attribute for use within the Cost module.
proof idea
A hypothesis is introduced to equate the reciprocal of exp t with exp(-t) via symmetry and simp on Real.exp_neg. The main step then applies simp with Jcost and this hypothesis.
why it matters
This result feeds the JensenSketch class, which requires axis_upper and axis_lower bounds using Jcost(exp t), and the Jcost_log_second_deriv_normalized lemma that sets the second derivative at zero to 1. It also enables the jcost_exp_eq_cosh theorem equating it to cosh t - 1. Within Recognition Science, the identity realizes the J-uniqueness (T5) by matching the form cosh(log x) - 1 and supports the composition law derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.