oneActCurvature
plain-language theorem explainer
Defines the one-act log-curvature of a cost member with positive unit $c$ as the second derivative at $t=0$ of $t\mapsto\cosh(ct)-1$. That value is the continuum-interface reading of the residual gauge parameter and equals $c^2$. Downstream calibration theorems cite it as the single real datum that forces the canonical unit $c=1$. The body is a direct second-derivative definition, not a proved identity.
Claim. For a real unit $c$, the one-act curvature is $\frac{d^2}{dt^2}\big|_{t=0}\bigl(\cosh(c t)-1\bigr)$. It is a continuum-interface scalar (a second derivative at the limit ratio $t=0$), not a discrete rational carrier quantity.
background
Recognition Science fixes the cost kernel $J$ uniquely (forcing chain T5) as $J(x)=\cosh(\log x)-1$. Scaling the log-chart by a positive unit $c$ yields the one-parameter family $t\mapsto\cosh(c t)-1$. The discrete rational carrier leaves a faithful one-real torsor of such units: no discrete $\delta$ datum selects $c=1$.
This module works in the $\mathbb{R}\delta$ protocol layer that bridges discrete ledger structure to continuum interface data. The one-act curvature is the minimal second-order continuum observable on that family: evaluate the second derivative of the scaled cosh chart at the identity ratio $t=0$.
Sibling results then prove the curvature equals $c^2$ and that normalizing it to $1$ forces $c=1$, closing the calibration gap with exactly one continuum act.
proof idea
Definitional, not a proof. The body sets the value equal to deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0, i.e. the ordinary second derivative of the scaled cosh-minus-one chart at the origin. Noncomputable because real differentiation is used. The identity that this equals $c^2$ is the separate theorem oneActCurvature_eq (via Calibration.logCurvature).
why it matters
This is the named continuum datum that closes cost-unit calibration. Downstream, oneActCurvature_eq evaluates it to $c^2$; unit_forced_by_one_act shows that for $c>0$, curvature $=1$ iff $c=1$; and calibration_is_one_continuum_act packages the Phase-4 headline that $\lambda=1$ is derived from exactly one recognition act at the $\mathbb{R}\delta$ interface.
NormalizedOneActInterface packages a positive unit together with the assertion that this curvature equals $1$. The closure theorem calibration_gap_closed_by_normalized_interface then states the full classification: the discrete laws do not force the unit, while the normalized one-act interface is necessary and sufficient for $c=1$. That is the honest residual-gauge accounting tied to T5 $J$-uniqueness: one real removed by one second-order datum, no hidden continuum completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.