costLambda_isNormalized
plain-language theorem explainer
Every member of the one-parameter cost family F_c(x) = ½(x^c + x^{-c}) − 1 is normalized: F_c(1) = 0. Anyone citing the uniqueness argument that only calibration pins J needs this unit law for the whole gauge orbit. The proof is a one-line wrapper of the already-proved unit identity.
Claim. For every real parameter $c$, the map $x \mapsto \tfrac12\bigl(x^c + x^{-c}\bigr) - 1$ satisfies the normalization condition $F(1) = 0$.
background
In the Primitive Recognition Calculus calibration-independence module, the cost gauge family is
$$\mathrm{costLambda},c,x = \tfrac12\bigl(x^c + x^{-c}\bigr) - 1$$
(with real powers). The member $c = 1$ is the standard J-cost $J(x) = \tfrac12(x + x^{-1}) - 1$, equivalently $\cosh(\log x) - 1$. On the positives the same family is written $\cosh(c,\log x) - 1$.
Normalization, in the Cost.FunctionalEquation sense used here, is simply the unit law $F(1) = 0$. It is one of the non-calibration hypotheses in the uniqueness package for J (alongside reciprocity, the Recognition Composition Law, and continuity on $(0,\infty)$). The sibling theorem costLambda_unit0 already records $F_c(1) = 0$ for every $c$, via the cosh form and $\cosh 0 = 1$.
proof idea
One-line wrapper: the goal is exactly IsNormalized (fun x => costLambda c x), i.e. costLambda c 1 = 0, which is the statement of costLambda_unit0 c. No extra algebra is performed at this site.
why it matters
This lemma feeds calibration_is_the_only_hypothesis_pinning_J, the airtight Item-2 claim that calibration is the sole hypothesis of the J-uniqueness theorem that selects $c = 1$. That parent theorem packages reciprocity, normalization, the RCL composition law, and continuity on the positives for every gauge member, then shows calibration holds iff $c = 1$ and that the family has genuinely distinct members. Hence the four non-calibration laws are satisfied by a continuum of costs and cannot force J alone.
In the Recognition forcing chain this sits under T5 (J-uniqueness): the functional equation and structural laws determine the shape of the cost up to the scale choice fixed by calibration (Condition 1.2 / $G''(0) = 1$). The present fact is the normalization half of that structural package for the full $\lambda$-family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.