S
plain-language theorem explainer
Defines the countable ascending chain of real subfields obtained by starting from the subfield generated by π and φ, then repeatedly adjoining exp and log images and closing under field operations. Anyone working on the Primitive Recognition Calculus exp/log field, or on which RS constants live in a constructive real subfield, cites this stage map. The body is a plain recursive definition on ℕ.
Claim. Define a sequence of real subfields $S:\mathbb{N}\to\mathrm{Subfield}(\mathbb{R})$ by $S_0=\overline{\{\pi,\varphi\}}$ (subfield closure of the generators) and $S_{n+1}=\overline{S_n\cup\exp(S_n)\cup\log(S_n)}$, where the bar denotes subfield closure in $\mathbb{R}$.
background
In the Primitive Recognition Calculus exp/log field module, one builds the smallest real subfield that is closed under real exponential and logarithm and that contains the RS seed constants. The generators are the two-element set ${\pi,\varphi}$: rationals appear automatically as the prime field of any subfield of $\mathbb{R}$, so these seeds plus field operations and exp/log are intended to reach every RS constant.
One stage of the construction, written $S_{\mathrm{step}}(K)$, takes a subfield $K\subseteq\mathbb{R}$, forms the set $K\cup\exp(K)\cup\log(K)$, and returns its subfield closure. The present definition iterates that stage from the generator closure, producing an increasing chain of stages indexed by natural numbers. The eventual target field is the directed union of the stages (the sibling object $T$ in the same module).
proof idea
No proof: this is a recursive definition on $\mathbb{N}$. Base case $n=0$ is the subfield closure of the generator set ${\pi,\varphi}$. Successor case applies the one-stage operator that closes under exp, log, and field operations. Downstream lemmas (monotonicity, directedness, countability) reason by induction on this recursion.
why it matters
This chain is the constructive backbone of the exp/log field used in Foundation: every later membership, countability, or closure fact about the RS constant field is stated relative to some stage $S_n$ or to the union $T=\bigcup_n S_n$. Sibling results such as stage monotonicity, directedness, and countability are immediate structural consequences of the recursion.
In the broader Recognition framework the seeds $\varphi$ and $\pi$ are forced landmarks ($\varphi$ from the self-similar fixed point in the forcing chain; $\pi$ from geometric normalizations such as $G=\varphi^5/\pi$). Closing under exp and log is how transcendental RS quantities (mass ladder factors, $\hbar=\varphi^{-5}$, bands around $\alpha^{-1}$) are placed inside a single countable real subfield rather than assumed as ambient reals. Name collisions with unrelated action functionals $S$ elsewhere in the monolith are accidental; the consumers of this definition are the PRC stage and union lemmas, not the Noether or ILG action layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.