costLambda_one_eq_jcost
plain-language theorem explainer
On positive reals the native cost family at exponent one equals the classical recognition cost J(x)=(x+x^{-1})/2-1. Anyone fixing the unit calibration that singles J out of the multiplicative gauge orbit cites this identity. The proof is a short unfold-and-rewrite on real powers.
Claim. For every real $x>0$, the native cost family member at exponent $\lambda=1$ equals the recognition cost: $F_1(x)=J(x)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Recognition Science works with a one-parameter family of reciprocal costs on $\mathbb{R}{>0}$. The member at exponent $\lambda$ is the composition of the classical cost $J$ with the multiplicative automorphism $x\mapsto x^\lambda$, so schematically $F\lambda(x)=J(x^\lambda)=\frac{x^\lambda+x^{-\lambda}}{2}-1$. The classical cost itself is $J(x)=\frac{x+x^{-1}}{2}-1$ (also written $\cosh(\log x)-1$), the unique continuous solution of the Recognition Composition Law once unit curvature is fixed.
The surrounding module treats calibration as a gauge: the composition law is invariant along the whole orbit ${F_\lambda:\lambda>0}$ under $\mathrm{Aut}(\mathbb{R}_{>0},\times)$. Algebra alone therefore does not prefer any basepoint; the external unit choice $\lambda=1$ is what names $J$. Upstream definitions supply $J$ itself and the multiplicative structure of $J$-automorphisms used to state the orbit.
proof idea
Term-mode proof by definition chase. Unfold both costLambda and Cost.Jcost, then rewrite with the three real-power identities $x^1=x$, $x^{-1}=x^{-1}$ (via Real.rpow_neg from positivity), and again $x^1=x$. The two sides become identical expressions $\frac{x+x^{-1}}{2}-1$. No lemmas beyond Mathlib real-power facts are required.
why it matters
This is the unit-calibration anchor inside the PRC native-cost uniqueness development. Downstream, single-point calibration uses it to show one real evaluation $F_\lambda(x_0)=F_\mu(x_0)$ at any $x_0>1$ forces $\lambda=\mu$; the joint stratification packages it as the clause that calibration selects $J$; and the monotone headline capstone law_of_logic_forces_jcost_monotone routes through the same identification when concluding $F=J$ from reciprocity, normalization, composition, monotonicity of the log-transform, and unit curvature.
In the forcing chain this is the concrete $\lambda=1$ face of T5 $J$-uniqueness: the composition law admits a full scale family, the family is a single homogeneous Aut-orbit, and only the external unit picks $J$. Without this equality the gauge story has no named basepoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.