costLambda_isCalibrated_iff
plain-language theorem explainer
For every positive scale parameter c, the one-parameter cost family F_c is calibrated (second derivative of its log-coordinate form at zero equals 1) if and only if c equals 1. Uniqueness arguments for the Recognition cost J cite this to isolate calibration as the sole scale-fixing hypothesis. The proof reduces to the curvature identity for cosh(c t)-1 after identifying the log reparametrization.
Claim. Let $c>0$. Write $F_c$ for the $c$-scaled cost family whose log-coordinate form is $G(t)=\cosh(c t)-1$. Then $F_c$ is calibrated, i.e. $G''(0)=1$, if and only if $c=1$.
background
In the Recognition cost calculus, candidate costs $F:\mathbb{R}{>0}\to\mathbb{R}$ are studied through the log-coordinate reparametrization $G_F(t)=F(e^t)$. Calibration (Condition 1.2) is the normalization $G_F''(0)=1$, equivalently $\lim{t\to 0} 2F(e^t)/t^2=1$. It fixes the unit of scale on the positive reals.
The family under study is the gauge orbit of the J-cost under argument rescaling: its log form is $G(t)=\cosh(c t)-1$. The ambient module isolates which hypotheses of the uniqueness theorem law_of_logic_forces_jcost actually force $c=1$. Upstream, IsCalibrated is exactly the second-derivative condition on $G$, and the identity $G(F_c)=\cosh(c,\cdot)-1$ is already available as a sibling lemma.
proof idea
Apply the sibling identity $G_{F_c}(t)=\cosh(c t)-1$ by functional extensionality. Unfold calibration to the claim that the second derivative of this $G$ at $0$ equals $1$. Rewrite under the identity just obtained, then finish with the curvature lemma that $\frac{d^2}{dt^2}\big|_0(\cosh(c t)-1)=c^2$ equals $1$ precisely when $c=1$ (using $c>0$).
why it matters
This is the calibration half of Item 2 in the PRC calibration-independence argument. The parent theorem calibration_is_the_only_hypothesis_pinning_J uses it to show every gauge member satisfies reciprocity, normalization, the Recognition Composition Law, and continuity on the positives, while calibration holds only at $c=1$. Hence the four non-calibration hypotheses of the uniqueness theorem cannot alone determine $J$: the unit of scale is logically independent of that law set.
In the forcing chain this sits under T5 J-uniqueness. The canonical cost $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$ is forced only once calibration pins $c=1$. The result closes the claim that calibration is the sole scale-fixing hypothesis, not a redundant consequence of the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.