oneActCurvature_eq
plain-language theorem explainer
For every real residual gauge parameter c, the one-act curvature equals c squared: the continuum interface reads the residual scale as a pure second-derivative (log-curvature) datum. Anyone proving that a single continuum normalization forces the canonical unit cites this identity. The proof is a one-line appeal to the calibration log-curvature evaluation.
Claim. For every real number $c$, the one-act curvature of $c$ equals $c^2$. Equivalently, the residual gauge parameter, read as the second derivative of the cost in logarithmic coordinates, is exactly the square of that parameter.
background
In the Primitive Recognition Calculus, cost functionals on the continuum interface carry a residual positive scale $c$ after discrete structure is fixed. Calibration (Cost Axioms, Axiom 3) normalizes that freedom by requiring the second derivative at the origin in log coordinates to equal one: if $G(t)=F(e^t)$, then $G''(0)=1$. That second derivative is the curvature of the cost at unity and is what selects a unique solution rather than a one-parameter family.
The local module treats the continuum interface of the real $\delta$-carrier. One-act curvature packages the residual gauge $c$ as that log-curvature readout. Upstream, the calibration class and related forcing structures supply the meaning of the second-derivative normalization; the present identity simply evaluates it on the residual parameter.
proof idea
Term-mode one-liner. The goal oneActCurvature c = c^2 is discharged by applying Calibration.logCurvature at $c$, which is the evaluation of the log-coordinate second derivative on the residual gauge and returns $c^2$ by definition of that readout.
why it matters
This identity is the algebraic hinge of the Phase 4 headline that calibration comes from one continuum act. Downstream, calibration_is_one_continuum_act packages three facts: curvature is always $c^2$; for $c>0$, curvature equals 1 if and only if $c=1$; and the cosh-scaled cost family is faithful in the scale. The first conjunct is exactly this theorem.
It also builds the canonical normalized interface (unit $1$, curvature unit via rewrite of this equality) and the physical one-act instrument's curvature readout. In framework terms it closes the residual real gauge left after discrete structure: one continuum datum removes one real, forcing the canonical $J$ (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) at unit scale rather than a scaled family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.