rsField
plain-language theorem explainer
The minimal real subfield that carries Recognition Science physics is the subfield of ℝ generated by φ, π, e, and α⁻¹. It automatically contains ℚ, so it is exactly the rationals adjoined with those four constant values. Carrier and F_RS authors cite it as the ambient field for every finite-description evaluation. The definition is the ordinary subfield closure of the named constant set.
Claim. Define $K \subseteq \mathbb{R}$ to be the subfield generated by $\{\varphi, \pi, e, \alpha^{-1}\}$. Then $K$ is the minimal field carrying RS physics; equivalently $K = \mathbb{Q}(\varphi, \pi, e, \alpha^{-1})$.
background
Primitive Recognition Calculus isolates a countable ambient field before any continuum analysis. The named constant inventory is the finite set ${\varphi, \pi, e, \alpha^{-1}}$, where $\varphi$ is the golden ratio, $\pi$ and $e$ are the usual reals, and $\alpha^{-1}$ is the RS fine-structure inverse (sitting in the narrow band near 137).
Any subfield of $\mathbb{R}$ contains the prime field $\mathbb{Q}$. Closing under field operations therefore yields exactly the adjunction of those four constants to the rationals. Downstream carrier syntax evaluates every finite term into this field and nowhere else.
The local module builds the minimal field and records elementary membership and countability facts for the generators. That package is the substrate for the F_RS carrier soundness theorems.
proof idea
One-line definition: take the Mathlib subfield closure of the finite set of named RS constants. No further proof obligations; membership of each generator and countability are separate sibling lemmas.
why it matters
This is the ambient field for the Phase 3 F_RS carrier headline. Soundness (eval_mem) states that every carrier term lands in this field; carrierValues_subset packages the same fact for the image set; frs_carrier quotes it as the countable home of all finite-description values. Complex-amplitude real and imaginary parts reuse the same membership.
Framework-wise it pins the claim that RS computation runs on finite generation over a fixed inventory (φ from T6, plus π, e, and α⁻¹), not on the uncountable continuum. Protocol display into the Δ-real interface then only needs values already inside this field. Without a named minimal field, the carrier would have no sharp codomain for soundness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.