rat_no_sqrt_two
plain-language theorem explainer
There is no rational whose square equals 2, so the standard model of the δ-native rational field is not real-closed. Anyone arguing that the continuum is not forced by δ-native data cites this gap. The proof casts a putative rational root to ℝ and contradicts Mathlib's irrationality of √2 via the absolute-value identity for squares.
Claim. There is no rational number $q \in \mathbb{Q}$ such that $q^2 = 2$. Equivalently, the ordered field $\mathbb{Q}$ does not contain a square root of $2$, so it is not real-closed.
background
In the Primitive Recognition Calculus, the δ-native discrete index is identified with the naturals, and the forced scalar field built from that index is the rationals. Completeness and real-closure are not automatic: they would require adjoining limits or roots that δ-counting alone does not supply.
The present lemma records the classical algebraic gap: $\mathbb{Q}$ has no square root of 2. That single missing root already shows the forced field is not real-closed, hence not a continuum model. Downstream, the continuum-not-forced package packages this gap together with countability of the δ-index and of $\mathbb{Q}$.
No Recognition-specific cost functional is used here; the statement is pure field arithmetic, imported so the uniqueness and continuum arguments can discharge a named hypothesis without project-local axioms.
proof idea
Tactic proof by contradiction. From a rational $q$ with $q^2=2$, cast to reals to get $(\mathbb{R}\text{-cast }q)^2=2$. Mathlib's irrational_sqrt_two says $\sqrt{2}$ is irrational. The identity $\sqrt{x^2}=|x|$ rewrites $\sqrt{2}$ as $|q|$ after substituting the cast equation, so $\sqrt{2}$ would equal the absolute value of a rational, contradicting irrationality.
why it matters
Feeds prc_continuum_not_forced, which asserts that the continuum is not δ-forced: each field of that structure is discharged from δ-native facts (DistinctionNat ≃ ℕ) and Mathlib cardinality, with no project-local axioms. The doc-comment there lists this lemma as forced_field_has_gap.
In the Recognition foundation stack, continuum structure (completeness, real-closure) must be earned, not smuggled in. Showing that the δ-native forced field already fails to contain $\sqrt{2}$ blocks any claim that δ-counting alone forces $\mathbb{R}$. That separation keeps later uniqueness results for native cost and J-cost from silently assuming a complete ambient field.
No T0–T8 landmark is proved here; the lemma is infrastructure for the continuum-not-forced side of the PRC native-cost uniqueness module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.