Jcost_exp
plain-language theorem explainer
Jcost_exp establishes that J(exp t) equals (exp t + exp(-t))/2 minus 1 for any real t. Analysts deriving Jensen bounds or log-coordinate derivatives in Recognition Science cite this identity. The proof is a short tactic sequence that introduces the reciprocal identity for the exponential and unfolds the Jcost definition.
Claim. For every real number $t$, $J(e^t) = (e^t + e^{-t})/2 - 1$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The Jcost function is defined by J(x) := (x + x^{-1})/2 - 1 for positive real x. This encodes the core cost appearing in the Recognition Composition Law and the phi-ladder mass formula. The present module isolates basic algebraic properties of this map before downstream applications to averaging bounds and derivatives. The lemma specializes the definition to exponential arguments, recovering the form that matches cosh(t) - 1 and thereby links to the T5 J-uniqueness landmark.
proof idea
The tactic proof first asserts that the multiplicative inverse of exp t equals exp(-t), justified by symmetry and the exp_neg simplification. It then applies simp using the Jcost definition together with this auxiliary equality.
why it matters
The identity is invoked inside JensenSketch to establish axis bounds, inside the normalized second-derivative lemma for the law of existence, and inside the direct proof that J(exp t) equals cosh t minus 1. It anchors the explicit hyperbolic form required by T5 and supplies the starting point for log-second-derivative calculations that normalize to 1 at the origin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.