pi_is_term
plain-language theorem explainer
Evaluating the dedicated π constructor of the F_RS expression syntax returns the real number π. Carrier and inventory lemmas cite this to pin the constant inventory inside the countable term language. The proof is pure reflexivity: eval is defined by cases to send that constructor to Real.pi.
Claim. The evaluation map on $F_{RS}$ expressions sends the atomic $\pi$ term to the real number $\pi$.
background
The module builds an explicit finite-description carrier for the Recognition Science field $F_{RS}$. Expressions are an inductive syntax over the rationals together with a fixed inventory of RS constants ($\varphi$, $\pi$, $e$, $\alpha^{-1}$), closed under negation, addition, multiplication, and inversion.
A recursive evaluation map interprets each expression as a real. On the atomic $\pi$ constructor that map is defined to be ordinary real $\pi$. Sibling facts do the same for rationals, $\varphi$, $e$, and $\alpha^{-1}$. The local goal is to show the framework computes on a finitely generated, countable proper subset of $\mathbb{R}$, not on the continuum.
proof idea
One-line reflexivity. By the case-wise definition of the evaluation map on the inductive expression type, the $\pi$ constructor evaluates to $\mathrm{Real}.\pi$, so the equality holds by rfl.
why it matters
Feeds the Phase 3 headline frs_carrier, which packages soundness into the minimal RS field, inventory equalities ($\varphi$, $\pi$, $e$, $\alpha^{-1}$), countability, proper-subset status, and protocol display in the $\mathbb{R}_\delta$ interface. The headline states that the carrier the framework actually computes on is finite generation over a fixed inventory, not the uncountable continuum. Pinning $\pi$ as a first-class term keeps geometric constants inside that countable syntax rather than as external oracles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.