costLambda_unit0
plain-language theorem explainer
For every real gauge parameter c, the multiplicative cost F_c satisfies F_c(1)=0. Cited when verifying that each member of the δ-forced cost family meets CostRequirements or IsNormalized. Proof rewrites to the cosh-log form, uses log 1 = 0, and evaluates cosh 0 − 1.
Claim. For every real number $c$, the cost gauge $F_c(x)=\frac12(x^c+x^{-c})-1$ obeys the unit law $F_c(1)=0$.
background
In the Primitive Recognition Calculus, recognition costs are real functions on the positives obeying symmetry, a unit law, and related structural axioms. The one-parameter family studied here is the δ-forced cost gauge in multiplicative coordinates: $F_c(x)=\frac12(x^c+x^{-c})-1$, with real powers via Real.rpow. The member $c=1$ is the classical J-cost $J(x)=\frac12(x+x^{-1})-1$ forced at T5.
On $(0,\infty)$ this coincides with the additive (log-coordinate) form $\cosh(c\cdot\log x)-1$ used by the calibration target module. The unit law $F(1)=0$ is one of the CostRequirements (and the normalization condition IsNormalized) that every bona fide recognition cost must satisfy; the present lemma discharges that obligation uniformly in $c$.
proof idea
Term-mode rewrite chain. Apply the identity that on positives $F_c(x)=\cosh(c\cdot\log x)-1$ at $x=1$ (using $1>0$). Then $\log 1=0$, so the argument is $c\cdot 0=0$, and $\cosh 0=1$. Subtracting 1 yields 0 after a norm_num cleanup. No case split on $c$ is needed.
why it matters
Feeds two parent results in the same module: costLambda_isCostRequirements (every positive-$c$ member is a bona fide recognition cost, with unit0 supplied by this lemma) and costLambda_isNormalized (IsNormalized is exactly the unit law). Together they underwrite the calibration-independence story: the cost laws alone do not force the unit of the gauge; every $F_c$ is structurally a cost, so the calibration scale remains an irreducible choice. Landmark contact is T5 J-uniqueness and the Recognition Composition Law background for J; here the whole cosh family inherits the unit axiom that J satisfies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.