rsField_mem_e
plain-language theorem explainer
Euler's number $e$ belongs to the minimal Recognition-Science subfield of $\mathbb{R}$ generated by the named constants. Anyone proving that finite RS expressions stay inside a countable carrier, or assembling the "physics below continuum" headline, cites this membership. The proof is a one-line wrapper: $e$ is literally one of the generators, so it sits in the subfield closure.
Claim. Let $S = \{\varphi, \pi, e, \alpha^{-1}\}$ be the named Recognition-Science constants, and let $K = \mathbb{Q}(S)$ be the subfield of $\mathbb{R}$ generated by $S$. Then $e \in K$.
background
The module builds the smallest subfield of $\mathbb{R}$ that can host the named Recognition-Science constants. The generator set rsConstants is exactly ${\varphi, \pi, e, \alpha^{-1}}$, where $\varphi$ is the golden ratio and $\alpha^{-1}$ is the fine-structure reciprocal used in RS units.
The object rsField is defined as the subfield closure of that finite set. Because every subfield of $\mathbb{R}$ contains the prime field $\mathbb{Q}$, the result is $\mathbb{Q}(\varphi,\pi,e,\alpha^{-1})$. The surrounding development uses this carrier to argue that RS physics lives in a countable subfield, strictly below the continuum.
Membership lemmas for each generator are the elementary facts that feed both the countability headline and the soundness of the finite-expression evaluator.
proof idea
One-line wrapper. Apply the Mathlib fact that every set is contained in its subfield closure (Subfield.subset_closure). Unfold the definition of the generator set and discharge membership of $e$ by simp, since $e = \mathrm{Real.exp},1$ is listed among the four generators.
why it matters
This is one of the four generator-membership facts that make the countable carrier usable. Downstream, eval_mem (soundness of the finite RS expression language) cases on the e constructor and invokes this lemma so every evaluated term lands in rsField. The same fact is conjoined into rs_physics_below_continuum, the Item-1 headline: every named RS constant lives in one countable subfield of $\mathbb{R}$, so the framework does not need the full continuum as the home of its constants.
In the broader Recognition chain the point is architectural rather than numerical: once $\varphi$ is forced (T6) and the remaining named constants are adjoined, the physics codomain stays countable. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.