S_directed

In the Primitive Recognition Calculus exp/log field module, a countable real subfield is built by iterating a stage operator. Stage zero is the subfield closure of a fixed generator set; each successor applies a one-step adjunction (exp/log structure) to the previous stage. The resulting map $S:\mathbb{N}\to\mathrm{Subfield},\mathbb{R}$ is the increasing chain of stages.

Monotonicity is already on record: each stage embeds in the next, so $S$ is a monotone sequence of subfields under inclusion. For subfields, directedness of a family is the standard hypothesis that makes the supremum subfield coincide with the set-theoretic union of carriers. That identification is exactly how the terminal field $T$ is handled downstream.

One-line term proof. Monotonicity of the stage map (obtained from the successor inequality via the usual monotone_nat_of_le_succ packaging) is fed to Mathlib's Monotone.directed_le, which turns any monotone sequence on $\mathbb{N}$ into a directed family under $\le$. No separate case analysis on indices is required.

Directedness is the hypothesis Mathlib needs to characterize the terminal field $T:=\bigvee_n S_n$. Downstream, membership in $T$ is rewritten as eventual membership in some stage, and the carrier of $T$ is identified with the union of the stage carriers; both rewrites invoke this lemma via the directed-supremum API for subfields.

Those characterizations immediately yield countability of $T$ as a countable union of countable stages, which is the structural backbone of the exp/log field in the Primitive Recognition Calculus. The lemma is pure order-theoretic glue inside the Foundation layer: it does not itself force physical constants, but it licenses treating the staged recognition field as a single countable subfield before continuum limits are taken.