isCalibrated_costLambda_pos_iff
plain-language theorem explainer
For every positive real exponent λ, the one-parameter cost F_λ(x)=(x^λ+x^{-λ})/2−1 is calibrated (G''(0)=1 in log coordinates) if and only if λ=1. This is the positive-ray half of the calibration gauge that isolates J among the δ-forced family. Anyone proving that completion selects J, or assembling the cost-joint stratification, cites it. The proof rewrites to the unrestricted calibration criterion and finishes by elementary quadratic arithmetic.
Claim. Let $\lambda\in\mathbb{R}$ with $\lambda>0$, and write $F_\lambda(x)=\frac{x^\lambda+x^{-\lambda}}{2}-1$. Then $F_\lambda$ is calibrated, meaning $G''(0)=1$ where $G(t)=F_\lambda(e^t)$, if and only if $\lambda=1$.
background
In the Primitive Recognition Calculus cost story, the δ-forced multiplicative family is the one-parameter gauge $F_\lambda(x)=\frac{x^\lambda+x^{-\lambda}}{2}-1$ (real powers). The member $\lambda=1$ is exactly the RS recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$, also written $\cosh(\log x)-1$.
Calibration (Condition 1.2) is the normalization $\mathrm{deriv}(\mathrm{deriv}(G_F))(0)=1$, equivalently $\lim_{t\to 0}2F(e^t)/t^2=1$, where $G_F(t)=F(e^t)$. It is an irreducible scale choice on the family: without it every positive exponent is a legitimate cost solution of the composition law.
The module develops native uniqueness of $J$ inside this family. An upstream sibling gives the unrestricted criterion relating calibration of $F_\lambda$ to an algebraic condition on $\lambda$; the present statement specializes that criterion to $\lambda>0$.
proof idea
One short term-mode argument. Rewrite the goal by the unrestricted calibration criterion isCalibrated_costLambda_iff, which converts calibration of $F_\lambda$ into an algebraic relation in $\lambda$ (essentially $\lambda^2=1$).
The forward direction feeds nlinarith the nonnegativity of $(\lambda-1)^2$ and $(\lambda+1)^2$ together with $\lambda>0$, forcing $\lambda=1$. The reverse direction substitutes $\lambda=1$ and closes by norm_num.
why it matters
This is the positive-exponent half of the headline that calibration selects $J$. Downstream, prc_jcost_strength_separation quotes it directly as completion_selects_jcost: δ-only does not force $J$, but the completion (calibration) does, and the strength tag strictly increases. It also feeds prc_cost_joint_stratification (the honest cost-joint assembly) and sits beside the single-point gauge theorem costLambda_single_point_calibration.
In the forcing chain this is the local PRC face of T5 J-uniqueness: among the RCL solutions $F_\lambda$, the curvature normalization $G''(0)=1$ pins $\lambda=1$, recovering $J(x)=\cosh(\log x)-1$. No project-local axioms are used.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.