logCurvature
plain-language theorem explainer
The second derivative at zero of the continuum cost member cosh(c t) − 1 equals c². Calibration and chain-bridge results cite this as the log-curvature invariant that labels residual gauge freedom after the δ-forced cost form is fixed. Who needs the continuum unit fixed to recover canonical J will reach for it. The proof is elementary real calculus: chain rule twice on cosh, then evaluate at the origin.
Claim. For every real number $c$, the second derivative at the origin of the map $t \mapsto \cosh(c t) - 1$ equals $c^2$: $$\frac{d^2}{dt^2}\Big|_{t=0}\bigl(\cosh(c t) - 1\bigr) = c^2.$$
background
In Recognition Science the unique cost forced by the Recognition Composition Law is $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$ (T5 J-uniqueness). In the logarithmic coordinate $t = \log x$ this becomes the one-parameter family $\cosh(c\cdot t) - 1$, of which canonical $J$ is the $c = 1$ member.
The discrete $\delta$-carrier that forces the cosh shape does not fix the continuum second-derivative scale. That residual real parameter is the log-curvature of the cost member at the unit $t = 0$. This module isolates that continuum gauge datum so later results can normalize it to 1 and recover $J$.
The surrounding calibration target treats curvature as an invariant of the function (not of a coordinate choice), which is why a pure calculus identity at $t = 0$ is enough to label the whole family.
proof idea
First show that the first derivative of $t \mapsto \cosh(c t) - 1$ is $t \mapsto c,\sinh(c t)$. Build a HasDerivAt certificate: scale the identity map by $c$, compose with hasDerivAt_cosh, subtract the constant 1, then extract deriv and tidy by ring. Rewrite the goal under that identity.
Next differentiate $t \mapsto c,\sinh(c t)$ at $0$: compose hasDerivAt_sinh with the same linear inner map, multiply by the outer factor $c$, and read off the derivative. Evaluate at zero with $\cosh 0 = 1$ and the zero multiplications (mul_zero, one_mul, mul_one), then finish by ring to $c^2$.
why it matters
This is the computational engine of the continuum calibration story. Downstream, the one-act curvature identity is just a rename of this fact. Faithfulness of the cost family (distinct positive curvature parameters give distinct functions) is proved by reading off this invariant at $t = 0$. Normalizing curvature to 1 forces $c = 1$, i.e. selects $J$. The Item 2 headline theorem assembles all three: the $\delta$-forced form leaves a faithful one-parameter gauge family whose only invariant is log-curvature $c^2$, and "curvature = 1" is exactly the condition selecting $J$.
On the chain side, the bridge result applies this at $c = 1$ to confirm that the RS cost entry is the gauge-fixed member with log-curvature exactly 1, not merely some member of the $\delta$-forced family. That pins T5's unique $J$ to the continuum calibration target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.