continuum_scale_family_uncountable
plain-language theorem explainer
The continuum gauge orbit of native costs is uncountable: distinct positive real exponents yield distinct cost functionals, so the family is as large as the positive reals. Anyone comparing the discrete carrier calibration to its continuum impostors cites this for the quantitative half of that comparison. The proof injects the positive reals into the family via costLambda, then injects the reals via exp, and contradicts uncountability of ℝ.
Claim. The continuum scale family (costs of the form $\mathrm{cost}_\lambda$ for $\lambda > 0$) is not a countable set. Equivalently, the continuum gauge orbit of reciprocal, normalized, composition-obeying costs on the line is uncountable.
background
In the Primitive Recognition Calculus native-cost ledger, admissible costs on the positive line are classified by a one-parameter scale family. Each positive real exponent $\lambda$ determines a cost functional $\mathrm{cost}_\lambda$; injectivity of this assignment means distinct exponents give genuinely different costs, not mere reparametrizations.
The surrounding module compares that continuum family to the discrete carrier forced by the calibration axiom. The doc-comment states the point directly: what calibration collapses on the line is not a discrete list of impostors. Size is the quantitative half of the comparison with the carrier.
Related structure in the ledger includes the reciprocal automorphism of the cost algebra and the J-cost composition law that forces the admissible shape. The continuum objects here are the monotone (not necessarily continuous) members of that class; a later remark in the file equates the monotone class exactly with the scale family.
proof idea
Proof by contradiction. Assume the continuum scale family is countable, so its underlying subtype is countable.
Build an injection from $(0,\infty)$ into the family by sending each positive $l$ to the pair $(\mathrm{cost}_l, \langle l,\ldots\rangle)$. Injectivity reduces to $\mathrm{costLambda_injective}$: equal costs force equal exponents. Countability then transfers to $(0,\infty)$.
Compose with the standard injection $\mathbb{R}\to(0,\infty)$ given by $x\mapsto e^x$ (injective by $\mathrm{Real.exp_injective}$). The composite makes $\mathbb{R}$ countable, contradicting $\mathrm{real_not_countable}$.
why it matters
This theorem supplies the cardinality half of the continuum-versus-carrier comparison in the PRC native-cost structural ledger. Downstream it feeds structuralStratificationCertificate_holds, which packages uniqueness, slimness, positivity, and gauge-inhabitation into the structural stratification certificate.
In Recognition Science terms, the forcing chain pins a unique J-cost shape (T5) and self-similar scale $\varphi$ (T6). On the continuum line, without discrete calibration, an uncountable gauge orbit of impostor costs remains. Stating uncountability formally prevents treating the collapsed family as a finite or countable nuisance list; the discrete carrier is doing real work against a continuum of alternatives.
The companion monotone-class identification (every reciprocal normalized composition-obeying monotone cost is some $\mathrm{cost}_\lambda$) makes the comparison honest: monotone against monotone, not monotone against continuous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.