S_monotone
plain-language theorem explainer
The stage map S on natural numbers is monotone as a chain of real subfields. Anyone building directed unions or countable colimits of the primitive recognition calculus stages cites this. The proof is a one-line application of the standard successor-to-monotone lemma to the already-proved successive inclusion.
Claim. The map $S:\mathbb{N}\to\{\text{subfields of }\mathbb{R}\}$ is monotone: if $m\le n$ then $S(m)\subseteq S(n)$.
background
In the primitive recognition calculus exp/log field module, one builds a nested sequence of real subfields that will eventually support the exponential and logarithm as field operations generated from a finite seed set. The stage map $S$ starts at the subfield closure of the generators and iterates a one-step closure operator Sstep.
The predecessor result states that each stage sits inside the next: $S(n)\le S(n+1)$ as subfields. That successive inclusion is the only arithmetic input needed here. The ambient setting is ordinary ordered subfields of $\mathbb{R}$; no Recognition-Science cost functional or forcing-chain hypothesis is used at this layer.
proof idea
One-line wrapper. Apply the Mathlib lemma monotone_nat_of_le_succ to the already-established successive inclusion $S(n)\le S(n+1)$. That lemma converts a chain of successor inequalities on $\mathbb{N}$ into full monotonicity of the map.
why it matters
Monotonicity is the immediate prerequisite for directedness of the stage system. The next theorem packages it as Directed (· ≤ ·) S via S_monotone.directed_le, which is the standard hypothesis for forming the directed union of the stages and proving that union remains a countable subfield. Inside the Recognition foundation this supplies the inductive scaffolding on which the exp/log field is later realized; it does not itself invoke the J-cost, the forcing chain T0–T8, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.