carrierValues_countable
plain-language theorem explainer
The set of real numbers obtained by evaluating finite F_RS carrier terms is countable. Anyone arguing that the Recognition carrier cannot smuggle continuum many constants will cite this. The proof is a one-line monotonicity transfer: the carrier range sits inside the countable RS constant field, so it is countable too.
Claim. The set of all real values of finite F_RS carrier expressions is a countable subset of $\mathbb{R}$. Equivalently, $\operatorname{range}(\mathrm{eval})\subseteq\mathbb{R}$ is countable.
background
In the Primitive Recognition Calculus, the F_RS carrier is an explicit finite-term syntax over a fixed inventory (rationals together with $\varphi$, $\pi$, $e$, and $\alpha^{-1}$). Evaluation sends each term to a real; the image of that map is the carrier value set.
That image is already known to lie inside the RS constant field: every evaluated term lands in the subfield of $\mathbb{R}$ generated by the finite RS constant inventory. Upstream, that RS field is countable because it is the subfield closure of a finite set of reals.
The same countability motif appears for registry values in the certified analytic protocols layer: finite expression trees over countable labels yield only countably many values, which is the fact that blocks continuum smuggling into the framework's computable carrier.
proof idea
One-line term proof. Apply set-monotonicity of countability to the inclusion of the carrier value set in the RS constant field, using the already-proved countability of that field. No new enumeration is built; the subset inherits countability from the ambient countable field.
why it matters
This lemma is the countability half of the Phase 3 F_RS carrier headline: the framework computes on finite generation over a fixed inventory, not on the uncountable continuum. Downstream, properness of the carrier value set relative to $\mathbb{R}$ is immediate: if the carrier filled all of $\mathbb{R}$, countability would contradict the uncountability of the reals.
Together with soundness (every term evaluates into the RS field), inventory coverage ($\varphi$, $\pi$, $e$, $\alpha^{-1}$, and rationals are terms), and protocol display into the $\mathbb{R}_\delta$ interface, this closes the claim that the carrier is an explicit finite-description syntax. It is the set-theoretic guardrail that keeps Recognition constants from being continuum-many free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.