S_mono
plain-language theorem explainer
Each finite stage of the real exp-log subfield tower sits inside the next stage. Anyone building or citing the monotone chain of subfields generated by successive exp and log adjunctions needs this step. The argument is a direct subset inclusion from the stage operator, which always re-includes its input field before closing.
Claim. For every $n \in \mathbb{N}$, the stage subfield $S_n \subseteq \mathbb{R}$ satisfies $S_n \subseteq S_{n+1}$, where $S_0$ is the subfield generated by the primitive generators and $S_{n+1}$ is obtained by adjoining images under $\exp$ and $\log$ to $S_n$ and taking the generated subfield.
background
In the Primitive Recognition Calculus exp-log field module one builds a nested sequence of real subfields by repeatedly adjoining transcendental images. The stage operator takes a subfield $K \subseteq \mathbb{R}$ and returns the subfield generated by $K \cup \exp(K) \cup \log(K)$. The chain $S$ starts at the subfield generated by a fixed finite generator set and iterates that operator: $S_0 = \overline{\mathrm{gens}}$ and $S_{n+1} = \mathrm{Sstep}(S_n)$.
The local goal is a countable real subfield closed under $\exp$ and $\log$, obtained as the directed union of the stages. Monotonicity of the chain is the first structural fact needed before directedness and countability.
Upstream, the definition of the stage operator already packages the three-set union and the subfield closure; the present lemma only records that the input field is among those three sets.
proof idea
Unfold $S(n+1) = \mathrm{Sstep}(S_n)$. By definition of the stage operator the carrier of $S_n$ is one of the three sets fed to subfield closure, so $\mathrm{Subfield.subset_closure}$ places every element of $S_n$ inside $\mathrm{Sstep}(S_n)$. The resulting set inclusion of carriers is converted to the subfield order via $\mathrm{SetLike.coe_subset_coe}$. No induction and no special properties of $\exp$ or $\log$ are used.
why it matters
This is the successor step for the full monotone statement $S_\mathrm{monotone}$, obtained immediately by $\mathrm{monotone_nat_of_le_succ}$. That monotone chain is the scaffold on which directedness, countability, and the eventual exp-log closed subfield $T$ of the Primitive Recognition Calculus rest.
In the Recognition foundation layer the construction supplies a concrete real field large enough to host the continuous calculus used by later forcing and measurement arguments, without assuming a pre-existing exp-log closed ambient field beyond $\mathbb{R}$ itself. The lemma is pure field-tower bookkeeping; it does not yet force physical constants or the T0–T8 chain, but it is a necessary rung under those analytic layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.