rsConstants_countable
plain-language theorem explainer
The named Recognition Science constants form a countable subset of the reals. Anyone building the minimal RS constant field or extending it by further named constants cites this. The proof is a one-line appeal to finiteness of that four-element set.
Claim. The set $\{\varphi, \pi, e, \alpha^{-1}\} \subset \mathbb{R}$ is countable.
background
In the Primitive Recognition Calculus minimal-field development, the named RS constants are collected as a single set of reals: the golden ratio $\varphi$, $\pi$, Euler's $e$, and the inverse fine-structure constant $\alpha^{-1}$. The minimal RS field is then the subfield of $\mathbb{R}$ generated by this set; it automatically contains $\mathbb{Q}$ as prime field.
Countability of the generating set is the first step toward showing that the generated field itself is countable, so the working RS arithmetic never needs the continuum. An upstream sibling already records that the same set is finite (four explicit singletons inserted in succession).
proof idea
One-line term proof: apply the Mathlib fact that every finite set is countable to the already-proved finiteness theorem for the named-constant set. No case analysis or unfolding is required at this step.
why it matters
This lemma is the countability half of the finite-generator package for the RS constant field. Downstream, rsField_extend_stays_countable uses it to show that adjoining any further countable family of constants keeps the subfield closure countable: "the construction never requires the continuum no matter how many constants RS eventually names."
In the broader framework this underwrites Item 1 of the minimal-field program: a countable carrier that still holds the $\varphi$-ladder, the eight-tick octave outputs, and the forced constants from the T0–T8 chain, without continuum cardinality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.