Sstep
plain-language theorem explainer
One inductive stage of the exp-log subfield tower: from a real subfield K, form the subfield generated by K together with exp(K) and log(K). Cited by anyone building the countable exp-log closed field T as the directed union of stages S n. The body is a direct Subfield.closure of the three-set union; no proof content.
Claim. Given a subfield $K \subseteq \mathbb{R}$, define the next stage $S_{\mathrm{step}}(K)$ to be the subfield of $\mathbb{R}$ generated by the set $K \cup \exp(K) \cup \log(K)$.
background
This module builds a countable real subfield closed under real exponential and logarithm, as part of the Primitive Recognition Calculus foundation. Stages begin from a finite generator set (gens) and grow by repeatedly adjoining images under exp and log.
Sstep is the single-step operator of that tower. For any real subfield $K$, one takes the set-theoretic union of $K$ with the direct images $\exp''(K)$ and $\log''(K)$, then passes to the subfield they generate via Subfield.closure. The resulting object is again a subfield of $\mathbb{R}$, so the operator can be iterated.
The ambient chain is S : ℕ → Subfield ℝ with S 0 = closure gens and S (n+1) = Sstep (S n). The directed union of the stages is the target field T.
proof idea
Pure definition: no tactic proof. The right-hand side is Subfield.closure applied to the union (K : Set ℝ) ∪ Real.exp '' (K : Set ℝ) ∪ Real.log '' (K : Set ℝ). Membership of generators in the closure is then immediate from Subfield.subset_closure and the corresponding Or injection, which is how later lemmas (monotonicity, exp/log closure of the union) discharge their goals.
why it matters
This is the elementary step that makes the exp-log tower well-defined. Downstream, S is defined by iterating Sstep; S_mono proves each stage embeds in the next by observing that $K$ sits inside the closure of $K \cup \exp(K) \cup \log(K)$. The limit field T inherits exp- and log-closure from one application of Sstep: if $x \in S n$ then $\exp x, \log x \in Sstep(S n) = S(n+1) \subseteq T$ (T_exp_closed, T_log_closed).
In the Recognition foundation this supplies a concrete countable real field on which the primitive recognition calculus can evaluate exp/log without leaving the field, supporting later analytic identities tied to the J-cost and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.