S_countable
plain-language theorem explainer
Every finite stage of the exp/log tower over {π, φ} is a countable subfield of ℝ. Anyone building the RS constant field or a closed observable framework cites this to keep the state space countable. The proof is induction on the stage index: finite generators at stage 0, then countable unions and images under exp/log plus subfield-closure countability at successors.
Claim. For every natural number $n$, the $n$-th stage $S(n)$ of the increasing chain of real subfields (starting from the subfield generated by $\{\pi,\varphi\}$ and iteratively adjoining images under $\exp$ and $\log$) is a countable subset of $\mathbb{R}$.
background
In the primitive recognition calculus, the RS constants live in a minimal real field closed under the field operations and under real exponential and logarithm. The seed set is $\mathrm{gens}={\pi,\varphi}$ (golden ratio); rationals come free as the prime field of any subfield of $\mathbb{R}$.
The stages $S:\mathbb{N}\to\mathrm{Subfield},\mathbb{R}$ form an increasing chain: $S(0)$ is the subfield closure of the generators, and $S(n+1)$ is one step that adjoins $\exp$ and $\log$ images of the current field and closes under the field operations again. The eventual exp/log-closed field is the directed union of these stages.
Upstream, subfield_closure_countable_of_finite and subfield_closure_countable_of_countable record that subfield generation never leaves the countable realm when the generators are finite or countable: "adjoining countably many reals to the rationals never escapes countability."
proof idea
Induction on the stage index $n$.
Base case $n=0$: $S(0)$ is the subfield closure of $\mathrm{gens}$. Finiteness of ${\pi,\varphi}$ plus the finite-generator closure lemma yields countability.
Successor: assume $S(n)$ countable. The set $S(n)\cup\exp(S(n))\cup\log(S(n))$ is a finite union of countable sets (the inductive hypothesis and images under continuous maps), hence countable. $S(n+1)$ is the subfield closure of that set, so the countable-generator closure lemma finishes the step.
why it matters
Countability of each stage is the load-bearing step toward countability of the full exp/log-closed RS field $T=\bigcup_n S(n)$, proved immediately downstream as a countable union of countable stages. That fact feeds the finite-description clause (C3) of a closed observable framework: countable state space, no continuous moduli.
Downstream uses include ledger reconstruction (a closed framework carries a zero-parameter comparison ledger), the boolean hierarchy obstruction example, and the canonical minimal-orbit framework on $\mathbb{N}$ in the unified forcing chain. Without stagewise countability, the RS constant field could smuggle continuous parameters and break the closed, zero-parameter story that the forcing chain relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.