rs_operations_below_continuum
plain-language theorem explainer
A single countable subfield of the reals is closed under field operations, exp, and log, and already contains π, φ, e, and α⁻¹. Anyone arguing that Recognition Science constants live below the continuum cites this existence package. The proof is a term that exhibits the directed-union field T and discharges countability, closure, seed membership, and properness via prior lemmas.
Claim. There exists a subfield $K \subseteq \mathbb{R}$ such that $K$ is countable, $x \in K$ implies $e^x \in K$ and $\log x \in K$, $\pi \in K$, $\varphi \in K$, $e \in K$, $\alpha^{-1} \in K$, and $K \neq \mathbb{R}$.
background
This module builds the exp/log-closed Recognition field inside the Primitive Recognition Calculus. The object $T$ is defined as the directed union $\bigsqcup_n S_n$ of an ascending chain of subfields of $\mathbb{R}$, started from the seeds $\pi$ and $\varphi$ and closed step-by-step under the field operations together with real exp and log. Sibling facts record that $T$ is countable, proper (not all of $\mathbb{R}$), and closed under exp and log.
The constants that matter for RS sit inside $T$ by construction. Membership of $\varphi$ and $\pi$ is by seed inclusion; $e = \exp 1$ follows from exp-closure once $1 \in T$; $\alpha^{-1}$ is the assembled expression $44\pi,\exp(-w_8\ln\varphi/(44\pi))$, and every intermediate (field ops, one log, one exp) lands in $T$. The ambient continuum is used only as the host of the standard real exp/log; the workspace of RS constant construction is the countable field $T$.
proof idea
Term-mode existence: the witness is the already-constructed subfield $T$. The proof is the 8-tuple $\langle T,,T_\mathrm{countable},,T_\mathrm{exp_closed},,T_\mathrm{log_closed},,\pi\in T,,\varphi\in T,,e\in T,,\alpha^{-1}\in T,,T_\mathrm{proper}\rangle$. Each conjunct is a prior lemma in the same module (countability of the directed union, the two closure maps, the four membership theorems, and properness). No new algebra is done here; the theorem only packages those facts into the existential claim.
why it matters
Doc-comment labels this Item 1 (deep half) of the PRC program: RS operations, not merely outputs, live below the continuum. Downstream, prc_shrunk_certificate consumes the sibling headline that physics constants sit in a countable field; this theorem is the operational half of that claim (closure under the generators, not just membership of finished constants).
In the broader framework it underwrites the claim that the forcing chain (T5 J-uniqueness through T8, $D=3$), the RCL, and the assembled constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, $\alpha^{-1}$ in the narrow band) can be written inside a countable exp/log field seeded by $\pi$ and $\varphi$. The continuum is ambient host, not computational substrate. It does not resolve the OPEN infrared boundary condition on the exact CODATA $\alpha^{-1}(0)$; it only shows the RS expression for $\alpha^{-1}$ never leaves $T$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.