costLambda_inj
plain-language theorem explainer
Distinct positive curvature parameters yield genuinely distinct members of the costLambda gauge family. Calibration-independence results cite this to show residual freedom is exactly one real parameter. The proof transports function equality along x = exp t and invokes injectivity of the log-coordinate family clog.
Claim. Let $c,d>0$. If the maps $x\mapsto \Lambda_c(x)$ and $x\mapsto \Lambda_d(x)$ agree as functions $\mathbb{R}\to\mathbb{R}$, then $c=d$. Here $\Lambda_c$ is the one-parameter gauge family of recognition costs (with $\Lambda_1=J$).
background
In the Primitive Recognition Calculus, recognition costs are maps $F:\mathbb{R}_{>0}\to\mathbb{R}$ obeying at least the bare CostRequirements: reciprocity $F(x)=F(x^{-1})$ and normalization $F(1)=0$. The classical J-cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, forced uniquely only after an extra calibration that pins the unit of scale.
The module studies a one-parameter gauge family costLambda (curvature parameter $c>0$) whose $c=1$ member recovers $J$. Sibling lemmas record the cosh form costLambda_eq_cosh, the unit law, symmetry, and that every member satisfies CostRequirements. Faithfulness of the family means distinct $c$ give distinct functions, so residual gauge freedom is exactly one real.
Upstream, CostRequirements is the minimal symmetric-plus-unit package; the fuller uniqueness theorem law_of_logic_forces_jcost adds reciprocity structure, the Recognition Composition Law, continuity, and calibration.
proof idea
Term-mode reduction to clog injectivity. Apply clog_inj on the positive parameters $c,d$. It remains to show the log-coordinate curves agree: funext over $t\in\mathbb{R}$. Evaluate the assumed function equality at $x=e^t$ (positive by exp_pos), rewrite both sides via costLambda_eq_cosh, cancel $\log\circ\exp$, and obtain pointwise equality of the clog family, which clog_inj converts into $c=d$.
why it matters
This is the faithfulness half of Item 2 in PRCCalibrationIndependence: the negative direction showing cost laws do not force the unit of scale. Downstream, calibration_unit_not_forced_by_cost_laws packages it with "every member is a bona fide cost", "$c=1$ is $J$", and an explicit pair of distinct members, so CostRequirements alone cannot single out $J$.
The tighter parent calibration_is_the_only_hypothesis_pinning_J lifts the same injectivity to the full non-calibration hypothesis set of law_of_logic_forces_jcost (reciprocal cost, normalization, RCL composition, continuity on positives). Calibration holds iff $c=1$; hence among T5-style J-uniqueness hypotheses, only calibration pins the unit. That isolates the irreducible gauge choice in the forcing chain before phi, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.