curvature_one_iff_J
plain-language theorem explainer
Normalizing the second derivative of cosh(c t)−1 at t=0 to equal 1 forces c=1, selecting the canonical cost J among the one-parameter family. Anyone calibrating the continuum cost or proving unit uniqueness cites this. The proof rewrites via log-curvature (equals c²) and factors c²−1 under positivity.
Claim. For every real $c>0$, the second derivative at $0$ of $t \mapsto \cosh(c t)-1$ equals $1$ if and only if $c=1$.
background
In the Primitive Recognition Calculus calibration layer, the δ-forced cost form still leaves a one-parameter continuum family $t \mapsto \cosh(c t)-1$ for $c>0$. The residual gauge parameter is read off as log-curvature: the second derivative of that member at the unit $t=0$.
Upstream, logCurvature states that this second derivative equals $c^2$. The canonical Recognition cost is the $c=1$ member, which in multiplicative coordinates is $J(x)=\cosh(\ln x)-1=\frac12(x+x^{-1})-1$ (the T5 unique cost). Calibration means fixing that curvature to 1 so the continuum interface selects $J$ rather than a rescaled twin.
proof idea
Rewrite the left-hand side by logCurvature, which replaces the double derivative at 0 with $c^2$. The claim becomes $c^2=1\leftrightarrow c=1$ under $c>0$.
Forward: from $c^2=1$ obtain $(c-1)(c+1)=0$ by nlinarith, split with mul_eq_zero, and discard $c=-1$ by positivity (linarith). Backward: substitute $c=1$ and evaluate $1^2=1$ by norm_num.
why it matters
This is the algebraic hinge that turns the continuum normalization "one-act curvature equals 1" into selection of canonical $J$. Downstream, unit_forced_by_one_act is a one-line unfold that cites it; costLambda_isCalibrated_iff uses the same identity to say calibration of costLambda c holds iff $c=1$; and calibration_unit_is_a_gauge packages it as the third conjunct of the Item-2 headline (curvature $=1$ selects $J$, while the discrete δ carrier does not fix the unit).
In the forcing chain this locks the T5 cost representative once the continuum second-derivative gauge is set, separating discrete recognition structure from the residual real scaling that only continuum calibration can kill.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.