rsField_extend_stays_countable
plain-language theorem explainer
Adjoining any countable set of real constants to the named RS constants still yields a countable subfield of ℝ. Foundation work that treats the RS working field as a proper countable subset of the continuum cites this. The proof is a one-line application of countable subfield closure to the union of the finite RS constant set with the adjoined family.
Claim. If $s \subseteq \mathbb{R}$ is countable, then the subfield of $\mathbb{R}$ generated by $\{\varphi, \pi, e, \alpha^{-1}\} \cup s$ is a countable subset of $\mathbb{R}$.
background
The Primitive Recognition Calculus minimal-field module isolates the smallest subfield of $\mathbb{R}$ that can carry RS arithmetic. The named constant set is $\mathrm{rsConstants} = {\varphi, \pi, e, \alpha^{-1}}$, with $\varphi$ the golden ratio forced at T6 and $\alpha^{-1}$ the fine-structure reciprocal in the RS band. That set is finite, hence countable.
The RS field itself is the subfield closure of those constants inside $\mathbb{R}$. Subfield closure of a countable set of reals remains countable: every element is a rational expression in finitely many generators, and the set of finite words over a countable alphabet is countable. The local claim extends that fact from the fixed constant set to an arbitrary countable enlargement.
Upstream, rsConstants_countable records countability of the base set (via finiteness), and subfield_closure_countable_of_countable is the general closure lemma used here.
proof idea
One-line term proof. Form the union $\mathrm{rsConstants} \cup s$; countability of the union follows from rsConstants_countable and the hypothesis that $s$ is countable. Feed that countable set into subfield_closure_countable_of_countable, which returns countability of the subfield closure as a subset of $\mathbb{R}$.
why it matters
Item 1 of the PRC minimal-field programme, sharpened: the working RS field stays a proper countable subset of $\mathbb{R}$ even after adjoining any further countable family of named constants. The construction therefore never needs the continuum, no matter how many constants the framework eventually names (ladder rungs, eight-tick integers, dimension $D=3$, additional derived scalars).
That underwrites the claim that RS physics lives on a countable $\varphi$-ladder arithmetic inside a countable field, not on a continuum-sized transcendental extension. No downstream theorems currently depend on this lemma in the graph, so it is presently a leaf that closes the countable-extension clause of the minimal-field story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.