normalized_interface_forces_J
plain-language theorem explainer
Any continuum interface that supplies a positive cost unit together with unit one-act log-curvature is forced to the canonical unit c = 1. Calibration and physical-instrument arguments cite this as the sufficiency half of cost-unit selection. The proof is a one-line modus ponens through the positive-unit curvature forcing lemma.
Claim. If $I$ is a normalized one-act interface (a positive real cost unit $u$ together with the assertion that the primitive one-act log-curvature of $u$ equals $1$), then $u = 1$.
background
In the primitive recognition calculus, discrete laws alone leave a faithful one-real torsor of cost units: they do not pin $c = 1$. Closing that gap needs a minimal continuum-side datum, not a full field completion.
A normalized one-act interface is exactly that datum: a positive real unit and the assertion that the primitive one-act chart has unit log-curvature, written oneActCurvature unit = 1. The curvature is the second-order recognition observable tied to the J-cost shape $J(x) = \cosh(\log x) - 1$ (equivalently $(x + x^{-1})/2 - 1$).
Upstream, unit_forced_by_one_act already shows that for any positive real the curvature condition is equivalent to the unit being $1$. The present theorem packages that equivalence against the interface structure.
proof idea
One-line term proof. Apply the forward direction of unit_forced_by_one_act at the interface's positivity witness, then feed the interface's curvature_unit hypothesis via modus ponens. No extra algebra is performed here; the work lives in the curvature-forcing lemma.
why it matters
This is the sufficiency arrow in the calibration closure theorem calibration_gap_closed_by_normalized_interface: every normalized one-act interface has unit $1$, the curvature condition is necessary and sufficient for $c = 1$ among positive reals, a witness interface exists, and the cosh-scaled cost charts separate units. Downstream, instrument_forces_canonical_unit reduces a physical one-act instrument to this statement by forgetting to the normalized interface.
In the Recognition forcing chain this sits next to T5 J-uniqueness: once the one-act log-curvature is normalized, the cost unit cannot float. The discrete side is already known not to force the unit (discrete_does_not_force_unit); this lemma shows the minimal second-order continuum interface does force it, closing the gap with one datum, no more and no less.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.