clog_inj
plain-language theorem explainer
Distinct positive scale parameters yield distinct cost curves of the form cosh(c t) − 1. Anyone calibrating the Recognition cost unit or proving the residual gauge is a free (ℝ>0)-torsor cites this injectivity. The proof reads the second derivative at t = 0 (an invariant of the function) and uses positivity to recover c from c².
Claim. If $c,d > 0$ and the maps $t \mapsto \cosh(c t) - 1$ and $t \mapsto \cosh(d t) - 1$ agree as functions $\mathbb{R} \to \mathbb{R}$, then $c = d$.
background
In the Primitive Recognition Calculus calibration layer, the discrete δ-laws force the cost shape only up to a positive real scale. The residual family is written in log-coordinates as $f_c(t) = \cosh(c t) - 1$ for $c > 0$. The $c = 1$ member is exactly the classical J-cost after the change of variables $x = e^t$, since $J(x) = (x + x^{-1})/2 - 1 = \cosh(\log x) - 1$.
The local invariant that separates members is log-curvature: the second derivative of $f_c$ at the unit $t = 0$. Upstream, logCurvature records that this second derivative equals $c^2$. Because curvature is read from the function alone, equal cost curves must share the same $c^2$, and positivity upgrades that to $c = d$.
The module frames this as Item 2 of the calibration target: the unit is a continuum-side gauge parameter that the discrete carrier does not fix.
proof idea
Apply the upstream curvature identity twice: the second derivative of $t \mapsto \cosh(c t) - 1$ at $0$ is $c^2$, and likewise $d^2$ for $d$. Function equality rewrites the first identity into the second, so $c^2 = d^2$. Factor as $(c - d)(c + d) = 0$. From the product vanishing, either $c = d$ or $c = -d$; the hypotheses $c > 0$ and $d > 0$ kill the negative branch by linear arithmetic. The argument is pure real calculus plus positivity; no discrete structure is used.
why it matters
Faithfulness of the cost family is the freeness half of the residual gauge. Downstream, cost_freedom_is_one_real_torsor pairs this injectivity with transitivity of the positive-real action to exhibit the family as a principal homogeneous space under $(\mathbb{R}_{>0}, \cdot)$: exactly one real of freedom. The same fact is packaged in calibration_unit_is_a_gauge and lifted to the multiplicative cost family by costLambda_inj (transport along $x = e^t$).
It is also a conjunct in the Phase-4 headlines calibration_is_one_continuum_act and calibration_gap_closed_by_normalized_interface: discrete laws leave a faithful one-real torsor, while normalizing one-act curvature to 1 forces $c = 1$ and selects J. That is the honest RS calibration story relative to T5 J-uniqueness: J is the curvature-normalized member of a continuum gauge family the discrete side cannot pin down alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.