Jmetric_exp_sinh
plain-language theorem explainer
The lemma supplies the hyperbolic simplification Jmetric(exp t) = 2 |sinh(t/2)| for the square-root cost metric on positive reals. Workers converting between multiplicative ratios and additive distances in Recognition Science cost models would cite it when evaluating strain on exponential scales. The proof is a direct algebraic reduction that unfolds the sqrt definition, substitutes the cosh form of Jcost, invokes the double-angle identity, and collapses the square root to an absolute value.
Claim. $J_{metric}(e^{t}) = 2 |sinh(t/2)|$ for every real $t$, where $J_{metric}(x) := sqrt(2 J_{cost}(x))$ and $J_{cost}(e^{t}) = cosh(t) - 1$.
background
In the Cost module the J-cost function is the recognition strain J(x) = (x + x^{-1})/2 - 1, equivalently cosh(log x) - 1. Jmetric is introduced as its square-root scaling sqrt(2 Jcost(x)), which recovers the absolute logarithm and therefore behaves metrically under multiplication. The local setting is the derivation of cost functions from the Recognition Composition Law and the J-uniqueness step of the forcing chain.
proof idea
The term proof unfolds Jmetric, rewrites via the lemma Jcost_exp_cosh to obtain cosh(t) - 1, applies cosh_minus_one_eq to reach 4 sinh^2(t/2), then uses ring, sqrt_sq_eq_abs, and abs_mul to reduce sqrt(4 sinh^2(t/2)) to 2 |sinh(t/2)|.
why it matters
The identity gives an explicit closed form for the metric induced by J-cost, supporting the T5 J-uniqueness claim in the forcing chain. It sits alongside the d'Alembert submultiplicative bound Jcost_submult and the explicit note that Jmetric itself fails the triangle inequality. No downstream theorems yet reference it, leaving open its insertion into phi-ladder or observer-forcing constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.