calibration_is_one_continuum_act
plain-language theorem explainer
Packages the Phase 4 calibration headline: one-act curvature equals the square of the continuum scale, so normalizing that curvature to 1 forces the scale to 1, and the continuum charts t ↦ cosh(c t)−1 separate distinct positive scales. Anyone citing the claim that λ=1 is fixed by a single continuum-interface datum (not by discrete δ) uses this. The proof is a three-conjunct term packing equality, unit-forcing, and clog injectivity.
Claim. The one-act curvature map satisfies $\mathrm{curv}(c)=c^2$ for every real $c$; for $c>0$, $\mathrm{curv}(c)=1$ if and only if $c=1$; and for $c,d>0$, if $t\mapsto \cosh(c t)-1$ equals $t\mapsto \cosh(d t)-1$ as functions, then $c=d$.
background
In the Recognition cost calculus, calibration is the normalization that removes the residual real gauge on the cost functional. CostAxioms states it as: if $G(t)=F(e^t)$, then $G''(0)=1$, so the log-curvature at unity is fixed and the solution is unique rather than a family. The discrete carrier alone does not pin that unit: residual scale is a one-real torsor.
This module works at the continuum interface $\mathbb{R}_\delta$. The primitive one-act chart is the continuum family $t\mapsto \cosh(c t)-1$ (the same shape as the unique $J$-cost $J(x)=\cosh(\log x)-1$ from T5). One-act curvature is the second-derivative / log-curvature extracted from that chart at the origin; sibling lemmas identify it with $c^2$ and show that setting it to 1 forces $c=1$.
Upstream calibration structures (CostAxioms.Calibration, CostFromDistinction.Calibration) supply the general meaning of a calibration datum: a distinguished inconsistent configuration and a positive cost value, or equivalently a second-derivative normalization. Here the datum is specialized to a single continuum one-act curvature condition.
proof idea
Term-mode triple pairing. First conjunct is the sibling equality oneActCurvature_eq, which identifies one-act curvature with $c\mapsto c^2$. Second conjunct applies unit_forced_by_one_act at each positive $c$, giving the biconditional curvature $=1$ iff $c=1$. Third conjunct is Calibration.clog_inj: positive scales are recovered injectively from equality of the continuum charts $t\mapsto \cosh(c t)-1$. No further rewriting; the theorem is the packaged conjunction of those three facts.
why it matters
Phase 4 headline of the primitive recognition calculus: $\lambda=1$ (equivalently the cost unit $c=1$) is derived from exactly one named continuum-interface datum, the one-act curvature normalization, while the discrete $\delta$ side is explicitly not enough. That matches the honest conditional in the doc-comment: residual gauge is one real, removed by one continuum act at the $\mathbb{R}_\delta$ interface.
It sits next to discrete_does_not_force_unit, NormalizedOneActInterface, normalized_interface_forces_J, and calibration_gap_closed_by_normalized_interface, which turn this packaging into the minimal interface that closes calibration and forces the $J$-cost. Framework-wise it discharges CostAxioms Calibration (G''(0)=1) in the continuum one-act language tied to T5 $J$-uniqueness $J(x)=\cosh(\log x)-1$. No used_by edges yet; the immediate consumers are the normalized-interface closure lemmas in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.