rat_mem
plain-language theorem explainer
Every rational, as a real, lies in the subfield generated by any countable family of named constants. Builders of the Primitive Recognition Calculus operational carrier cite this to place the prime field inside the generable reals. The proof is a one-line appeal to the subfield axiom that every subfield of the reals contains the rationals.
Claim. For any family of named constants $\kappa:\mathbb{N}\to\mathbb{R}$ and any $q\in\mathbb{Q}$, the real embedding of $q$ belongs to the subfield of $\mathbb{R}$ generated by the range of $\kappa$.
background
In Primitive Recognition Calculus, the generable reals relative to a countable family of named constants $\kappa$ are the subfield of $\mathbb{R}$ obtained by closing the range of $\kappa$ under the field operations. Equivalently, they are everything obtainable from those constants and the rationals by finitely many additions, multiplications, and inverses.
Any subfield of $\mathbb{R}$ automatically contains the prime field $\mathbb{Q}$. The present statement records that fact for the specific carrier genField κ := Subfield.closure (Set.range κ). Upstream, constant rational ledgers are already known to be Cauchy sequences in the PRC real construction, so the rational base is available both algebraically and as completed limits.
The local module assembles the generable carrier as the countable, operationally closed home for quantities that can actually be named and computed from a discrete list of constants.
proof idea
One-line term proof. Apply the Mathlib subfield-class lemma that every subfield of a characteristic-zero field (here $\mathbb{R}$) contains the image of the rational cast, instantiated at the subfield genField κ and the given rational $q$. No unfolding of the closure is required.
why it matters
This is the rational half of the claim that the generable field is a genuine operational carrier. The parent theorem genField_is_operational_carrier packages five closure properties: containment of every rational, containment of every named constant, and closure under addition, multiplication, and negation. Without the rational inclusion, the carrier would be a bare generated set rather than a field containing the prime field.
In the Recognition foundation stack this anchors the discrete-to-continuous bridge: named constants and rationals generate a countable subfield that can serve as the arithmetic substrate for later PRC constructions (Cauchy ledgers, display bounds, properness). It does not itself invoke the forcing chain T0–T8 or the J-cost, but it supplies the algebraic base those layers sit on once constants are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.