costLambda_injOn_pos
plain-language theorem explainer
If two positive scale exponents induce the same cost on (0,∞), they are equal: the residual freedom in the forced cost family is exactly one positive real. Anyone classifying monotone, reciprocal, normalized composition-law costs cites this injectivity. The argument evaluates at x=2, rewrites as a cosh identity, and cancels log 2 via strict monotonicity of cosh on [0,∞); no completeness is used.
Claim. Let $\ell,\ell'>0$. If $\tfrac12(x^\ell+x^{-\ell})-1=\tfrac12(x^{\ell'}+x^{-\ell'})-1$ for every $x>0$, then $\ell=\ell'$.
background
In the primitive recognition calculus the δ-forced cost gauge is the one-parameter family $\mathrm{cost}_\ell(x)=\tfrac12(x^\ell+x^{-\ell})-1$ on $x>0$, with real exponents via $r$-powers. The member $\ell=1$ is the classical $J$-cost $J(x)=\tfrac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$.
The Recognition Composition Law and reciprocal symmetry force costs into this shape once monotonicity of the log-transform is assumed; the remaining free datum is the positive scale $\ell$. The present module closes the uniqueness half of that classification without topological completeness.
Upstream, the family is defined exactly as above in the calibration-independence development; the $c=1$ case recovers $J$ from the T5 uniqueness landmark in the forcing chain.
proof idea
Specialize the pointwise equality to $x=2$. Unfolding the definition yields $\tfrac12(2^\ell+2^{-\ell})=\tfrac12(2^{\ell'}+2^{-\ell'})$. Rewrite each side via $2^a=\exp(a\log 2)$ as $\cosh(\log 2\cdot\ell)$ and $\cosh(\log 2\cdot\ell')$. Both arguments $\log 2\cdot\ell$ and $\log 2\cdot\ell'$ lie in $[0,\infty)$ by positivity. Strict monotonicity of $\cosh$ on that ray gives $\log 2\cdot\ell=\log 2\cdot\ell'$; cancel the positive factor $\log 2$.
why it matters
Doc-comment §9 capstone: residual freedom after the composition law, reciprocity, normalization, and monotonicity is exactly one positive real, faithfully parameterized and irreducible by order-only data. Downstream, law_of_logic_forces_jcost_monotone uses this injectivity (with the companion surjectivity that every monotone solution is some scale member) to force $F=J$ under unit calibration, the completeness-free analogue of the classical continuity-based forcing. The successor-increment limit theorem likewise needs unique recovery of the calibration invariant $c^2$ from the δ-act ladder across the whole family. In the RS forcing chain this pins the T5 $J$-uniqueness residual: scale is genuine, not an artifact of a loose argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.