G_costLambda
plain-language theorem explainer
In log coordinates, each one-parameter cost F_λ(x)=(x^λ+x^{-λ})/2−1 becomes cosh(λ t)−1. Classification of Recognition Composition Law solutions via the cosh-add identity cites this reparametrization constantly. The proof is a short term calculation: unfold the log map and real powers, then match the exponential form of cosh.
Claim. For every real $\lambda$, if $F_\lambda(x)=\frac{x^\lambda+x^{-\lambda}}{2}-1$, then the log-coordinate reparametrization $G(F_\lambda)(t):=F_\lambda(e^t)$ equals $\cosh(\lambda t)-1$ for all real $t$.
background
The cost functional equation is studied in log coordinates. The operator $G$ sends a cost $F:(0,\infty)\to\mathbb{R}$ to $G(F)(t)=F(e^t)$, so multiplicative structure on the positive reals becomes additive structure on $\mathbb{R}$. Calibration is the curvature condition $G''(0)=1$ (equivalently $\lim_{t\to 0}2F(e^t)/t^2=1$).
The one-parameter family at issue is the natural scale deformation of the T5 J-cost: $F_\lambda(x)=(x^\lambda+x^{-\lambda})/2-1$. When $\lambda=1$ this is exactly $J(x)=\cosh(\log x)-1$. The Recognition Composition Law (RCL) is the d'Alembert/cosh-add identity on $G(F)$.
This module develops native uniqueness for that cost inside the Primitive Recognition Calculus, without completeness assumptions. The present identity is the bridge that turns every algebraic statement about $F_\lambda$ into a hyperbolic-function identity on $\mathbb{R}$.
proof idea
Term-mode, pointwise. Apply functional extensionality, then for each $t$ record $e^t>0$. Unfold $G$ and the definition of the $\lambda$-family (real powers). Rewrite $x^\lambda$ and $x^{-\lambda}$ via the positive-base definition of rpow, cancel log(exp t), and invoke the exponential form of cosh together with a one-line ring identity $t\cdot(-\lambda)=-(t\lambda)$. The two sides match.
why it matters
This is the workhorse reparametrization for the whole cost-uniqueness arc. Downstream, calibration_value_costLambda reads off $G(F_\lambda)''(0)=\lambda^2$, so the calibration condition $G''(0)=1$ forces $\lambda=\pm 1$; the positive branch is the native J-cost. The same identity feeds costLambda_isCalibrated_iff and the RCL check costLambda_coshAddIdentity (both sides reduce to $2\cosh(ct)\cosh(cu)-2$).
At framework scale it sits under T5 J-uniqueness and the RCL: once monotonicity plus reciprocity plus normalization put a cost inside the $F_\lambda$ family (composition_law_monotone_forces_costLambda), this lemma converts the residual scale parameter into ordinary hyperbolic calculus, after which calibration kills the free parameter. No completeness is used; the argument is purely real-analytic on the log line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.