FRSExpr
plain-language theorem explainer
Finite term syntax for the F_RS carrier: rationals plus the fixed RS inventory (φ, π, e, α⁻¹), closed under negation, addition, multiplication, and inversion. Anyone citing the Phase-3 carrier headline or soundness of evaluation into rsField depends on this datatype. As an inductive definition it carries no proof burden; it is the grammar that later evaluation and membership theorems interpret.
Claim. The carrier expression language $F_{\mathrm{RS}}$ is the free inductive syntax generated by rational constants $q\in\mathbb{Q}$, the named constants $\varphi$, $\pi$, $e$, and $\alpha^{-1}$, and the field operations $-$, $+$, $\cdot$, and $(\,\cdot\,)^{-1}$.
background
Primitive Recognition Calculus builds a countable working field inside $\mathbb{R}$ rather than treating the continuum as the computational substrate. The minimal field inventory supplies four named transcendentals: the golden ratio $\varphi$ (forced as the self-similar fixed point in the T6 step of the forcing chain), $\pi$, Euler's $e$, and the RS fine-structure value $\alpha^{-1}=44\pi\exp(-w_8\ln\varphi/(44\pi))$ from the PRC minimal-field package (related to the canonical exponential resummation in Constants.Alpha).
Field operations on the ambient reals are already available; what is missing is an explicit finite-description syntax whose values stay inside that countable subfield. The module therefore introduces a free term language over $\mathbb{Q}$ and the inventory, closed under the four field operations. Downstream evaluation maps each constructor to the corresponding real (cast of a rational, Real.goldenRatio, Real.pi, Real.exp 1, or the minimal-field $\alpha^{-1}$), and soundness shows every such value lands in rsField.
proof idea
No proof: this is an inductive datatype declaration. The nine constructors are the grammar; DecidableEq and Repr are derived automatically. Semantic content appears only in the companion evaluator eval and the soundness theorem eval_mem, which proceed by structural induction on this type.
why it matters
This syntax is the concrete carrier the framework actually computes on. The Phase-3 headline frs_carrier packages soundness (eval_mem), the four constant-as-term identities (phi_is_term, pi_is_term, e_is_term, alphaInv_is_term), countability and proper-subset claims for the image, and protocol display into the $\mathbb{R}_\delta$ interface (has_protocol_display). Without a finite term language, those statements would quantify over an uncountable continuum rather than over finitely generated expressions.
In the broader Recognition picture the inventory is not arbitrary: $\varphi$ is the T6 fixed point, the eight-tick/octave structure (T7) and $D=3$ (T8) sit upstream of the coupling constructions that produce the $\alpha^{-1}$ band near $(137.030,137.039)$. The carrier makes precise that every number the calculus manipulates is a finite word in those landmarks and the rationals. The exact infrared CODATA match for $\alpha^{-1}(0)$ remains an open boundary condition; the syntax itself does not resolve it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.