T_exp_closed
plain-language theorem explainer
If a real number lies in the countable exp/log-closed RS subfield T, its exponential does too. Anyone placing e or α⁻¹ inside T, or proving that RS constant-building stays below the continuum, cites this closure. The argument lifts membership one stage along the directed chain: exp-images are adjoined by the next S-step, so the union T is stable under exp.
Claim. Let $T\subseteq\mathbb{R}$ be the directed union $\sup_n S_n$ of the stage subfields that successively adjoin $\exp$ and $\log$. If $x\in T$, then $\exp(x)\in T$.
background
The module builds a single countable subfield of $\mathbb{R}$ large enough for Recognition Science constants yet strictly below the continuum. Start from a finite seed set of generators, close under field operations, then iterate a stage map that adjoins images under real $\exp$ and $\log$.
Concretely, Sstep K is the subfield generated by $K\cup\exp(K)\cup\log(K)$. The chain $S_0=\overline{\mathrm{gens}}$, $S_{n+1}=\mathrm{Sstep}(S_n)$ is increasing and directed. The target field is the directed supremum $T=\bigsqcup_n S_n$. Membership in $T$ is equivalent to membership in some finite stage: $x\in T\Leftrightarrow\exists n,,x\in S_n$.
This lemma is the exp half of the closure package that makes $T$ an exp/log-closed carrier for later constant constructions.
proof idea
Rewrite both the hypothesis and the goal with the stage characterization of membership in $T$. From $x\in S_n$, form the witness $n+1$. By definition $S_{n+1}=\mathrm{Sstep}(S_n)$ is the subfield closure of $S_n\cup\exp(S_n)\cup\log(S_n)$, so $\exp(x)$ sits in that generating set (as an exp-image of an element of $S_n$). Subfield.subset_closure finishes the membership, hence $\exp(x)\in T$.
why it matters
Exp-closure is the elementary step that puts Euler's number in $T$ ($e=\exp(1)$ with $1\in T$) and keeps every exp appearing in the RS formula for $\alpha^{-1}$ inside the same countable carrier. Downstream, e_mem_T is a one-line application; alphaInv_mem_T chains field operations, one log, and one exp entirely in $T$; rs_operations_below_continuum and the headline cost_and_constants_share_one_countable_field package the same fact into the claim that RS constants and the cost $J$ share one countable field.
In framework terms this removes the continuum from the workspace of constant construction: seeds $\pi$ and $\varphi$, the operations, and derived values such as $e$ and $\alpha^{-1}$ (in the RS band near $137$) all live in $T$. It is foundation scaffolding for the countable-carrier half of the Primitive Recognition Calculus, not a forcing-chain (T0–T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.