jcost_log_eq_clog_one
plain-language theorem explainer
In log coordinates the recognition cost of a positive ratio equals cosh(t) − 1, so it is the unit-curvature member of the δ-forced family. Anyone citing J-calibration or the PRC-to-RS chain bridge needs this identity. The proof is a short simplification: unfold J at exp(t) and match the definition of cosh.
Claim. For every real $t$, the recognition cost satisfies $J(e^{t}) = \cosh(t) - 1$. Equivalently $J(e^{t}) = \cosh(1 \cdot t) - 1$, so in log coordinates $J$ is the $c = 1$ member of the $\delta$-forced cost family.
background
The recognition cost on positive reals is $J(x) = (x + x^{-1})/2 - 1$. Substituting the log chart $x = e^{t}$ yields the classical identity $J(e^{t}) = \cosh(t) - 1$. That is exactly the $c = 1$ slice of the one-parameter family $\cosh(c t) - 1$ forced by the δ-axioms.
The surrounding module bridges Primitive Recognition Calculus to the RS forcing chain. Upstream, Calibration (Axiom 3) demands that the second derivative of $F(\exp t)$ at the origin equal 1, which normalizes curvature at unity and selects a unique gauge rather than a family. The present identity is the explicit log-coordinate form of that gauge-fixed $J$.
proof idea
Term-mode proof by simplification only. Unfold $J(x) = (x + x^{-1})/2 - 1$ at $x = e^{t}$, drop the trivial factor $1 \cdot t$ via one_mul, and rewrite $(e^{t} + e^{-t})/2$ with the Mathlib identities Real.cosh_eq and Real.exp_neg. No external RS lemmas are required beyond the definition of $J$.
why it matters
Direct input to the sibling theorem that the log-curvature of $J$ at the unit is exactly 1. That parent result places $J$ as the gauge-fixed member singled out by Calibration, not merely some member of the δ-forced family. In the forcing chain this is the T5 landmark: $J(x) = (x + x^{-1})/2 - 1 = \cosh(\log x) - 1$. The bridge uses the identity to show the RS chain's cost entry is the calibrated δ-cost, linking PRC into the full RS development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.