costLambda_isReciprocalCost

In the Primitive Recognition Calculus, costs are real functions on the positive reals. A reciprocal cost (Definition 2.1) is any $F$ with $F(x)=F(1/x)$ for all $x>0$; normalization $F(1)=0$ is a separate axiom.

The one-parameter family studied here is the $\delta$-forced gauge $F_c(x)=\frac12(x^c+x^{-c})-1$, written via real powers. The member $c=1$ is the standard $J$-cost $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. On positives the multiplicative form coincides with the additive log-coordinate form used in the calibration target module.

Reciprocal symmetry for every member was already established: $F_c(x)=F_c(x^{-1})$ follows by rewriting as $\cosh(c\log x)-1$ and using $\log(x^{-1})=-\log x$ together with evenness of $\cosh$.

One-line term proof. Unfold the reciprocal-cost predicate and apply the existing symmetry theorem for the same family: for each $x>0$, the equality $F_c(x)=F_c(x^{-1})$ is exactly costLambda_symm. No further algebra is needed.

Feeds the headline independence theorem in this module: calibration is the only hypothesis of the uniqueness theorem that pins $J$. That result shows every gauge member $F_c$ satisfies the full non-calibration package (reciprocity, normalization, the Recognition Composition Law, and continuity on the positives), while calibration holds iff $c=1$, and distinct $c$ give genuinely distinct costs. Reciprocity is the first conjunct of that package, so this lemma is the reciprocity leg of the argument.

In the broader forcing chain this supports T5 ($J$-uniqueness): the RCL and related cost laws alone do not select the unit of scale; the calibration choice is logically independent of the rest of the law set. Without a clean reciprocity certificate for the whole family, the "only calibration pins $J$" claim would not typecheck.