OneActInstrument
plain-language theorem explainer
A physical one-act instrument is a positive real candidate cost unit paired with a readout that equals the one-act curvature of that unit and is locked exactly to one. Calibration and unit-forcing results cite this carrier as the continuum-side datum a lab-style instrument would supply. The declaration is a structure with four fields; the companion conversion builds the normalized interface by rewriting the two equalities.
Claim. A one-act instrument consists of a positive real unit $u>0$ and a real readout $r$ such that $r$ equals the one-act curvature of $u$ and $r=1$. From any such instrument one obtains a normalized one-act interface whose unit field is $u$.
background
In the primitive recognition calculus, a one-act instrument is the continuum-side packaging of a single recognition act: choose a positive scale (the candidate cost unit), compute the one-act curvature at that scale, and demand that the instrument's readout equal both that curvature and the number one. The lock $r=1$ is the physical normalization condition; the equality with one-act curvature ties the readout to the RS cost geometry rather than an arbitrary meter.
The module sits downstream of delta-real calibration and the broader forcing chain that isolates the J-cost $J(x)=(x+x^{-1})/2-1$. Related cost constructions (multiplicative recognizer cost, rung-coarsen cost, measure-forcing weights) supply the ambient language of recognition cost, but this structure only needs the one-act curvature map and the already-defined normalized one-act interface.
The conversion toInterface is the bridge: every instrument yields a normalized interface with the same unit, so later theorems can apply interface-level forcing lemmas without re-proving field bookkeeping.
proof idea
Pure structure definition: four fields (unit, positivity, readout, two equalities). No tactic proof on the structure itself.
The companion conversion to a normalized one-act interface copies unit and positive, then discharges the interface curvature-unit obligation by rewriting: reverse the reads-curvature equality and substitute the lock-to-one field, so the interface sees curvature equal to one at that unit.
why it matters
This is the data type the physical one-act calibration story is about. Downstream, instrument_forces_canonical_unit applies the normalized-interface forcing lemma to I.toInterface and concludes every instrument has unit equal to one. canonicalInstrument is the consistency witness at unit one. The headline theorem packages both directions: every instrument forces unit one, some instrument exists at unit one, and the interface conversion preserves the unit field.
In framework terms this is the lab-facing half of cost-unit calibration: once a physical readout is locked to one-act curvature and to one, the only admissible unit is the canonical RS cost unit. It does not invent new physics constants; it pins the continuum interface so later alpha-band and mass-ladder normalizations speak the same unit language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.