rather
plain-language theorem explainer
Algebraic reals over the rationals are countable, contain √2, and sit strictly below the uncountable continuum. The observation pins the arena for completeness-free cost uniqueness: even the most generous algebraic closure of the δ-forced field remains countable. Anyone tracking the §9 resolution (monotone d'Alembert forces the cosh/J family without lub) cites this cardinality gap. The argument is a three-fact conjunction from Mathlib countability and one algebraic witness.
Claim. The set of reals algebraic over $\mathbb{Q}$ is countable, contains $\sqrt{2}$ (a root of $X^2-2$), and is therefore a proper subset of $\mathbb{R}$, which is uncountable. Hence the algebraic closure of the $\delta$-forced base field remains strictly below the continuum; only a completeness assumption crosses that cardinality gap.
background
The ambient module develops uniqueness of the native recognition cost inside Primitive Recognition Calculus. The cost functional $J$ is the unique (up to a single scale) solution of the Recognition Composition Law that is reciprocal-symmetric and normalized; equivalently, the doubled-trace lift $H$ solves d'Alembert's functional equation $H(s+t)+H(s-t)=2H(s)H(t)$ with $H(0)=1$ and evenness.
Section 9 of the development asks whether that uniqueness still holds when one drops topological completeness and retains only field operations, order, square roots, and Archimedean density. The positive answer is recorded upstream as dAlembert_cosh_of_monotone (every even, normalized, monotone-on-$[0,\infty)$ d'Alembert solution is $H(t)=\cosh(c\cdot t)$) and its cost-form corollary composition_law_monotone_forces_costLambda (monotone composition-law costs land in the costLambda family).
The present remark supplies the cardinality backdrop: the base field forced by the discrete $\delta$-calculus is essentially rational, and its real-algebraic closure is still countable.
proof idea
Three named facts are conjoined, with no further analytic work. Mathlib's Algebraic.countable gives countability of the reals algebraic over $\mathbb{Q}$. The local lemma sqrt_two_isAlgebraic exhibits $\sqrt{2}$ as a root of $X^2-2$, so the algebraic reals properly enlarge $\mathbb{Q}$. The local lemma real_not_countable (via Cardinal.not_countable_real) shows $\mathbb{R}$ is uncountable. The cardinality gap between the algebraic closure and the continuum is then immediate, and is read as the precise boundary that completeness alone crosses.
why it matters
Inside Recognition Science this remark underwrites the strength claim of the §9 package: $J$-uniqueness (forcing-chain landmark T5, with $J(x)=(x+x^{-1})/2-1$) is obtained from the composition law plus monotonicity, without least-upper-bound completeness. The countable algebraic arena is exactly where one is entitled to ask that question, and the answer is affirmative via dAlembert_cosh_of_monotone and composition_law_monotone_forces_costLambda.
Downstream constant and cosmology modules that inherit the native cost (alpha exponential form, electroweak VEV ledger scale, $\lambda$ balance, dimensional boundary matrix, baryogenesis yield carriers) sit on top of that uniqueness; they do not re-open the cardinality question. The remark also clarifies a non-claim: algebraic closure does not smuggle continuum many degrees of freedom into the cost ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.