frs_carrier
plain-language theorem explainer
The F_RS carrier is a finite expression syntax over rationals and the fixed inventory φ, π, e, α⁻¹, closed under field operations. Every term lands in the countable RS field, the inventory evaluates to the expected reals, the value set is countable and proper in ℝ, and each value admits a Δ-real protocol display. Anyone citing the Phase-3 carrier or strong closure will use this. The proof is a pure conjunction of the already-proved component lemmas.
Claim. Every finite $F_{RS}$ term evaluates into the countable RS field; the constants evaluate as $\mathrm{eval}(\varphi)=\varphi$, $\mathrm{eval}(\pi)=\pi$, $\mathrm{eval}(e)=e$, $\mathrm{eval}(\alpha^{-1})=\alpha^{-1}_{\mathrm{RS}}$; the set of all term values is countable and a proper subset of $\mathbb{R}$; and every term value equals the real denoted by some $\Delta$-real protocol (nested rational intervals of width $\le 1/(n+1)$).
background
The Primitive Recognition Calculus builds a computable carrier for Recognition Science quantities. FRSExpr is an inductive finite syntax: rationals, the inventory atoms φ, π, e, α⁻¹, and closure under negation, addition, multiplication, and inversion. Evaluation sends each term to a real; the target ambient object is MinimalField.rsField, the countable field generated by that inventory inside ℝ.
A Δ-real protocol is a nested family of rational intervals whose widths shrink as $1/(n+1)$; its value is the unique real in every interval (equivalently the supremum of lower endpoints). The carrier value set is the image of evaluation on all terms. Upstream siblings already pin the inventory equalities (e.g. alphaInv_is_term is definitional), countability, properness, and membership in rsField.
Local setting (module): Phase 3 of the foundation stack asserts that the framework computes on finite generation over a fixed inventory, not on the uncountable continuum.
proof idea
Term-mode conjunction: the proof is the 8-tuple of prior lemmas
eval_mem, phi_is_term, pi_is_term, e_is_term, alphaInv_is_term,
carrierValues_countable, carrierValues_proper, and has_protocol_display.
No new algebra is done here; each conjunct is discharged by the corresponding sibling theorem (inventory equalities are mostly rfl against the MinimalField constants; countability and properness come from the inductive syntax and the known transcendence/independence of the generators; protocol display routes each evaluated real through the Δ-real interface).
why it matters
Doc-comment labels this the Phase 3 headline: the carrier the framework actually computes on is finite generation over a fixed inventory, not ℝ. Downstream, strongClosureCertificate in DeltaNativeStrongClosure assembles the closed Δ-native theorem surface and consumes this carrier package (alongside generable-field and certified-analytic entries).
In the broader RS stack this pins where φ (T6 fixed point), the fine-structure construction α⁻¹ (canonical exponential resummation near 137.04; exact IR value still OPEN as a boundary condition), and the classical constants π, e sit as first-class terms with protocol displays. It separates the countable computational substrate from continuum scaffolding and feeds any later claim that RS quantities are operationally presentable in ℝδ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.