costLambda_isCostRequirements
plain-language theorem explainer
For every real calibration parameter c, the gauge family member costLambda c satisfies the two recognition-cost axioms: reciprocal symmetry on the positives and vanishing at the unit. Anyone arguing that CostRequirements alone leave a residual scale free will cite this. The proof is a two-field structure constructor that plugs in the already-proved symmetry and unit lemmas.
Claim. For every real number $c$, the map $x \mapsto \tfrac12\bigl(x^{c}+x^{-c}\bigr)-1$ satisfies the recognition cost requirements: it is reciprocal-symmetric on $(0,\infty)$ and vanishes at $1$.
background
Recognition costs are maps $F:\mathbb{R}\to\mathbb{R}$ obeying two structural laws packaged as CostRequirements: reciprocal symmetry $F(x)=F(x^{-1})$ for $x>0$, and the unit law $F(1)=0$. The classical J-cost $J(x)=\tfrac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$) is the $c=1$ case of a one-parameter gauge family.
In this module the family is written multiplicatively as $\mathrm{costLambda},c,x=\tfrac12(x^{c}+x^{-c})-1$, with real powers via Real.rpow. On the positives it coincides with the additive form $\cosh(c\cdot\log x)-1$ used in the calibration target. Two prior lemmas already establish the axioms memberwise: the unit law holds for every $c$, and reciprocal symmetry holds for every $c$ on $(0,\infty)$ via the evenness of cosh after $\log(x^{-1})=-\log x$.
proof idea
Term-mode structure construction. The CostRequirements record has two fields. The symmetry field is discharged by applying costLambda_symm c at the positivity hypothesis; the unit field is discharged by costLambda_unit0 c. No further rewriting or case analysis is needed.
why it matters
This is the positive half of Item 2 in the PRC calibration-independence argument: every gauge member is a bona fide recognition cost. Downstream, calibration_unit_not_forced_by_cost_laws conjoins this universal statement with faithfulness of the family, the identification of the $c=1$ member with $J$, and an explicit pair of distinct members (e.g. $c=1$ and $c=2$) both satisfying the cost laws. That conjunction is the negative direction: the bare cost axioms do not force the unit of scale.
In the broader forcing chain this sits under T5 J-uniqueness. Uniqueness of $J$ requires more than CostRequirements alone (continuity plus the Recognition Composition Law / functional equation). The present lemma isolates exactly how much freedom survives when only the two structural axioms are imposed, clarifying why the full uniqueness theorem needs the stronger hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.