costLambda_injective
plain-language theorem explainer
Distinct positive scale parameters yield distinct continuum cost functions: pointwise equality of the two gauge-family members forces the exponents to coincide. Anyone treating the admissible-cost family as a torsor under multiplicative reparameterization, or arguing that calibration removes exactly one real degree of freedom, cites this freeness half. The proof equates log-coordinate curvatures at the unit via the calibration identity, obtains equal squares of the exponents, and discards the negative root by positivity.
Claim. Let $\ell, m > 0$. If the gauge-family cost functions satisfy $F_\ell(x) = F_m(x)$ for every real $x$, then $\ell = m$.
background
In the Primitive Recognition Calculus, admissible continuum costs form a one-parameter family $F_\lambda$ indexed by a positive real scale $\lambda$. The declaration costLambda is that family: each positive exponent produces a cost on the line (equivalently, on positive distinction ratios after exponential change of coordinate).
The log-coordinate reparametrization $G_F(t) = F(e^t)$ turns multiplicative structure into additive structure. The calibration identity records that the curvature of $G_{F_\lambda}$ at the unit equals $\lambda^2$. Equal functions therefore have equal unit curvatures, which is the algebraic lever used below.
The companion transitivity result says every admissible cost is some $F_\lambda$. Freeness (this theorem) plus transitivity make ${F_\lambda:\lambda>0}$ a torsor under the multiplicative gauge group: the action is free and transitive, so fixing the calibration unit $\lambda=1$ removes exactly one real degree of freedom and singles out the canonical $J$-cost.
proof idea
Pointwise equality of $F_\ell$ and $F_m$ implies equality of their log-coordinate transforms $G$, by function extensionality and the definition $G_F(t)=F(e^t)$. The calibration identity then supplies unit curvature $\ell^2$ on the left and $m^2$ on the right, so $\ell^2=m^2$. Factor as $(\ell-m)(\ell+m)=0$. The sum-zero branch contradicts $\ell,m>0$; the remaining branch is $\ell=m$. The argument is a short tactic script: rewrite through calibration, linear combination to factor, then mul_eq_zero with two linarith discharges.
why it matters
This is the freeness half of the native-cost gauge torsor. Downstream, the continuum gauge orbit is packaged as a set of functions, and its uncountability theorem invokes this injectivity together with uncountability of the positive reals: what calibration collapses is not a discrete list of impostors. Four-law completeness then identifies the positive-curvature solution set of the four algebraic laws exactly with the gauge orbit ${F_c:c>0}$, so after the laws the only residual freedom is the one real calibration datum. In the Recognition Science forcing story this underwrites that $J$ is singled out once unit curvature is fixed, with no algebraically preferred member among the continuum of admissible costs before calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.