delta_algebraic_closure_stays_countable
plain-language theorem explainer
The real algebraic numbers over the rationals form a countable set that contains √2, while the reals themselves are uncountable. Anyone arguing that δ-forced polynomial comparisons stay strictly below the continuum cites this packing. The proof is a three-conjunct term applying standard Mathlib cardinality facts.
Claim. The set $\{ x \in \mathbb{R} : x \text{ is algebraic over } \mathbb{Q} \}$ is countable, $\sqrt{2}$ is algebraic over $\mathbb{Q}$, and $\mathbb{R}$ is not countable.
background
In Primitive Recognition Calculus the δ-forced field starts at the rationals. Polynomial comparisons (gaps such as √2 that ℚ misses) may require real-algebraic extensions. The standing prose claim is that even the full real-algebraic closure of that field stays countable, so closing every δ-posable polynomial question never reaches the continuum.
A real is algebraic over ℚ when it is a root of a nonzero rational polynomial. The local module develops native-cost uniqueness without completeness; this lemma pins the precise carrier for that program. Upstream cost notation (J-cost as $(x+x^{-1})/2-1$) is ambient context only: the statement itself is pure cardinality.
proof idea
One-line term proof: the triple conjunction of Mathlib facts Algebraic.countable ℚ ℝ (algebraic reals are countable), sqrt_two_isAlgebraic (√2 is algebraic over ℚ), and real_not_countable (ℝ is uncountable). No local arithmetic or case analysis.
why it matters
Converts the prose assertion behind prc_continuum_not_forced into a checked theorem: the most generous algebraic closure of the δ-forced field remains strictly below the continuum. Only a completeness posit crosses the cardinality gap. That pins the §9 arena (now closed positively via monotone d'Alembert forcing into the costLambda family, and ultimately Cost.Jcost at unit calibration): ask whether J can be forced without completeness inside a countable field where every polynomial δ-question resolves; the answer is yes. Downstream, costLambda_successor_increment_tendsto reads the calibration invariant off the discrete δ-act ladder inside this same countable setting. Framework landmark: supports T5 J-uniqueness and the Recognition Composition Law without continuum hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.