cosh_minus_one_eq
plain-language theorem explainer
The identity equates twice the deviation of cosh from unity to four times the square of sinh at half argument. Researchers deriving the J-metric from the exponential form of the cost function cite it when converting between representations. The proof applies the double-angle formula for cosh together with the Pythagorean identity for hyperbolic functions and finishes with ring arithmetic.
Claim. For every real number $t$, $2 (cosh t - 1) = 4 sinh^2 (t/2)$.
background
In the Cost module the J-cost function is defined by J(x) = (x + x^{-1})/2 - 1, equivalently cosh(log x) - 1. The present lemma converts the deviation of cosh from 1 into a squared sinh term required for the absolute-value expression of the J-metric. The module imports standard real analysis; the identity is independent of the Recognition Science axioms but is invoked whenever exponential and hyperbolic representations of the cost must be reconciled.
proof idea
The tactic proof first invokes Real.cosh_two_mul on t/2 to obtain cosh t = cosh²(t/2) + sinh²(t/2). It then uses Real.cosh_sq_sub_sinh_sq to replace cosh²(t/2) by 1 + sinh²(t/2). A calc block rewrites the left-hand side through these substitutions and applies ring to reach the right-hand side.
why it matters
Jmetric_exp_sinh applies this lemma after unfolding Jmetric and invoking Jcost_exp_cosh, thereby obtaining Jmetric(exp t) = 2 |sinh(t/2)|. The identity therefore supports the translation between the exponential and hyperbolic pictures of the cost function that appears in the Recognition Composition Law and the phi-ladder mass formulas. It closes a small but necessary algebraic gap in the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.