mem_T_iff
plain-language theorem explainer
Membership in the exp/log-closed Recognition Science field equals membership in some finite stage of its directed subfield chain. Anyone placing constants (φ, π) in that field, or proving exp/log-closure, cites this equivalence. The proof is a one-line wrapper of the directed-supremum membership lemma for subfields.
Claim. For $x\in\mathbb{R}$, $x$ lies in the exp/log-closed RS field $T:=\bigvee_n S_n$ if and only if there exists $n\in\mathbb{N}$ with $x\in S_n$, where $(S_n)$ is the increasing directed chain of stage subfields of $\mathbb{R}$.
background
In the Primitive Recognition Calculus exp/log field module, one builds a countable subfield of $\mathbb{R}$ closed under real exponential and logarithm. The stages $S:\mathbb{N}\to\mathrm{Subfield},\mathbb{R}$ start from the subfield closure of a finite generator set and iterate a one-step closure operator that adjoins exp and log of prior elements. The chain is monotone, hence directed under inclusion.
The target object $T$ is defined as the directed supremum $T=\bigsqcup_n S_n$ (written $\sup_n S_n$ in the subfield lattice). Directed-suprema of subfields are again subfields, so $T$ is a subfield of $\mathbb{R}$. The directedness theorem records that the stage map is directed under $\le$, which is exactly the hypothesis needed to characterize membership in the supremum by existential membership in some stage.
proof idea
One-line wrapper: apply the Mathlib lemma that an element lies in the supremum of a directed family of subfields if and only if it lies in some member of the family, instantiated at the directedness of the stage chain. No further case analysis or induction is required.
why it matters
This characterization is the working interface for every concrete membership and closure argument about the exp/log-closed RS field. Downstream, it is rewritten both ways to place $\pi$ and the golden ratio $\varphi$ in $T$ at stage zero (via the generator set), and to prove that $T$ is closed under $\exp$ and $\log$ by lifting a witness stage $n$ to stage $n+1$ under the one-step closure. Those facts pin the ambient scalar field in which Recognition Composition Law identities, the $\varphi$-ladder mass formula, and the forced constants ($c=1$, $\hbar=\varphi^{-5}$, etc.) are interpreted as living inside a single countable exp/log-closed subfield of $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.