calibration_value_costLambda
plain-language theorem explainer
The log-coordinate curvature of the gauge cost F_λ at the unit equals λ²: the second derivative of G(F_λ) at 0 is exactly λ². Anyone selecting the unique calibrated member of the cost family, or proving the gauge parameterization is faithful, cites this identity. The proof is a direct chain-rule computation on cosh(λt)−1, evaluated at the origin.
Claim. For every real $\lambda$, let $F_\lambda$ be the corresponding member of the gauge cost family and let $G_F(t)=F(e^t)$ be its log-coordinate reparametrization. Then $$\frac{d^2}{dt^2}\Big|_{t=0} G_{F_\lambda}(t)=\lambda^2.$$
background
Recognition Science takes the native cost on positive ratios to be the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. The functional-equation layer reparametrizes any candidate cost $F$ by $G_F(t)=F(e^t)$, so the curvature of $F$ at the multiplicative unit becomes the ordinary second derivative of $G_F$ at $t=0$. Calibration demands that this curvature equal 1 (the normalization used by the law that forces J).
The one-parameter family $F_\lambda$ is the gauge orbit obtained by stretching the log coordinate by $\lambda$. Explicitly, $G_{F_\lambda}(t)=\cosh(\lambda t)-1$, so $F_1$ recovers $J$ on $\mathbb{R}_{>0}$. This module stratifies that family: $\delta$ plus algebra force the orbit; calibration is the remaining within-family selector.
proof idea
Rewrite $G(F_\lambda)$ via the closed form $G(F_\lambda)(t)=\cosh(\lambda t)-1$. The map $t\mapsto\lambda t$ has derivative $\lambda$ everywhere. Differentiating the cosh composition then gives first derivative $\sinh(\lambda t)\cdot\lambda$. Differentiating again at $t=0$ yields $\cosh(0)\cdot\lambda\cdot\lambda$. Substitute the derivative equalities, use $\cosh 0=1$, and finish by ring simplification to $\lambda^2$.
why it matters
This identity is the exact numerical content of "calibration selects $\lambda=\pm 1$". Downstream, the calibrated-member criterion rewrites IsCalibrated$(F_\lambda)$ as $\lambda^2=1$; with $\lambda>0$ one obtains $\lambda=1$ and recovers $J$. The same curvature feeds injectivity of the gauge parameterization (equal costs share equal $\lambda^2$, hence equal positive $\lambda$) and underwrites the single-orbit picture under multiplicative automorphisms.
In the forcing chain this is the within-family half of T5 J-uniqueness: $\delta$ plus algebra force the family; calibration $\lambda^2=1$ picks $J$. The absolute value of the calibration constant (the residual gauge) is not itself fixed by $\delta$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.