G_costLambda
plain-language theorem explainer
In log coordinates, every member of the multiplicative cost-gauge family evaluates to cosh(c t) − 1. Anyone classifying solutions of the Recognition Composition Law or proving calibration selects c = 1 cites this identity. The proof is a two-step rewrite: unfold the log reparametrization and apply the cosh form of the gauge on exp t.
Claim. For all real $c$ and $t$, if $G$ is the log-coordinate reparametrization $G(F)(t) := F(e^t)$ and $\mathrm{cost}_\lambda(c,x) := \tfrac12(x^c + x^{-c}) - 1$, then $G(\mathrm{cost}_\lambda(c,\cdot))(t) = \cosh(c\, t) - 1$.
background
The Primitive Recognition Calculus works with a one-parameter gauge of reciprocal costs on the positive reals: $\mathrm{cost}_\lambda(c,x) = \tfrac12(x^c + x^{-c}) - 1$, with the $c = 1$ member equal to the canonical $J$-cost. On $(0,\infty)$ this coincides with the additive form $\cosh(c\log x) - 1$ (theorem costLambda_eq_cosh).
Functional-equation work is done after the change of variables $G(F)(t) := F(e^t)$, which converts multiplicative composition into additive d'Alembert/cosh identities. The module imports the Cost functional-equation layer and the calibration-target interface; the local goal is to show that every gauge member is already in the $\cosh(c\cdot)$ family that the classification theorems consume.
Upstream, $G$ is defined simply as evaluation at the exponential, and the identity event sits at the $J$-minimum $x = 1$. The present lemma is the bridge that makes those two languages interchangeable for the whole gauge.
proof idea
Term-mode, two rewrites. First reduce the claim by definition of $G$ to $\mathrm{cost}_\lambda(c, e^t) = \cosh(c t) - 1$. Then apply costLambda_eq_cosh at the strictly positive point $e^t$, which yields $\cosh(c\log(e^t)) - 1$, and cancel $\log\circ\exp$ by Real.log_exp. No case splits or analytic hypotheses beyond positivity of the exponential.
why it matters
This is the log-coordinate normal form for the entire cost gauge. Downstream, costLambda_coshAddIdentity uses it to prove every gauge member satisfies the Recognition Composition Law (both sides collapse to $2\cosh(ct)\cosh(cu)-2$ via cosh-add). The calibration criterion costLambda_isCalibrated_iff rewrites $G$ via this lemma and reads off $G''(0) = c^2$, so calibration forces $c = 1$.
In the uniqueness module the same identity appears as G_costLambda (function extensionality form) and feeds calibration_value_costLambda ($\mathrm{deriv}^2 G = \ell^2$) and the §9 payoff composition_law_monotone_forces_costLambda, which places any reciprocal, normalized, composition-law, monotone cost inside the gauge. Framework-wise this is the concrete realization of the T5 $J$-uniqueness family before the unit-curvature pin selects $J$ itself; the residual scale $c$ is exactly the one free posit that calibration kills.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.