discrete_does_not_force_unit
plain-language theorem explainer
The continuum cost family t ↦ cosh(c t)−1 is faithful in the positive scale c and closed under positive time rescaling, so residual unit freedom is a one-real torsor. Calibration and continuum-interface arguments cite this to show discrete carrier data alone never pins the unit. Proof is a one-line re-export of the calibration cost-freedom torsor lemma.
Claim. For all positive reals $c,d$, if $t\mapsto\cosh(c t)-1$ equals $t\mapsto\cosh(d t)-1$ as functions of $t$, then $c=d$. Moreover, for all positive $c,d$ there exists $\mu>0$ such that $t\mapsto\cosh(c(\mu t))-1$ equals $t\mapsto\cosh(d t)-1$. Hence residual freedom of the cost unit is a one-real torsor: the discrete carrier does not force the unit.
background
Recognition Science forces the cost shape (T5) to $J(x)=\cosh(\log x)-1$, equivalently $(x+x^{-1})/2-1$. At the continuum interface one studies the scaled family $t\mapsto\cosh(c t)-1$ with positive real unit $c$. Distinct $c$ give distinct costs (faithfulness); any two units are related by a positive time reparameterization (transitive rescaling). Together those properties mean residual scale freedom is a one-real torsor.
The Calibration axiom normalizes curvature: if $G(t)=F(e^t)$, then $G''(0)=1$, selecting a unique solution rather than a family. Cost-from-distinction calibration instead names a distinguished inconsistent configuration and a positive cost value. This module separates how much of the pinning is discrete versus continuum-side.
Local setting (Phase 4): without a one-act continuum normalization datum the unit remains genuinely free on the discrete carrier.
proof idea
One-line term wrapper. The statement is exactly the conjunction already established by the calibration cost-freedom lemma (cost freedom is a one-real torsor): faithfulness of $c\mapsto(t\mapsto\cosh(c t)-1)$ on positive reals, plus existence of a positive rescaling $\mu$ matching any two units. No new analytic work is done at this declaration; it re-exports that lemma under the discrete-carrier reading used by the Phase 4 narrative.
why it matters
Phase 4 headline: the unit $c$ is a faithful one-real torsor on the discrete carrier; no discrete $\delta$ datum fixes it. A single continuum-interface datum (one-act curvature normalization) is what forces $c=1$. Downstream, the canonical normalized interface is built with unit $1$, and the objecthood registry classifies the cost-scale unit as convention/gauge: "a faithful, transitively-rescaled torsor, a single free real fixed only by a continuum-side datum."
This separates T5 J-uniqueness (shape of the cost) from residual scale gauge. The honest conditional is that calibration is not discrete-$\delta$-forced; $\lambda=1$ comes from exactly one recognition act at the continuum interface, with the residual gauge being one real removed by one named datum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.