carrierValues_subset
plain-language theorem explainer
The set of reals obtained by evaluating finite carrier expressions sits inside the minimal RS subfield of ℝ generated by the named constants. Anyone proving countability or properness of that value set cites this inclusion. The argument is a short range elimination that applies evaluation soundness.
Claim. The set of all real numbers obtained by evaluating finite FRS carrier expressions is contained in the minimal subfield of $\mathbb{R}$ generated by the Recognition Science constants (the closure of those constants under field operations).
background
The FRS carrier is a finite-term syntax built from rational literals and the named RS constants (φ, π, e, α⁻¹, and siblings). Evaluation sends each term to a real via the certified analytic protocol stack; the carrier value set is exactly the range of that evaluation map.
The minimal RS field is the subfield of ℝ obtained by closing those named constants under the field operations. It automatically contains ℚ as the prime field, so it is ℚ adjoined with the constant values.
Upstream soundness states that every carrier term evaluates into this field: induction on expression structure handles rationals by the prime-field embedding and each named constant by the corresponding membership lemma.
proof idea
Take an arbitrary element of the carrier value set. By definition it is the evaluation of some finite carrier expression. Apply the soundness theorem for evaluation, which places that real inside the minimal RS field. The inclusion follows immediately; no further field arithmetic is required.
why it matters
This inclusion is the bridge from syntactic evaluation to the algebraic carrier used throughout the primitive recognition calculus. The immediate parent is the countability theorem for the carrier value set, which obtains countability by monotonicity from the already-countable minimal RS field. That countability step, together with the proper-subset result, pins the carrier as a countable proper subset of ℝ: only countably many finite terms exist, and they never exhaust the continuum. In the broader foundation layer this keeps every RS-native constant and every finite combination of them inside a single countable subfield before later forcing and mass-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.