costLambda
plain-language theorem explainer
Defines the one-parameter cost gauge family F_c(x) = (x^c + x^{-c})/2 - 1 on the reals, with real powers. The c = 1 member is the Recognition cost J. Downstream uniqueness and calibration-independence theorems cite this family to show that cost laws alone leave a free scale unit. The body is a direct closed-form definition via Real.rpow.
Claim. For real parameters $c$ and $x$, define the multiplicative cost gauge $F_c(x) := \frac{1}{2}\bigl(x^{c} + x^{-c}\bigr) - 1$, using real exponentiation. When $c = 1$, this recovers the standard Recognition cost $J(x) = \frac{x + x^{-1}}{2} - 1$.
background
In Recognition Science the cost functional is forced by the Recognition Composition Law (RCL) together with reciprocity, normalization, and continuity; the unique calibrated solution is $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$ (forcing step T5). Before calibration is imposed, a residual one-parameter family remains.
This module works in the Primitive Recognition Calculus calibration-independence layer. The family is written in multiplicative coordinates with real powers; an equivalent additive (log-coordinate) form $\cosh(c\cdot\log x) - 1$ is used in the calibration-target development. A parallel definition already appears in the native-cost uniqueness module as the full one-parameter family $F_\lambda$.
The local goal is to exhibit that every positive curvature parameter $c$ yields a bona fide cost satisfying the non-calibration hypotheses, so that only the unit-of-scale choice pins $J$.
proof idea
Pure definition: the right-hand side is the closed form $(x^c + x^{-c})/2 - 1$ via Real.rpow. No proof obligations. Immediate companion lemmas rewrite it as $\cosh(c\log x)-1$ on $(0,\infty)$, check continuity, injectivity in $c$, the cosh-add (RCL) identity, and membership in the cost-requirements class.
why it matters
This family is the concrete witness that calibration is logically independent of the rest of the cost laws. It feeds the headline results in this module: that every gauge member satisfies reciprocity, normalization, the RCL composition law, and continuity on the positives; that the family is faithful (distinct positive $c$ give distinct functions); that $c=1$ is exactly $J$; and therefore that calibration is the only hypothesis of the uniqueness theorem that pins $J$.
In the broader forcing chain this sits under T5 (J-uniqueness): the RCL and related axioms force the functional shape up to a scale unit, and the calibration condition $\delta$-fixes that unit to $c=1$. Downstream lemmas such as the cosh-add identity for each member and the continuous-on-$(0,\infty)$ statement are the technical steps that make the independence argument airtight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.