rat_is_term
plain-language theorem explainer
Evaluating a rational constant inside the F_RS expression syntax recovers that rational as a real. Anyone discharging base cases for the countable RS carrier field cites this. The proof is pure definitional equality via reflexivity.
Claim. For every rational $q \in \mathbb{Q}$, evaluation of the corresponding F_RS carrier term equals the canonical embedding of $q$ into $\mathbb{R}$.
background
The F_RS carrier is a finite expression syntax over the rationals together with a fixed inventory of Recognition Science constants ($\varphi$, $\pi$, $e$, and $\alpha^{-1}$), closed under negation, addition, multiplication, and inversion. Evaluation sends each such term to a real number by interpreting constructors in the obvious way.
This module builds the countable field of values that finite RS descriptions can name. The rational constructor is the base of that syntax: every other constant and every field operation sits on top of it. Upstream, the inductive type of carrier expressions records exactly those constructors and nothing else.
Local soundness work (every term lands in the minimal RS subfield of $\mathbb{R}$) treats the rational case first, then the named constants, then the field operations by induction.
proof idea
One-line reflexivity proof. By definition, evaluation on the rational constructor is the standard cast $\mathbb{Q} \to \mathbb{R}$, so the equality holds definitionally with no lemmas required.
why it matters
This is the rational base case of the constant inventory for the F_RS carrier. It anchors the claim that finite RS descriptions never leave a countable, explicitly generated subfield of the reals: every rational is present as a term and evaluates to itself.
Together with the sibling facts for $\varphi$, $\pi$, $e$, and $\alpha^{-1}$, it feeds the soundness induction that every carrier term lands in the minimal RS field. That countable carrier is the semantic home for RS-native constants (including the $\varphi$-ladder mass formula and the $\alpha^{-1}$ band) before any continuum analysis begins. No downstream theorem is wired yet in the graph, but the inventory is the prerequisite for any later uniqueness or completeness argument about named RS values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.