eval
plain-language theorem explainer
The evaluation map sends every finite carrier expression built from rationals and the RS constant inventory (φ, π, e, α⁻¹) to its real value, with field operations read as ordinary arithmetic on ℝ. Anyone working with the F_RS carrier or the minimal RS field cites this as the semantic bridge from syntax to reals. It is a structural recursion on the expression tree, not a theorem.
Claim. Define $\mathrm{eval}$ from finite $F_{RS}$ carrier expressions to $\mathbb{R}$ by: each rational $q$ maps to its real embedding; $\varphi$ maps to the golden ratio; $\pi$ to $\pi$; $e$ to $\exp(1)$; $\alpha^{-1}$ to the RS fine-structure value $44\pi\,\exp(-w_8\ln\varphi/(44\pi))$; and negation, addition, multiplication, inversion act as the corresponding operations on $\mathbb{R}$.
background
The module builds the $F_{RS}$ carrier: a countable subfield of $\mathbb{R}$ generated by the Recognition Science constant inventory. The syntax is the inductive type of finite terms over $\mathbb{Q}$ together with named constants $\varphi$, $\pi$, $e$, and $\alpha^{-1}$, closed under negation, addition, multiplication, and inversion.
Upstream, rsField is the subfield of $\mathbb{R}$ obtained as the Subfield-closure of those named constant values (so it automatically contains $\mathbb{Q}$). The MinimalField $\alpha^{-1}$ is the specific transcendental $44\pi\exp(-w_8\ln\varphi/(44\pi))$, matching the RS-native fine-structure construction (distinct from the exponential-resummation form in Constants.Alpha, which remains OPEN at the exact IR boundary).
Evaluation is the unique structure-preserving interpretation of that syntax into $\mathbb{R}$. The next lemma (soundness) asserts every such term lands inside rsField.
proof idea
Pure definition by structural recursion on the inductive expression type. Each constructor is interpreted by the matching real operation or constant: rationals via the canonical cast; $\varphi$ via Real.goldenRatio; $\pi$ via Real.pi; $e$ via Real.exp 1; $\alpha^{-1}$ via the MinimalField value; and the four field operations via negation, addition, multiplication, and inversion on $\mathbb{R}$. No lemmas are applied; noncomputability is inherited from the real constants.
why it matters
Without a concrete evaluation map, the carrier syntax is only formal. This definition is the semantic layer that lets later results (soundness: every term lands in rsField; membership lemmas for rationals, $\varphi$, $\pi$, $e$, $\alpha^{-1}$; countability and properness of the carrier value set) talk about actual reals rather than trees.
In the Recognition framework it pins the minimal field that must carry RS physics: the prime field plus the forced constants from the forcing chain (T5–T6 give $J$ and $\varphi$; the alpha band sits near $137.03$–$137.04$). Downstream siblings use it to prove the finite-description syntax never escapes the countable carrier. No used_by edges are recorded yet; the immediate consumers are the in-module soundness and carrier-value lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.