unit_forced_by_one_act
plain-language theorem explainer
For any positive real scale c, one-act curvature equals 1 if and only if c equals 1. Continuum-calibration arguments cite this biconditional: a single normalization datum pins the residual cost unit to the canonical J. The proof unfolds the curvature definition and applies the Calibration lemma that unit curvature forces the unit.
Claim. For every real $c > 0$, the one-act curvature of the cost at scale $c$ equals $1$ if and only if $c = 1$. Equivalently, the continuum normalization that sets one-act curvature to unity selects the canonical cost unit.
background
In Recognition Science the cost functional on the discrete carrier is fixed only up to a positive real scale $c$. The cost family is faithful and transitively rescaled, so residual freedom is a one-real torsor: no discrete $\delta$ datum forces the unit.
At the continuum interface one introduces one-act curvature, the second-derivative normalization of the cost in log coordinates. CostAxioms Calibration states that $G''(0)=1$ where $G(t)=F(e^t)$, which "normalizes the curvature of the cost functional at unity, ensuring a unique solution rather than a family."
The local module packages the claim that exactly one continuum act closes this gap. Sibling facts record that one-act curvature of scale $c$ equals $c^2$, so the unit-curvature condition is algebraically $c^2=1$ under positivity.
proof idea
Short term-mode proof. Unfold the definition of one-act curvature, then apply the Calibration lemma that unit curvature is equivalent to the canonical scale, at the positivity hypothesis $c>0$. That lemma already carries the biconditional for the J-cost family; no further algebra is done here.
why it matters
Atomic forcing step for continuum calibration. Downstream, calibration_is_one_continuum_act packages it as the Phase 4 headline: the unit is a faithful one-real torsor on the discrete carrier, while a single continuum-interface datum forces $c=1$, so the scale is derived from exactly one recognition act at the continuum interface, with the residual gauge being one real removed by one datum.
It also feeds normalized_interface_forces_J (any normalized one-act interface has unit 1) and the necessity-and-sufficiency closure that one-act curvature equals 1 iff $c=1$. In the forcing chain this is the continuum half of selecting unique J (T5 / RCL), after the discrete carrier has left a residual real gauge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.