carrierValues
plain-language theorem explainer
The image of the finite FRS carrier evaluation map: every real obtained by evaluating a finite expression built from the fixed constant inventory and field operations. Anyone proving countability, properness, or containment in the RS minimal field cites this set. The definition is the range of evaluation; no proof content.
Claim. Define the carrier value set as the image of evaluation on finite FRS expressions: $\{ \operatorname{eval}(e) \mid e \text{ is a finite carrier term} \} \subseteq \mathbb{R}$.
background
In the Primitive Recognition Calculus, the FRS carrier is an explicit finite-description syntax over a fixed inventory (golden ratio, $\pi$, $e$, $\alpha^{-1}$, and rationals) closed under field operations. Evaluation sends each term to a real. The sibling membership lemma records that every such value lands in the RS minimal field: the subfield of $\mathbb{R}$ generated by the named constants (automatically containing $\mathbb{Q}$).
Upstream, real display of certified analytic protocols is the supremum of lower endpoints of a nested interval protocol (equivalently the unique real in every interval). The carrier value set packages the range of that evaluation story for the FRS syntax alone, before countability and proper-subset arguments.
proof idea
Pure definition: the set is declared as the range of the carrier evaluation map on FRS expressions. No tactics or lemmas are applied at this declaration.
why it matters
This set is the object the Phase 3 headline theorem packages. Downstream, containment in the RS minimal field is immediate from evaluation membership; countability follows by monotonicity from countability of that field (only countably many finite terms); properness versus $\mathbb{R}$ is then cardinality: a countable set cannot be all of $\mathbb{R}$. The headline frs_carrier assembles soundness into the minimal field, exact values of $\varphi$, $\pi$, $e$, $\alpha^{-1}$, countability, properness, and protocol display in the $\mathbb{R}_\delta$ interface. Framework point: the carrier the theory actually computes on is finite generation over a fixed inventory, not the uncountable continuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.