Jcost_exp
Jcost applied to exp t equals the average of exp t and exp -t minus one. Analysts deriving logarithmic derivatives or Jensen bounds in the cost model cite this identity when normalizing curvatures or establishing axis bounds. The proof is a short tactic sequence that rewrites the reciprocal via exp negation then unfolds the Jcost definition.
claimFor every real $t$, $Jcost(e^{t}) = (e^{t} + e^{-t})/2 - 1$, where $Jcost(x) := (x + x^{-1})/2 - 1$.
background
Jcost is defined in the Cost module by the expression Jcost(x) = (x + 1/x)/2 - 1. The lemma supplies its explicit form on the image of the exponential map, converting multiplicative arguments into additive coordinates for the Recognition Composition Law. It is drawn from the JcostCore submodule and supplies the base case for second-derivative normalization at the origin in the Law of Existence module.
proof idea
An auxiliary fact equates the reciprocal of exp t to exp(-t) by symmetry and the negation rule for the exponential. The main step then applies the definition of Jcost via the simp tactic on both the target and the auxiliary equality.
why it matters in Recognition Science
The identity is used by the JensenSketch class to bound averaging functions from above and below, and by the theorem that rewrites Jcost(exp t) as cosh t minus one. It also enables the normalized second-derivative result in the Law of Existence module, where the curvature of J composed with exp is fixed at one at the origin. This anchors the shift to hyperbolic coordinates that align with the phi-ladder and eight-tick octave in the forcing chain.
scope and limits
- Does not prove uniqueness of Jcost under the Recognition Composition Law.
- Does not evaluate Jcost at phi-ladder rungs or compute mass formulas.
- Does not derive spatial dimension D=3 or the alpha inverse band.
formal statement (Lean)
36@[simp] lemma Jcost_exp (t : ℝ) :
37 Jcost (Real.exp t) = ((Real.exp t) + (Real.exp (-t))) / 2 - 1 := by
proof body
Tactic-mode proof.
38 have h : (Real.exp t)⁻¹ = Real.exp (-t) := by
39 symm; simp [Real.exp_neg t]
40 simp [Jcost, h]
41