classify_forced_rationals
plain-language theorem explainer
Every subfield of the reals contains every rational: the unique prime subfield is forced into every carrier. Foundation work on objecthood cites this to mark the rationals as ontologically forced, not conventional or completed. The proof is a one-line term applying the Mathlib fact that rational casts land in every subfield.
Claim. For every subfield $K \subseteq \mathbb{R}$ and every rational $q \in \mathbb{Q}$, the canonical real image of $q$ belongs to $K$. Equivalently, $\mathbb{Q}$ is contained in every subfield of $\mathbb{R}$.
background
The ObjecthoodRegistry module sorts mathematical ingredients of the primitive recognition calculus by ontological status: forced, display, completion, convention, quotient, observable, permitted. The label forced means no admissible carrier can omit the object; it is present in every structure the framework allows.
Here a carrier is treated as a subfield of the reals. Classically, $\mathbb{Q}$ is the prime subfield of $\mathbb{R}$: every subfield of $\mathbb{R}$ contains the image of every rational under the canonical cast. That is pure field theory (characteristic zero), not an RS-specific construction.
Sibling entries classify forced scales, displays, completions, conventions, and related statuses, and feed the objecthood periodic table that inventories what the calculus may assume versus what it must derive.
proof idea
One-line term proof. Instantiate Mathlib's SubfieldClass.ratCast_mem on an arbitrary subfield $K \subseteq \mathbb{R}$ and rational $q$. That lemma already states that the coercion of any rational into the ambient field lands in every subfield (more generally, every SubfieldClass instance). No Recognition lemmas, cost identities, or calibration facts are used.
why it matters
In Recognition Science, forced objects are non-negotiable skeleton: every carrier must contain them. Recording that the rationals are forced anchors the arithmetic presupposed by comparisons, quotients, cost functionals, and later classifiers. The doc-comment states they are the unique prime subfield and that no carrier of the framework can omit them.
This sits with the forced-scale classifier and the display, completion, convention, quotient, observable, and permitted classifiers as registry rows for the objecthood periodic table. The dependency graph currently shows no downstream consumers, so the declaration is a foundational inventory entry rather than a lemma later proofs rewrite with. It fixes a modeling boundary: $\mathbb{Q}$ is not optional scaffolding and is not an RS-derived constant like $\varphi$ or the eight-tick period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.