costLambda_one_eq_J
plain-language theorem explainer
For every positive real x, cosh(log x) − 1 equals (x + x⁻¹)/2 − 1. This is the elementary identity that identifies the unit-curvature member of the PRC cost-gauge family with the classical J-cost. Anyone citing T5 J-uniqueness or the c = 1 calibration of costLambda needs it. The proof is a three-rewrite expansion of cosh via exponentials and exp(log x) = x.
Claim. For every real $x > 0$, $\cosh(\log x) - 1 = \frac{1}{2}\bigl(x + x^{-1}\bigr) - 1$.
background
Recognition Science forces a unique cost functional J on positive ratios, classically written $J(x) = \frac12(x + x^{-1}) - 1$ and equivalently $J(x) = \cosh(\log x) - 1$ (forcing-chain T5). In the Primitive Recognition Calculus calibration layer, the discrete $\delta$-carrier leaves a one-parameter continuum gauge of cost forms whose only invariant is the log-curvature $c^2$ at the unit; the condition "curvature $= 1$" is exactly the selection of J.
The family is realized by a map costLambda parameterized by a positive real $c$. The present identity is the pure real-analysis step that says the $c = 1$ slice coincides with the two classical expressions for J. Upstream cost definitions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen weighted sums) all ultimately land on this same functional once the gauge is fixed.
proof idea
Term-mode rewrite proof. Expand $\cosh$ by its exponential definition, replace $e^{-\log x}$ by the reciprocal via Real.exp_neg, and cancel $e^{\log x} = x$ with the positivity hypothesis via Real.exp_log. The two sides become identical rational expressions in $x$ and $x^{-1}$. No Recognition-specific lemmas are required; the argument is pure real analysis.
why it matters
This identity is the bridge from the continuum gauge picture to the named J-cost used everywhere in the monolith. Downstream, costLambda_one_eq_Jcost rewrites costLambda 1 x into Cost.Jcost x by applying this lemma after the cosh form of costLambda. That step closes Item 2 of the PRC calibration target: the $\delta$-forced cost leaves a faithful one-parameter gauge, and curvature $= 1$ selects J.
In the broader framework it is the concrete realization of T5 J-uniqueness in multiplicative coordinates, and it underwrites every later citation that treats $J(x) = \cosh(\log x) - 1$ and $J(x) = \frac12(x+x^{-1})-1$ as interchangeable. Without it the calibration-independence theorems cannot name the unit member as the standard cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.