carrierValues_proper
plain-language theorem explainer
The FRS carrier value set is a proper subset of the reals: not every real arises as the evaluation of a finite carrier term. Anyone citing the Phase 3 FRS-carrier headline needs this properness clause. The proof is a one-step cardinality contradiction: the carrier values are countable, while ℝ is not.
Claim. The set of real numbers obtained by evaluating FRS carrier expressions is not equal to $\mathbb{R}$; equivalently, that set is a proper subset of the continuum.
background
In the Primitive Recognition Calculus, the FRS carrier is an explicit finite-description syntax whose terms evaluate to reals. The set carrierValues is defined as the range of that evaluation map: every element is the real denoted by some carrier expression built from a fixed inventory (rationals together with $\varphi$, $\pi$, $e$, and $\alpha^{-1}$).
A companion lemma records that this range is countable, because the syntax of expressions is countable and evaluation is a function out of it. Separately, classical cardinality supplies that $\mathbb{R}$ itself is uncountable.
The local module packages these facts toward the Phase 3 claim that the framework computes on a finitely generated carrier inside a countable subfield, not on the full continuum. Delta-real protocols sit nearby as the display interface that renders each carrier value as a nested rational-interval approximation.
proof idea
Assume for contradiction that the carrier value set equals $\mathbb{R}$. Substitute that equality into the already-proved countability of the carrier values. The resulting statement says $\mathbb{R}$ is countable, which is refuted by the standard Mathlib fact that the reals are uncountable. The argument is a pure cardinality reductio; no analytic estimates appear.
why it matters
This lemma is one conjunct of the Phase 3 headline frs_carrier: that theorem packages soundness into the minimal RS field, presence of the constant inventory, countability of term values, properness inside $\mathbb{R}$, and protocol display into the $\mathbb{R}_\delta$ interface. The properness clause is what blocks the misreading that the carrier is the whole continuum.
In Recognition Science terms, the framework's computational substrate is finite generation over a fixed inventory (the phi-ladder constants and companions), not an uncountable real line. Without properness, the "finite-description carrier" slogan would be empty. The result is pure set theory once countability is in hand; it does not itself force $\varphi$ or the eight-tick structure, but it seals the carrier side of the foundation stack that those later forcing steps sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.