T_coe
plain-language theorem explainer
The carrier of the exp/log-closed RS subfield of the reals equals the set-theoretic union of its directed stage chain. Anyone proving countability or set-level properties of that field cites this identification. The proof is a one-line application of Mathlib's directed-supremum carrier lemma for subfields.
Claim. As subsets of $\mathbb{R}$, the exp/log-closed RS subfield equals $\bigcup_{n\in\mathbb{N}} S_n$, where $(S_n)_{n\in\mathbb{N}}$ is the directed increasing chain of stages whose lattice supremum defines that subfield.
background
In the Primitive Recognition Calculus, one builds an exp/log-closed subfield of $\mathbb{R}$ by stages. The stage map $S:\mathbb{N}\to\mathrm{Subfield}(\mathbb{R})$ starts at the subfield generated by a fixed finite generator set and iterates a one-step exp/log closure operator. The full object $T$ is defined as the lattice supremum $\bigsqcup_n S_n$ in the complete lattice of subfields.
Directedness of the chain under inclusion is already recorded: monotonicity of $S$ yields $\mathrm{Directed}(\le)S$. For any directed family of subfields, Mathlib identifies the carrier of the supremum with the ordinary union of carriers. That set-level fact is exactly what is needed before one can talk about countability or membership in $T$ via the stages.
proof idea
One-line term proof. Apply Subfield.coe_iSup_of_directed to the already-proved directedness of the stage chain. The lemma states that if a family of subfields is directed under inclusion, then the underlying set of their supremum equals the union of the underlying sets; instantiating on $S$ gives the claim.
why it matters
Immediate parent is the countability theorem for the exp/log-closed field: that result rewrites the carrier via this equality and concludes countability as a countable union of countable stages. Countability is a structural constraint in the Primitive Recognition Calculus: successive exp/log closure from a countable seed stays countable, so the RS number system sits strictly between $\mathbb{Q}$ and $\mathbb{R}$. Later closure-under-exp statements in the same module also work at the set level once the carrier is identified with the stage union.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.