genField_proper
plain-language theorem explainer
For any countable family of named real constants, the subfield they generate is a proper subset of the reals. Anyone citing the Phase 2 split between generable ontology and analytic display needs this fact. The proof is a one-line cardinality argument: the generable field is countable, hence cannot equal the continuum.
Claim. For every sequence $\kappa:\mathbb{N}\to\mathbb{R}$, the subfield of $\mathbb{R}$ generated by the range of $\kappa$ is not equal to $\mathbb{R}$ as a set.
background
In the Primitive Recognition Calculus, the generable reals relative to a countable constant family $\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 $+,-,\times,\div$. That set is the candidate ontology: only countably many finite descriptions exist.
The companion countability theorem records that this carrier is countable, via the standard fact that the subfield closure of a countable set of reals remains countable. The local module then separates that countable carrier from the full continuum that analysis can display through Delta-real protocols (nested-interval constructions whose values are arbitrary reals).
proof idea
Assume for contradiction that the generable field equals the universe of reals. Transport the already-proved countability of the generable field along that equality to conclude that $\mathbb{R}$ is countable. That contradicts the classical fact that the continuum is uncountable. The argument is a pure cardinality one-liner; no further field-theoretic structure is used beyond the countability lemma.
why it matters
This is the properness half of the Phase 2 headline. Downstream, the display-exceeds-generation theorem combines it with surjectivity of Delta-real protocol values to produce an explicit real that analysis can name yet finite generation cannot: the guard against smuggling uncountable ontology through the analysis interface. The objecthood registry packages countability and properness together as the admissibility criterion for any countable constant inventory. Within Recognition Science foundation work, the result keeps the operational carrier strictly smaller than the display continuum, so the ontology stays countable while analysis still reaches every real as a limit object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.