isCalibrated_costLambda_iff
plain-language theorem explainer
The one-parameter cost F_λ(x)=(x^λ+x^{-λ})/2−1 is calibrated (log-coordinate curvature at the unit equals 1) exactly when λ²=1. Anyone pinning J inside the δ-forced gauge family cites this criterion. The proof is a direct rewrite of the calibration predicate through the already-computed value λ².
Claim. For every real $\lambda$, the cost $F_\lambda(x)=\frac12(x^\lambda+x^{-\lambda})-1$ satisfies the calibration condition $\frac{d^2}{dt^2}\big|_{t=0} F_\lambda(e^t)=1$ if and only if $\lambda^2=1$.
background
In the Primitive Recognition Calculus native-cost uniqueness module, costs live in the multiplicative gauge family $F_\lambda(x)=\frac12(x^\lambda+x^{-\lambda})-1$ (equivalently $\cosh(\lambda\log x)-1$ on positives). The member $\lambda=1$ is the recognition cost $J$.
Calibration (Condition 1.2 of the functional-equation package) is the unit-curvature demand: writing $G(t)=F(e^t)$, one requires $G''(0)=1$, equivalently $\lim_{t\to 0} 2F(e^t)/t^2=1$. Upstream, the calibration value of $F_\lambda$ is computed exactly: $G''(0)=\lambda^2$. That identity is the sole input here.
The local setting is the within-family selection step of the law-of-logic forcing chain: $\delta$ plus algebra force the family; calibration then cuts the family down to $\lambda=\pm 1$.
proof idea
Term-mode, two steps. Unfold the definition of calibration to the statement $G''(0)=1$ for $G(t)=F_\lambda(e^t)$. Rewrite that equality by the upstream identity that the second derivative at zero equals $\lambda^2$. The biconditional $\mathrm{IsCalibrated}(F_\lambda)\leftrightarrow\lambda^2=1$ is immediate. No further analysis or case splits.
why it matters
This is the exact within-family selection lemma that makes the stratification of recognition costs sharp: $\delta$ plus algebra force ${F_\lambda}$; calibration $\lambda^2=1$ selects the $\pm 1$ members; positivity then isolates $\lambda=1$, i.e. $J$. It feeds the positive-exponent refinement (calibrated iff $\lambda=1$), and sits under the two capstones that force $J$ by monotonicity alone and by the completeness-free law of logic. In the forcing chain this is the concrete content of T5 J-uniqueness inside the native PRC cost family: the Recognition Composition Law plus calibration pin $J(x)=\frac12(x+x^{-1})-1=\cosh(\log x)-1$. The gauge value itself is not fixed by $\delta$; only the curvature condition selects it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.