e_is_term
plain-language theorem explainer
Evaluating the base inventory term for Euler's number in the F_RS expression syntax yields the real exp(1). Anyone assembling or citing the countable RS carrier field uses this identity. The proof is pure reflexivity against the evaluation clauses.
Claim. The evaluation map on the $F_{RS}$ expression syntax sends the distinguished base constructor for Euler's number to $\exp(1)\in\mathbb{R}$.
background
The module builds an explicit finite-description carrier for Recognition Science arithmetic. FRSExpr is the inductive syntax of terms generated from rationals together with a fixed inventory of RS constants ($\varphi$, $\pi$, $e$, $\alpha^{-1}$), closed under negation, addition, multiplication, and inversion.
Evaluation is the recursive map from that syntax into $\mathbb{R}$ that interprets each constructor at its intended real value and each field operation as the corresponding real operation. The local goal is to pin every inventory constant to a named real, so the carrier is not an opaque subset of $\mathbb{R}$ but a finitely generated expression language.
Upstream, the inductive declaration of the syntax already includes a nullary constructor for $e$; this lemma only records how that constructor is interpreted.
proof idea
One-line reflexivity. By definition of the evaluation function on the nullary inventory constructor for Euler's number, the equality eval e = Real.exp 1 holds definitionally, so rfl closes the goal.
why it matters
Feeds the Phase 3 headline frs_carrier, which packages soundness of evaluation into the countable RS field, the four inventory identities ($\varphi$, $\pi$, $e$, $\alpha^{-1}$), countability, proper-subset status inside $\mathbb{R}$, and protocol display in the $\mathbb{R}_\delta$ interface. The downstream doc-comment stresses that "the carrier the framework actually computes on is finite generation over a fixed inventory, not the uncountable continuum." This lemma is the $e$-clause of that inventory package: without it the headline conjunction cannot name $\exp(1)$ as a term value. It is pure foundation scaffolding for later mass-ladder and constant-band work, not itself a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.