continuumScaleFamily
plain-language theorem explainer
The continuum gauge orbit is the set of all real functions F_λ(x) = ½(x^λ + x^{-λ}) − 1 for λ > 0. Anyone comparing the size of the calibration-collapsed family to a discrete carrier cites this set. It is a pure set-comprehension definition over the one-parameter cost family, not a proved claim.
Claim. Define the continuum scale family as the set of all maps $F:\mathbb{R}\to\mathbb{R}$ for which there exists $\lambda>0$ with $F(x)=\tfrac12(x^\lambda+x^{-\lambda})-1$ for every $x$ (equivalently $F=\cosh(\lambda\log\,\cdot\,)-1$ on the positive reals).
background
In the primitive recognition calculus the native cost on positive ratios is forced (up to calibration) to the J-cost $J(x)=\tfrac12(x+x^{-1})-1$, also written $\cosh(\log x)-1$. The one-parameter family $F_\lambda(x)=\tfrac12(x^\lambda+x^{-\lambda})-1$ is the continuum gauge orbit of that cost: each positive exponent $\lambda$ is a pure scale choice on the multiplicative line, and $\lambda=1$ recovers $J$.
Upstream, costLambda packages exactly this family (real powers via Real.rpow). Injectivity of the parameterization is already proved: distinct positive exponents yield distinct functions, because log-coordinate curvature at the unit equals $\lambda^2$. The present module records structural ledger facts about that orbit after calibration independence has been set up.
Locally the object is only the set of those functions as a subset of $\mathbb{R}\to\mathbb{R}$. No minimality or uniqueness is asserted here; those live in the uniqueness and minimality-certificate modules.
proof idea
Definition only: the body is the set comprehension ${F\mid \exists,\lambda\in\mathbb{R},; 0<\lambda\land F=\mathrm{costLambda},\lambda}$. No tactics, no lemmas applied at this site. Downstream cardinality arguments will invoke injectivity of the map $\lambda\mapsto F_\lambda$ separately.
why it matters
This set is the quantitative carrier for the continuum half of the calibration comparison. The immediate parent is the theorem that the continuum gauge orbit is uncountable: injectivity of the positive-exponent parameterization plus uncountability of $(0,\infty)$ shows that what the calibration axiom collapses on the line is not a discrete list of impostors.
In the Recognition forcing picture this sits under T5 J-uniqueness and the Recognition Composition Law: the native cost is unique up to the irreducible scale choice $\lambda$, and the size of that residual family is part of the ledger that separates continuum gauge freedom from discrete structure on the carrier. Stating the set explicitly (rather than leaving it as a remark) makes the cardinality half of that comparison a first-class object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.