T
plain-language theorem explainer
The exp/log-closed Recognition Science scalar field is the directed union of the stage chain of real subfields. Anyone working in the primitive recognition calculus cites it as the ambient field closed under the iterative exp/log step. The definition is a one-line lattice supremum of that increasing chain.
Claim. Let $S:\mathbb{N}\to\mathrm{Subfield}(\mathbb{R})$ be the increasing stage chain with $S_0$ the subfield generated by the primitive generators and $S_{n+1}$ the exp/log step of $S_n$. The exp/log-closed RS field is the subfield $T:=\bigvee_{n\in\mathbb{N}} S_n\subseteq\mathbb{R}$.
background
In the primitive recognition calculus, one builds a real subfield large enough for the RS cost and ladder constructions by closing under exponentiation and logarithm. The stage map $S$ starts at the subfield generated by a finite generator set and iterates a single-step closure operator that adjoins the needed exp/log values.
The module records that this chain is increasing, monotone, directed, and countable. The present declaration packages the whole tower into one object: the join (directed union) in the lattice of subfields of $\mathbb{R}$. That join is again a subfield, so all later calculus can treat $T$ as a single ambient scalar domain.
Upstream, the stage definition is exactly $S_0=\overline{\mathrm{gens}}$ and $S_{n+1}=\mathrm{Sstep}(S_n)$. Homonymous symbols elsewhere (ILG action functionals, discrete edge index sets) are unrelated; here $S$ and $T$ are purely field-theoretic.
proof idea
One-line definitional wrapper: $T$ is declared as the supremum $\bigsqcup_n S_n$ in the complete lattice of subfields of $\mathbb{R}$. No tactic proof is required; well-formedness follows from the directedness of the stage chain already established for $S$.
why it matters
This is the ambient exp/log-closed scalar field for the Recognition foundation layer. Downstream action and Noether developments (momentum conservation from space-translation invariance of a $J$-action, quadratic leading coefficient of the cost at the minimum, inertial reduction of the Euler–Lagrange equation) sit on real calculus that presupposes a field closed under the operations the stage chain adjoins.
In the broader RS picture it supplies the scalar domain in which the $J$-cost, the $\varphi$-ladder, and related analytic limits are interpreted, without enlarging all the way to $\mathbb{R}$ when a smaller exp/log hull suffices. With roughly forty use sites it is infrastructural rather than a deep theorem: parent results quote membership or coercion into $T$ whenever they need the closed field as a type.
It does not itself force $\varphi$, the eight-tick period, or $D=3$; those live in the unified forcing chain. It only freezes the scalar universe in which such statements are written.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.