canonicalInterface
plain-language theorem explainer
The canonical normalized one-act interface is the continuum-side calibration datum with cost unit equal to 1 and unit log-curvature on the primitive one-act chart. Citation target for anyone invoking the calibration closure theorem, which needs an explicit witness that such an interface exists. Construction is immediate: fix the unit at 1 and discharge positivity and curvature by numerical check against the one-act curvature identity.
Claim. There is a normalized one-act interface with cost unit $u = 1$, satisfying $0 < 1$ and $\mathrm{oneActCurvature}(1) = 1$ (unit log-curvature of the primitive one-act chart).
background
In the Primitive Recognition Calculus calibration layer, discrete recognition laws leave the cost unit free on a faithful one-real torsor: they do not force $c = 1$. Closing that gap requires a minimal continuum-side interface, not a full field completion.
A normalized one-act interface is exactly that datum: a positive real cost unit together with the assertion that the primitive one-act chart has unit log-curvature at that unit. This matches the classical Calibration axiom on cost functionals (second derivative of $F(\exp t)$ at the origin equals 1), which normalizes curvature so the cost is unique rather than a scale family.
Upstream, the one-act curvature identity equates the chart curvature at a candidate unit to an explicit numerical expression, so the unit-$1$ case is checkable by arithmetic.
proof idea
Definitional construction of the structure. Set the cost unit field to $1$. Positivity is norm_num on $0 < 1$. The curvature field rewrites via the sibling identity equating one-act curvature at the unit to its closed form, then norm_num verifies that value is $1$. No external lemmas beyond that identity and numeric normalization.
why it matters
Supplies the existence witness in the calibration closure theorem: discrete laws leave a one-real torsor of units, while any normalized one-act interface is necessary and sufficient for $c = 1$. The cost-unit issue is thereby classified as not discrete-forced and closed exactly by this minimal second-order recognition interface.
That closure sits under the CostAxioms Calibration normalization (curvature at unity) and aligns with T5 J-uniqueness of the cost $J(x) = (x + x^{-1})/2 - 1$, where the same second-order normalization selects the unique solution of the Recognition Composition Law rather than a scale family. Downstream, the closure theorem packages existence, uniqueness of the unit, and injectivity of the cosh-scaled cost family into one statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.