costLambda
plain-language theorem explainer
Defines the one-parameter cost family F_λ(x)=(x^λ+x^{-λ})/2−1 on the reals via real powers. The λ=1 member is the standard J-cost; other positive λ give distinct continuous reciprocal costs that still obey the Recognition Composition Law and normalization. Anyone arguing uniqueness of J, or the logical independence of calibration, cites this family. The body is a direct closed-form definition, not a derived construction.
Claim. For real parameters $\lambda$ and $x$, define $F_\lambda(x) := \frac{x^\lambda + x^{-\lambda}}{2} - 1$. When $\lambda = 1$ this is the J-cost $J(x) = \frac{x+x^{-1}}{2}-1$; when $\lambda = 2$ it is the distinct double-exponent member of the same family.
background
Recognition Science pins the cost of a positive ratio $x$ by a functional equation (the Recognition Composition Law, RCL): $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, together with reciprocity $J(x)=J(x^{-1})$, normalization $J(1)=0$, continuity on $(0,\infty)$, and a curvature calibration at the identity. The uniqueness theorem law_of_logic_forces_jcost states that these axioms force $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$).
The present definition isolates the residual freedom once calibration is dropped. Replacing the unit exponent by a free real $\lambda$ yields $F_\lambda(x)=(x^\lambda+x^{-\lambda})/2-1$. On positives this coincides with $\cosh(\lambda\log x)-1$, so every member inherits the cosh-addition identity that encodes RCL. The module sits in Primitive Recognition Calculus and feeds the calibration-independence development: the algebra alone cannot prefer $\lambda=1$ over any other positive scale.
proof idea
Pure definition: the right-hand side is written with real exponentiation and arithmetic. No lemmas are applied and no tactics run. Downstream proofs rewrite members into cosh-log form (costLambda_eq_cosh), then discharge continuity, injectivity in $\lambda$, the cosh-add identity, and the calibration criterion $G''(0)=\lambda^2$ by elementary real analysis on that closed form.
why it matters
This family is the concrete witness that calibration is the only hypothesis of the Law-of-Logic uniqueness theorem that pins $J$. Downstream, calibration_is_the_only_hypothesis_pinning_J shows every $F_\lambda$ satisfies reciprocity, normalization, RCL, and continuity, while calibration holds iff $\lambda=1$. The companion calibration_unit_not_forced_by_cost_laws records that the cost-requirement package is satisfied by more than one member (explicitly $\lambda=1$ versus $\lambda=2$).
In the forcing chain this is the precise obstruction before T5 J-uniqueness: without a $\delta$-native curvature fixing $\lambda=1$, the continuous solution set of RCL is the whole gauge orbit ${F_\lambda:\lambda>0}$. The forward program is therefore either to derive $\lambda=1$ from native curvature or to accept that $\delta$ forces $J$ only up to cost scale. The definition is reused throughout PRCCalibrationIndependence (continuity, injectivity, cosh identities, calibrated-iff statements).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.