Jcost_exp_eq_cosh_sub_one
plain-language theorem explainer
The recognition cost of an exponential state equals hyperbolic cosine minus one: J(e^t) = cosh(t) − 1. Continuum-layer measure-forcing arguments and sub-Gaussian tail bounds cite this change of coordinates. The proof is a short algebraic rewrite from the definition of J and the exponential form of cosh.
Claim. For every real $t$, the recognition cost satisfies $J(e^{t}) = \cosh t - 1$, where $J(x) = \frac{x + x^{-1}}{2} - 1$ for $x > 0$.
background
The J-cost is the unique recognition cost forced by the Recognition Composition Law: $J(x) = \frac{x + x^{-1}}{2} - 1$ on positive reals (T5). Equivalently $J(x) = \cosh(\log x) - 1$. It vanishes only at $x = 1$ and is nonnegative elsewhere.
This module (T9) forces the weighting on recognition states after T0–T8 have fixed the shape of the law. The continuum layer treats weight as a function of a real additive cost; the natural coordinate is the log-deviation $t$ with state $e^{t}$. The identity here converts J from the multiplicative ratio coordinate into that additive log coordinate.
Upstream definitions of Jcost across Cost, Gravity, Cosmology, and Spiral modules all share the same algebraic body $(x + x^{-1})/2 - 1$.
proof idea
Term-mode, three steps. Unfold Cost.Jcost to expose $(e^{t} + (e^{t})^{-1})/2 - 1$. Rewrite the inverse as $e^{-t}$ via Real.exp_neg. Apply Real.cosh_eq, which states $\cosh t = (e^{t} + e^{-t})/2$, and cancel. No lemmas beyond the standard real-analysis identities are required.
why it matters
Parent consumer is sub_gaussian_in_J: the forced measure at rate $\lambda \ge 0$ in the J-coordinate is dominated by a Gaussian of variance $1/\lambda$ in log-deviation, $\exp(-\lambda \cdot J(e^{t})) \le \exp(-\lambda t^{2}/2)$. That bound opens by rewriting via this identity, then using $\frac{t^{2}}{2} \le \cosh t - 1$.
In the framework primer this is exactly the T5 form $J(x) = \cosh(\log x) - 1$, specialized to the exponential chart used by continuum measure forcing. Without the coordinate change, the Gibbs weight $\propto \exp(-\lambda J)$ cannot be compared to ordinary Gaussian tails on $\mathbb{R}$. It is scaffolding for the continuum half of T9 (factorization, antitonicity, and the self-similar rate pinned by $\varphi$), not a new forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.