classify_convention
plain-language theorem explainer
The cost-scale unit is pure gauge: the family t ↦ cosh(c t)−1 is faithful in c>0, yet any two positive units are related by a positive time rescaling μ. Anyone tracking residual freedom after discrete recognition cites this. The proof is a one-line alias of the discrete-carrier calibration theorem.
Claim. For all $c,d>0$, if $t\mapsto\cosh(c t)-1$ equals $t\mapsto\cosh(d t)-1$ as functions then $c=d$; and for all $c,d>0$ there exists $\mu>0$ such that $t\mapsto\cosh(c(\mu t))-1$ equals $t\mapsto\cosh(d t)-1$. Thus the cost-scale unit is a faithful, transitively rescaled one-real torsor (a gauge fixed only by continuum-side data).
background
In the Primitive Recognition Calculus, continuous cost is the one-parameter family $J_c(t)=\cosh(c t)-1$. This is the continuum avatar of the RS J-cost $J(x)=\cosh(\log x)-1$ (T5), with $c$ playing the role of a scale unit on the time/argument axis.
ObjecthoodRegistry partitions RS objects by how they are forced: rationals, scale, display, completion, convention, quotient, observable, permitted. The convention slot is the residual unit freedom after the discrete carrier is fixed.
Upstream, DeltaRealCalibration proves that the discrete carrier does not force the unit: the cost family is faithful (distinct units give distinct costs) and transitively rescaled, so residual freedom is a one-real torsor. Without a one-act normalization datum the unit is genuinely free.
proof idea
One-line term wrapper: the statement is definitionally identical to discrete_does_not_force_unit from DeltaRealCalibration, so the proof is just that theorem name. No extra algebra or case split is performed here; classification only re-tags the calibration result as the convention entry in the objecthood table.
why it matters
Places the cost-scale unit in the objecthood periodic table as gauge, not as a forced RS object. That separation matters for the forcing chain: T5 fixes the shape $J(x)=\cosh(\log x)-1$, but the absolute unit on the continuous argument remains a continuum-side normalization (hbar, c, etc. in RS-native units). Downstream siblings (classify_forced_rationals, classify_forced_scale, classify_quotient, objecthood_periodic_table) contrast forced discrete structure with this free torsor. No used_by edges yet; the lemma is a registry tag rather than a computational stepping stone. It closes the scaffolding question of whether discrete recognition alone pins the unit: it does not.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.