subfield_closure_countable_of_countable
plain-language theorem explainer
Any subfield of the reals generated by a countable set remains countable. Recognition Science cites this whenever it adjoins countably many named constants (φ, π, e, ladder values) and must stay inside a countable working field. The proof is a short cardinal comparison: Mathlib bounds the cardinality of a subfield closure by ℵ₀ whenever the generators are at most countable.
Claim. If $s \subseteq \mathbb{R}$ is countable, then the subfield of $\mathbb{R}$ generated by $s$ is countable as a set.
background
In the Primitive Recognition Calculus minimal-field module, the working number system is the subfield of $\mathbb{R}$ generated by a small list of RS constants (φ, π, e, and related weights). Countability of that field is the structural guarantee that every named constant and every finite expression built from them still lives in a countable set, never forcing the continuum.
Subfield closure is the smallest subfield containing a given generating set $s$. The present lemma is the general countable-generator case. Its finite-generator specialization is the form used for the fixed RS constant list. The doc-comment frames it as the field-level analogue of algebraic-closure countability, extended to arbitrary (including transcendental) generators: adjoining countably many reals to $\mathbb{Q}$ never escapes countability.
The argument is pure Mathlib cardinal arithmetic on Subfield.closure; no Recognition-specific axioms enter.
proof idea
Convert the hypothesis s.Countable into the cardinal inequality $# s \le \aleph_0$ via Cardinal.mk_le_aleph0_iff and Set.countable_coe_iff. Apply Mathlib's Subfield.cardinalMk_closure_le_max, which bounds $#(\mathrm{Subfield.closure}, s)$ by $\max(# s, \aleph_0)$. With $# s \le \aleph_0$ this max is $\aleph_0$, so the closure has cardinality at most $\aleph_0$. Convert back to Set.Countable on the underlying set of the subfield. No induction or explicit enumeration is written by hand.
why it matters
This is the load-bearing countability fact for the RS minimal field. Downstream, subfield_closure_countable_of_finite is the one-line finite special case used for the fixed RS constant list; rsField_extend_stays_countable uses the general form to show that adjoining any further countable family of constants keeps the field countable ("the construction never requires the continuum no matter how many constants RS eventually names"). genField_countable applies it to the range of a sequence of generators so that generable reals stay countable. S_countable in the exp/log field stages relies on the finite form at stage zero and inherits the same closure discipline.
In the broader framework this underwrites the claim that the φ-ladder, eight-tick integer outputs, and named constants (c, ħ, G, α-band quantities) can all live inside one countable subfield of $\mathbb{R}$. It does not itself force φ or the octave; it only keeps the arithmetic carrier countable once those constants are named.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.