costLambda_continuousOn
plain-language theorem explainer
For every real scale parameter c, the multiplicative cost gauge F_c(x)=(x^c+x^{-c})/2-1 is continuous on (0,∞). Cited by anyone showing that continuity cannot select the recognition cost J among its one-parameter family. Proof rewrites to the cosh-log form and composes standard continuous maps on the positives.
Claim. For every real number $c$, the map $x \mapsto \tfrac12(x^{c}+x^{-c})-1$ is continuous on $(0,\infty)$.
background
Recognition Science measures the cost of a positive ratio by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. The forcing chain (T5) pins this functional form once a calibration (unit of scale) is chosen, together with reciprocity, normalization, the Recognition Composition Law, and continuity on the positives.
This module studies the one-parameter gauge family $F_c(x)=\tfrac12(x^c+x^{-c})-1$, written costLambda c x, whose $c=1$ member is exactly $J$. On $(0,\infty)$ the multiplicative form coincides with the additive log-coordinate form $\cosh(c\cdot\log x)-1$ (the identity costLambda_eq_cosh). The local goal is to check which uniqueness hypotheses hold for every $c$, so that only calibration can force $c=1$.
proof idea
Reduce via costLambda_eq_cosh so the claim is continuity of $x\mapsto\cosh(c\cdot\log x)-1$ on $(0,\infty)$. Real log is continuous on the positive reals; multiply by the constant $c$; compose with continuous cosh; subtract the constant $1$. Finish by pointwise congruence with the cosh identity on Set.Ioi 0.
why it matters
Direct input to calibration_is_the_only_hypothesis_pinning_J, the headline result that calibration is the only uniqueness hypothesis pinning $J$. That theorem shows every family member satisfies reciprocity, normalization, the RCL composition law, and continuity on the positives; calibration holds iff $c=1$; and distinct $c$ give genuinely distinct costs. Continuity therefore does not discriminate inside the family.
In framework terms this closes the continuity half of the T5 argument: the law set (including RCL) forces the cosh shape up to a free scale exponent, and only the calibration choice selects the native $J$. Without this lemma the non-calibration hypothesis bundle could not be verified uniformly for all $c$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.