NormalizedOneActInterface
plain-language theorem explainer
A normalized one-act interface is the minimal continuum-side datum that closes cost-unit calibration: a positive real unit whose primitive one-act log-curvature equals one. Calibration and PRC authors cite it as the exact interface that is necessary and sufficient for selecting the canonical unit. It is pure structure data (positivity plus the curvature equation), not a proved identity.
Claim. A normalized one-act interface consists of a positive real cost unit $u>0$ together with the assertion that the log-curvature of the primitive one-act chart at $u$ equals $1$.
background
In the Primitive Recognition Calculus calibration layer, discrete recognition laws leave a faithful one-real torsor of candidate cost units: they do not force the unit by themselves. Closing that gap needs a continuum-side interface that is deliberately thin: not a full continuum and not a field completion, only a positive unit plus unit log-curvature of the primitive one-act chart.
One-act curvature is the second-order response of recognition cost under a single continuum act. Upstream, recognition cost is the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), appearing as event cost in observer forcing and as the derived cost of multiplicative recognizers. Related forcing packages supply the canonical self-similar dressing and the initial Peano arithmetic object; the present module only packages the minimal second-order lock that selects among positive units.
proof idea
Definitional structure, not a proof. It records three fields: a real unit, a positivity witness $0<u$, and the equation that one-act curvature of that unit equals 1. No tactics run at the structure itself. Downstream, the forcing theorem applies the one-act unit-forcing lemma to the positivity and curvature fields and concludes the unit is 1; the canonical inhabitant is built by setting the unit to 1 and discharging curvature via the explicit one-act curvature identity.
why it matters
This is the exact interface datum in the calibration closure theorem: discrete laws leave a one-real torsor, while any normalized one-act interface forces the unit to 1, and for positive candidates the curvature condition is necessary and sufficient for the canonical member. It is inhabited by the canonical interface, feeds the theorem that every such interface forces the canonical cost unit, and is the abstract core of the physical one-act instrument (positive unit, curvature readout, lock-to-one). In framework terms it is the continuum-side lock after J-uniqueness (T5): the second-order recognition interface that closes the cost-unit gap without smuggling a full continuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.