sqrt_two_isAlgebraic
plain-language theorem explainer
√2 is algebraic over ℚ as a root of X² − 2. Recognition Science cites this to discharge the concrete gap that the δ-forced rational field cannot answer, while staying inside a countable carrier. The proof is a short term construction: exhibit the monic polynomial and evaluate it at √2.
Claim. The real number $\sqrt{2}$ is algebraic over $\mathbb{Q}$: there exists a nonzero polynomial $p \in \mathbb{Q}[X]$ with $p(\sqrt{2}) = 0$. Explicitly, $p(X) = X^2 - 2$ works.
background
In the Primitive Recognition Calculus native-cost uniqueness module, the δ-forced field is the rationals: every comparison forced by the discrete distinction index lands in ℚ. That field has a concrete gap: it does not contain √2. The structure prc_continuum_not_forced records this as forced_field_has_gap := rat_no_sqrt_two, together with countability of the forced field and of the distinction index.
Algebraicity over ℚ is the standard Mathlib predicate IsAlgebraic ℚ: a real is algebraic when it is a root of some nonzero rational polynomial. The real algebraic numbers are exactly the carrier in which every δ-posable polynomial comparison resolves, including the √2 gap that bare ℚ misses. The module's §5.1 / §9 backing argument needs both that √2 sits in that carrier and that the carrier remains countable.
proof idea
Term-mode witness. Refine with the polynomial $X^2 - C,2$ and two subgoals. Nonzeroness is Polynomial.X_pow_sub_C_ne_zero with a numeric check that the constant 2 is nonzero. Evaluation uses Real.sq_sqrt (so $(√2)^2 = 2$), then aeval simplification and the cast identity (algebraMap ℚ ℝ) 2 = 2, reducing to 2 - 2 = 0.
why it matters
Feeds delta_algebraic_closure_stays_countable and the companion packaging theorem that turns the prose claim of prc_continuum_not_forced into checked Lean: the set of reals algebraic over ℚ is countable, it contains √2, and ℝ is uncountable. Closing every δ-posable polynomial comparison therefore never escapes countability; the continuum is not δ-forced.
This is foundation bookkeeping for the Recognition forcing story, not a new physical constant. It pins the gap named in forced_field_has_gap and supports the countability half of the continuum-not-forced certificate. Downstream cost-ladder results in the same module sit in the broader uniqueness development; this lemma itself is the algebraic √2 witness those countability packages quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.