genField_is_operational_carrier
plain-language theorem explainer
For any countable family of named constants, the generable reals form a genuine field carrier: they contain Q and the constants, are closed under the field operations, and remain countable. Foundation work on Delta-native closure cites this as the operational-carrier certificate. The proof is a one-line packaging of the subfield membership lemmas plus countability of the closure.
Claim. For every sequence $\kappa:\mathbb{N}\to\mathbb{R}$ of named constants, the generable subfield $K_\kappa\subseteq\mathbb{R}$ satisfies: $\mathbb{Q}\subseteq K_\kappa$; $\kappa(n)\in K_\kappa$ for all $n$; $K_\kappa$ is closed under $+$, $\cdot$, negation, and inversion; and $K_\kappa$ is a countable subset of $\mathbb{R}$.
background
In the Primitive Recognition Calculus, physical quantities are not free reals: they must be obtainable from a countable list of named constants by finitely many field operations. The generable field relative to $\kappa$ is defined as the subfield of $\mathbb{R}$ generated by the range of $\kappa$ (equivalently, everything reachable from those constants and the rationals by $+$, $\cdot$, $-$, and inverse).
Upstream facts pin the pieces: every rational sits in the subfield (prime-field embedding); every named constant is in the generating set, hence in the closure; and the closure of a countable set under the field operations remains countable. The module therefore treats generable reals as the candidate operational carrier for later Delta-native protocols, not as an arbitrary subset of $\mathbb{R}$.
proof idea
Term-mode conjunction that packages seven already-proved facts. Rational membership is rat_mem; constant membership is const_mem. Closure under addition, multiplication, negation, and inversion is the corresponding Subfield membership lemmas applied to the two (or one) generable hypotheses. Countability is genField_countable, which reduces to countable subfield-closure of a countable generating set. No new algebra is performed.
why it matters
This is the certificate that the generable construction is a real operational carrier rather than a bare set: field operations stay inside, and countability keeps the carrier strictly smaller than the continuum. Downstream, strongClosureCertificate in Delta-native strong closure wires it in as generableCarrier, assembling the closed Delta-native theorem surface alongside display-real and certified-analytic entries.
In the Recognition foundation stack this supports the claim that the arithmetic of named constants (the inputs to later forcing and ladder constructions) lives in a countable field carrier. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those sit higher in the T0–T8 chain. It closes the generable-carrier slot needed before strong closure can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.