costLambda_single_point_calibration
plain-language theorem explainer
Agreement of two positive-scale native costs at a single ratio x₀ > 1 forces the scales equal. Anyone citing the residual one-real gauge freedom of the four-law cost family needs this: the torsor is pinned by one measurement, not pointwise identity of functions. The proof clears denominators to (a−b)(ab−1)=0 with a,b>1, discards ab=1, then uses strict monotonicity of t ↦ x₀^t.
Claim. Let $x_0,\ell,m\in\mathbb{R}$ with $x_0>1$ and $\ell,m>0$. Write $F_\lambda(x)=\frac{x^\lambda+x^{-\lambda}}{2}-1$. If $F_\ell(x_0)=F_m(x_0)$, then $\ell=m$.
background
In the Primitive Recognition Calculus cost layer, the native one-parameter family is $F_\lambda(x)=\mathrm{costLambda},\lambda,x$, the J-cost of the powered ratio: essentially $J(x^\lambda)$ with $J(x)=(x+x^{-1})/2-1$. The Recognition Composition Law and reciprocal/normalization axioms are satisfied by every $F_\lambda$ for $\lambda>0$; algebra therefore forces the form, not a unique function.
The residual freedom is a multiplicative-automorphism gauge: $x\mapsto x^\lambda$ on $\mathbb{R}{>0}$. Full injectivity of $\lambda\mapsto F\lambda$ needs agreement everywhere (or equal log-curvature). The local setting of this module is the honest stratification of that joint: form forced, gauge orbit identified, calibration selecting $J$ inside the family.
Upstream, $J$ itself is the RS recognition cost of a positive ratio, and the functional-equation package records that the law of logic forces $J$ once calibration is imposed. This lemma isolates the single-point half of the gauge story.
proof idea
Positivity and strict super-unity of the powers are immediate: $x_0>1$ and $\ell,m>0$ give $a:=x_0^\ell>1$ and $b:=x_0^m>1$. Unfolding $\mathrm{costLambda}$ and rewriting negative powers turns the hypothesis into $a+a^{-1}=b+b^{-1}$.
Clear denominators by multiplying through by $ab$: the identity expands to a cubic relation rearranged by linear_combination into $(a-b)(ab-1)=0$. The factor $ab-1$ cannot vanish ($a,b>1$), so $a=b$. Strict monotonicity of $t\mapsto x_0^t$ for base $>1$ (Real.rpow_le_rpow_left_iff) yields both $\ell\le m$ and $m\le\ell$.
why it matters
Operationally this is the load-bearing gauge pin: the family ${F_\lambda:\lambda>0}$ is a torsor under multiplicative automorphisms, so fixing the gauge costs exactly one real degree of freedom, and that degree is a single distinction-ratio measurement $x_0\neq 1$. Downstream, prc_four_law_completeness identifies every positive-curvature four-law solution with some $F_c$, and prc_cost_freedom_is_one_real upgrades existence to unique existence; both rest on single-point (or equivalent) injectivity to kill residual redundancy.
In the framework landmarks this sits at the T5 J-uniqueness joint: RCL plus reciprocal/normalization force the cosh-log form up to scale, while calibration $\lambda=1$ selects $J$ itself. The recognition quantum, read through $\delta$, is precisely this one real datum. No further structure is required once the value at one $x_0>1$ is supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.