costLambda_eq_cosh
plain-language theorem explainer
On positive reals, the multiplicative gauge member equals the log-coordinate form cosh(c log x) − 1. Anyone transporting PRC cost laws between multiplicative and additive coordinates cites this identity. The proof rewrites real powers via the exponential definition and applies the standard cosh formula.
Claim. For every real $c$ and every $x > 0$, $\tfrac12\bigl(x^{c} + x^{-c}\bigr) - 1 = \cosh(c\,\log x) - 1$.
background
In the Primitive Recognition Calculus, the one-parameter cost family is written multiplicatively as $\mathrm{costLambda},c,x = \tfrac12(x^c + x^{-c}) - 1$, with real powers via Real.rpow. The member $c = 1$ is the Recognition cost $J(x) = \tfrac12(x + x^{-1}) - 1$ (equivalently $\cosh(\log x) - 1$), forced unique by the T5 step of the forcing chain and the Recognition Composition Law.
The calibration-target side of the development works in log coordinates, where the same family appears as $\cosh(c,t) - 1$. This lemma is the bridge: on $(0,\infty)$ the two presentations agree. The surrounding module shows that every positive curvature parameter $c$ yields a cost obeying the unit law, reciprocal symmetry, continuity, and the RCL, so the cost axioms alone do not pin the calibration scale.
proof idea
Two local identities rewrite the real powers: $x^c = \exp(c\log x)$ and $x^{-c} = \exp(-(c\log x))$, each from Real.rpow_def_of_pos (with a short ring cleanup on the second). Unfold the multiplicative definition, substitute both identities, and finish by Real.cosh_eq, which is exactly $\cosh u = (e^u + e^{-u})/2$ at $u = c\log x$.
why it matters
This is the workhorse identity of PRCCalibrationIndependence. Downstream it discharges the unit law (costLambda_unit0), reciprocal symmetry (costLambda_symm), continuity on $(0,\infty)$ (costLambda_continuousOn), the $c=1$ match to Cost.Jcost (costLambda_one_eq_Jcost), injectivity of the family in the curvature parameter (costLambda_inj), and the log-coordinate readout $G(\mathrm{costLambda},c),t = \cosh(c,t)-1$ (G_costLambda).
That last form is what feeds the upstream functional-equation classification: every gauge member satisfies the cosh-add / d'Alembert identity (the RCL). In framework terms it keeps the T5 $J$-uniqueness story honest: $J$ is the $c=1$ slice of a whole cosh family, and calibration of $c$ is an irreducible scale choice not forced by the cost laws alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.