calibration_datum_necessary_and_sufficient
plain-language theorem explainer
For any positive real unit c, the one-act log-curvature equals 1 if and only if c = 1, selecting the canonical cost member. Continuum-interface and calibration arguments cite this as the exact one-datum closure of the residual gauge: necessary and sufficient, nothing more. The proof is a one-line symmetry of the already-proved unit-forcing theorem.
Claim. For every real $c > 0$, one has $c = 1$ if and only if the one-act curvature of the cost member with unit $c$ equals $1$, where that curvature is the second derivative at $t = 0$ of $t \mapsto \cosh(c\, t) - 1$.
background
In the Primitive Recognition Calculus calibration layer, the cost family is parameterized by a positive real unit $c$. The continuum interface reads a second-order quantity: the one-act log-curvature, defined as the second derivative at $t = 0$ of $t \mapsto \cosh(c t) - 1$. That residual gauge parameter evaluates to $c^2$ and lives in the real-protocol layer, not on the discrete rational carrier.
Upstream, the theorem that one continuum datum fixes the unit already proves the biconditional in the opposite presentation: one-act curvature equals 1 if and only if $c = 1$, via the curvature-one criterion for the canonical $J$. A sibling result records that the discrete carrier alone does not force the unit, leaving a faithful one-real torsor. The present statement is the calibration-gap phrasing of that same continuum forcing: one datum, no more and no less, selects the canonical member.
proof idea
One-line term proof: apply symmetry of the upstream unit-forcing theorem. That theorem unfolds one-act curvature and invokes the curvature-one criterion for $J$ under the hypothesis $c > 0$; flipping the biconditional yields the stated form.
why it matters
This is the exact closure of the calibration gap in the cost-unit story: the one-act curvature datum is necessary and sufficient for the canonical member. It is consumed by the calibration closure theorem in the same module, which packages four facts: every normalized one-act interface has unit 1; the present biconditional for all positive $c$; existence of a normalized interface (the canonical member); and faithfulness of the continuum cost family under equal cosh profiles.
Framework-wise it sits under T5 $J$-uniqueness ($J(x) = \cosh(\log x) - 1$): the continuum second-derivative normalization pins the residual scale that discrete Recognition Composition Law identities leave free. The discrete non-forcing sibling and this continuum sufficiency together classify the cost-unit issue completely: not discrete-forced; closed exactly by the minimal second-order recognition interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.