T_log_closed
plain-language theorem explainer
The countable RS field T is closed under real logarithm: if x lies in T then log x also lies in T. Anyone assembling RS constants (especially α⁻¹) or proving that all RS operations stay below the continuum cites this. The proof is a one-step stage bump: membership in some S n puts log x into S(n+1) by the definition of Sstep.
Claim. Let $T\subset\mathbb{R}$ be the exp/log-closed Recognition Science subfield (the directed union of the stage chain $S_n$). If $x\in T$, then $\log x\in T$.
background
In the Primitive Recognition Calculus, the ambient workspace for RS constants is not all of $\mathbb{R}$ but a countable subfield $T$ built to be closed under the operations that actually appear: field operations, $\exp$, and $\log$.
The construction is staged. Generators seed $S_0$ as a subfield closure. Each successor $S_{n+1}=\mathrm{Sstep}(S_n)$ adjoins the images of the current field under $\exp$ and $\log$, then closes again under field operations. The chain is directed and increasing; $T:=\bigsqcup_n S_n$ is their supremum as a subfield of $\mathbb{R}$.
Membership in $T$ is characterized by mem_T_iff: $x\in T$ if and only if $x$ already lives in some finite stage $S_n$. That equivalence is the only upstream fact needed here.
proof idea
Rewrite both the hypothesis and the goal with mem_T_iff, so the claim becomes: if $x\in S_n$ for some $n$, then $\log x\in S_m$ for some $m$. Take $m=n+1$. By definition, $S_{n+1}=\mathrm{Sstep}(S_n)$ is the subfield closure of $S_n$ together with $\exp(S_n)$ and $\log(S_n)$. The set inclusion $\mathrm{Subfield.subset_closure}$ puts $\log x$ into that closure once $x\in S_n$, via the right-hand disjunct of the generating set. Done.
why it matters
Log-closure is half of the operational package that lets RS constants be built without leaving a countable carrier. Downstream, rs_operations_below_continuum packages $T$ as a single countable subfield closed under $\exp$ and $\log$ and already containing the seeds $\pi$ and $\varphi$; alphaInv_mem_T uses log-closure (with exp-closure and field operations) to keep every step of $\alpha^{-1}=44\pi,\exp(-w_8\ln\varphi/(44\pi))$ inside $T$; and the headline cost_and_constants_share_one_countable_field unifies that operational closure with $J$-cost closure and the derived constants $e$ and $\alpha^{-1}$.
In framework terms this is the foundation layer under the forcing chain and the Recognition Composition Law: the workspace for $J$, $\varphi$, and the fine-structure band is countable and log-closed, so the continuum is ambient only, not operational.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.