J_exp_eq_cosh
plain-language theorem explainer
The identity equates the cost functional applied to an exponential argument with the shifted hyperbolic cosine. Researchers deriving the recognition wavelength from ledger curvature cite this conversion between multiplicative ratios and additive costs. The tactic proof unfolds the cost definition, substitutes the exponential inverse via simplification, and rewrites with the standard cosh identity.
Claim. For every real number $t$, $J(e^t) = cosh(t) - 1$, where the cost functional satisfies $J(x) = (x + x^{-1})/2 - 1$.
background
The module derives the recognition wavelength from equating bit cost to curvature cost in RS-native units. The cost functional is defined by $J(x) = (x + x^{-1})/2 - 1$ and satisfies the Recognition Composition Law. Upstream results establish that recognition event costs equal this J-cost and that multiplicative recognizers induce derived costs on positive ratios. The module doc states: 'From the unique cost functional J(x) = ½(x + x⁻¹) - 1, evaluated at the self-similar scale φ, we get J_bit = J(φ) = cosh(ln φ) - 1.'
proof idea
Unfold the definition of J to expose the average of the argument and its inverse. A simp tactic yields (exp t)^{-1} = exp(-t). The final rewrite invokes the equality that defines cosh t as (exp t + exp(-t))/2.
why it matters
The downstream theorem J_bit_eq_cosh applies this result to obtain the bit cost as cosh(log phi) - 1. It closes the first step in the Conjecture C8 chain that equates bit cost to curvature cost and recovers the Planck ratio after face averaging. The identity instantiates J-uniqueness at the exponential scale within the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.