genField
plain-language theorem explainer
The generable reals relative to a countable family of named constants are the subfield of the reals generated by those constants (equivalently, all values reachable from the constants and rationals by finitely many field operations). Anyone citing the ontology-vs-display split in Primitive Recognition Calculus uses this carrier. The body is a one-line Mathlib subfield-closure of the image of the constant map.
Claim. For a family of named constants $\kappa:\mathbb{N}\to\mathbb{R}$, write $\mathrm{Gen}(\kappa)$ for the subfield of $\mathbb{R}$ generated by $\{\kappa(n):n\in\mathbb{N}\}$. Equivalently, $\mathrm{Gen}(\kappa)$ is the set of all reals obtainable from the values of $\kappa$ and the rationals by finitely many additions, multiplications, and additive inverses.
background
Primitive Recognition Calculus separates a countable operational ontology from the continuum that analysis can display. The ontology side is carried by a subfield of $\mathbb{R}$ generated from a named constant family $\kappa:\mathbb{N}\to\mathbb{R}$. A subfield is a subset closed under $+$, $\cdot$, and additive inverse and containing $1$; Mathlib's subfield closure returns the smallest such set containing a given generating set.
Taking the range of $\kappa$ yields a countable generating set. Downstream results then show the resulting subfield is countable, proper in $\mathbb{R}$, contains every rational and every $\kappa(n)$, and is closed under the field operations, so it is a genuine operational carrier rather than a bare set.
The module imports minimal-field countability lemmas and the Delta-real protocol layer used on the display side of the comparison.
proof idea
One-line definition: the generable field is Mathlib's Subfield.closure applied to Set.range κ. No further proof obligations; the noncomputable marker is inherited from subfield closure.
why it matters
This is the carrier object for Phase 2 of Primitive Recognition Calculus. Every sibling theorem hangs off it: countability of the generable set, membership of rationals and named constants, properness in $\mathbb{R}$, and the packaged operational-carrier statement (closed under field operations, contains $\mathbb{Q}$ and the constants).
The headline result "display exceeds generation" uses properness to produce a real that is the value of some Delta-real protocol yet lies outside the generable field. That gap is the guard against smuggling uncountable ontology through the analysis interface: protocols can land on the full continuum, while the ontology remains the countable generable subfield. Downstream, ObjecthoodRegistry.classify_permitted also consumes the carrier when classifying permitted objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.