canonicalInstrument
plain-language theorem explainer
A concrete physical one-act instrument sits at unit 1 with readout 1, witnessing that the normalized continuum interface is attainable. Anyone citing the physical one-act calibration headline needs this existence half. The instance fills structure fields: positivity and the curvature identity close by arithmetic after rewriting one-act curvature as a square.
Claim. Define the canonical physical one-act instrument by unit $u=1$, readout $r=1$, with $0<1$, $r$ equal to the one-act curvature of $u$, and $r$ locked to $1$. (One-act curvature of a candidate unit $c$ is $c^2$.)
background
In the primitive recognition calculus, a physical one-act instrument packages four data: a positive candidate unit $u\in\mathbb{R}$, a real readout, a proof that the readout equals the one-act curvature of that unit, and a lock that the readout equals one. The structure then projects to a normalized continuum-side interface whose unit field is exactly $u$.
Upstream, one-act curvature is identified with the residual gauge parameter read as a second derivative: for any real $c$, one-act curvature equals $c^2$. The companion continuum fact is that the single normalization "one-act curvature equals 1" forces $c=1$ and thereby selects the canonical cost. This module sits on that calibration layer and treats instruments as physical witnesses of the same normalization, not as lab hardware constructions.
proof idea
Structure instance with unit and readout both set to $1$. Positivity is norm_num on $0<1$. The curvature field rewrites via oneActCurvature_eq (one-act curvature equals the square) and closes by norm_num since $1^2=1$. The lock is definitional equality rfl of readout with $1$.
why it matters
Supplies the existence half of the physical one-act calibration headline: any instrument forces unit $=1$, and there exists an instrument with unit $=1$ (this one), while the interface projection preserves the unit. The doc-comment is explicit that this is a consistency witness, not a construction of apparatus. Together with the forcing lemma that every instrument has unit $1$, it closes the bridge from abstract one-act normalization to a physically stated instrument datum at the continuum interface. In the broader Recognition chain this is local calibration bookkeeping under the J-cost / continuum interface, not a new forcing step (T5–T8 already fix $J$, $\varphi$, the eight-tick octave, and $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.