real_uncountable
plain-language theorem explainer
The real line is uncountable: its cardinality is the continuum, strictly larger than ℵ₀. Anyone arguing that continuum geometry cannot arise from a countable distinction protocol cites this fact. The proof is a short Mathlib reduction: rewrite countability via cardinal comparison and apply aleph0 < continuum.
Claim. The set of real numbers is not countable: $\neg\mathrm{Countable}(\mathbb{R})$. Equivalently, $|\mathbb{R}|=\mathfrak{c}>\aleph_0$.
background
This module develops the cardinality form of real-line non-nativity inside Primitive Recognition Calculus. The surrounding claim is that a faithful certificate assignment from reals into a countable certificate type is impossible, so continuum structure cannot be native to a finite-distinction ledger.
Countability here is the standard Mathlib notion: a type admits an injection into the naturals (equivalently, its cardinal is at most $\aleph_0$). The continuum cardinal $\mathfrak{c}=|\mathbb{R}|$ is known to strictly exceed $\aleph_0$.
Sibling lemmas package the recognition-side reading: a faithful cover into a countable certificate type forces the domain to be countable, and therefore no uncountable type (in particular $\mathbb{R}$) admits such a cover. This theorem supplies the pure set-theoretic input to that chain.
proof idea
Term-mode, three Mathlib facts. Rewrite $\mathrm{Countable},\mathbb{R}$ as $|\mathbb{R}|\le\aleph_0$ via Cardinal.mk_le_aleph0_iff. Replace $|\mathbb{R}|$ by the continuum using Cardinal.mk_real. Conclude with not_le applied to Cardinal.aleph0_lt_continuum, i.e. $\aleph_0<\mathfrak{c}$.
why it matters
Feeds directly into real_not_faithfully_certifiable: no countable certificate type and assignment $\mathbb{R}\to\mathrm{Cert}$ can be faithful. The downstream doc states the framework reading: "The continuum carries surplus that no countable distinction protocol can witness; $\mathbb{R}$ enters only through a completion interface, not from distinction alone."
In Recognition Science this is a foundation blocker, not a dynamics theorem. Primitive distinction and the forcing chain (T0–T8) generate discrete ledger structure, eight-tick periodicity, and $D=3$; they do not mint continuum many independent certificates. The continuum must be imported as a completion or carrier refinement, which is why metric-refinement and carrier-blocker arguments appear nearby in the graph.
Without uncountability, the cardinality weapon against faithful real-line certification collapses. This lemma is the set-theoretic pin that makes non-nativity of $\mathbb{R}$ a theorem rather than a slogan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.