eval_mem
plain-language theorem explainer
Soundness of the F_RS carrier: every finite expression built from rationals and the RS constant inventory (φ, π, e, α⁻¹) under field operations evaluates into the minimal RS subfield of ℝ. Anyone citing the Phase 3 carrier headline or complex-amplitude real/imag parts needs this. The proof is structural induction on the expression syntax, closing each constructor with subfield axioms and the named-constant membership lemmas.
Claim. For every finite carrier expression $e$ built from rationals and the constants $\varphi$, $\pi$, $e$, $\alpha^{-1}$ under negation, addition, multiplication, and inversion, the real value of $e$ lies in the minimal subfield of $\mathbb{R}$ generated by those constants.
background
The F_RS carrier is a finite-description syntax for the numbers the Recognition framework actually computes on. Expressions are inductive terms: rational literals, four named constants (the golden ratio φ, π, Euler's e, and the RS inverse fine-structure value α⁻¹), and the field operations negation, addition, multiplication, and inversion.
The target set is the minimal RS field: the subfield of ℝ obtained by closing the named constant inventory under field operations. It automatically contains ℚ as the prime field, so it is exactly the rationals adjoined with those transcendental values. Upstream membership lemmas already place each named constant inside that subfield.
Locally this module builds the explicit syntax and its evaluation map into ℝ. Soundness means evaluation never leaves the countable carrier field: finite terms stay inside the subfield generated by the inventory.
proof idea
Structural induction on the carrier expression. Rational leaves use the subfield axiom that every rational cast lies in any subfield of ℝ. Each named constant (φ, π, e, α⁻¹) is discharged by the corresponding membership lemma already proved for the minimal RS field, with a short simpa against the evaluation clauses.
Inductive steps for negation, addition, multiplication, and inversion apply the standard subfield closure lemmas (neg_mem, add_mem, mul_mem, inv_mem) to the induction hypotheses. No arithmetic identities beyond subfield axioms are required.
why it matters
This is the soundness half of the Phase 3 carrier headline: every term evaluates into the countable field rsField, so the framework works on finite generation over a fixed inventory rather than the uncountable continuum. The parent theorem frs_carrier packages this universal membership with the four constant evaluations and the inventory-as-terms facts.
Immediately downstream, carrierValues_subset is a one-line application: the set of all evaluated terms sits inside rsField. The complex-amplitude layer reuses the same fact for real and imaginary parts of F_RS[i] expressions, keeping displayed amplitudes inside the real RS carrier field.
In the broader foundation, this pins the computational carrier before mass-ladder and coupling constructions that quote φ and α⁻¹. It does not settle the open infrared boundary condition on the exact CODATA α⁻¹(0); it only guarantees that whatever value the inventory names stays inside the closed subfield.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.