physical_one_act_calibration_headline
plain-language theorem explainer
Any physical one-act instrument is forced to the canonical cost unit 1, such an instrument exists, and its continuum interface carries the same unit. Calibration and foundation authors cite this as the bridge from lab-style one-act readout to the normalized abstract interface. The proof is a three-conjunct term packing the forcing lemma, the canonical witness, and definitional unit agreement.
Claim. Every physical one-act instrument $I$ (positive candidate unit, readout equal to one-act curvature of that unit, readout locked to $1$) satisfies $I.\mathrm{unit}=1$; there exists at least one such instrument with unit $1$; and the normalized continuum interface extracted from $I$ carries exactly $I$'s unit.
background
In the primitive recognition calculus, a physical one-act instrument packages a positive real candidate unit, 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 extracted continuum interface is the normalized one-act interface whose unit field is that candidate.
Upstream, the forcing lemma states that any such instrument forces the canonical cost unit: the physical instrument forces unit $=1$ by reducing through the normalized-interface forcing for the $J$-cost side. Separately, a canonical instrument is defined at unit $1$ with readout $1$, using the identity for one-act curvature at the unit, as a consistency witness rather than lab hardware.
The module sits in the foundation layer that calibrates continuum one-act data against the native discrete unit (the one-step orbit in the finite $\delta$-orbit). The headline packages uniqueness, existence, and interface agreement into a single calibration claim.
proof idea
Term-mode conjunction of three facts. The first conjunct is exactly the forcing theorem: every one-act instrument has unit $1$, via reduction to the normalized-interface $J$-forcing on the extracted interface. The second is the pair of the canonical instrument (unit $1$, readout $1$, curvature identity) with reflexivity, witnessing existence. The third is definitional: the interface map copies the instrument's unit field, so unit agreement is rfl for every instrument.
why it matters
This is the physical calibration headline for one-act normalization: abstract unit forcing is realized by any physical instrument, existence is witnessed, and the continuum interface is faithful on the unit. Downstream it feeds the strong closure certificate in Delta-native strong closure, which assembles the closed Delta-native theorem surface (real forgetful protocol, generable carrier, certified analytic and transformer entries).
In the Recognition framework it pins the continuum-side unit to the same canonical value that the native discrete unit predicate isolates as the one-step orbit. That alignment is a prerequisite for treating lab-style one-act curvature readouts as instances of the normalized interface used in later forcing and mass-ladder work. It does not itself invoke T5–T8, but it stabilizes the unit that those steps assume when continuum and discrete sides are identified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.