real_not_countable
plain-language theorem explainer
The real line is uncountable at the type level. PRC uniqueness cites this to separate the countable δ-forced algebraic carrier from the continuum, so distinction never forces ℝ. The proof is a one-line appeal to Mathlib's cardinality fact on the universe set.
Claim. The continuum is not countable: $\neg\,\mathrm{Countable}(\mathbb{R})$.
background
In Primitive Recognition Calculus, δ (distinction) generates a countable index type equivalent to ℕ and a forced field that begins as ℚ. Closing algebraic questions over that field yields the real algebraic numbers, still a countable set, which already contains √2 (the gap bare ℚ cannot answer).
The module's continuum-not-forced package needs a sharp size comparison: whatever δ forces stays countable, while the ambient continuum does not. This declaration is the type-level half of that comparison, imported from Mathlib cardinality rather than reproved project-locally.
Local setting is native-cost uniqueness and structural ledger arguments: scale families, generated closures under finitary rules, and the claim that calibration collapses an uncountable gauge orbit rather than a discrete list of impostors.
proof idea
Assume a Countable instance on ℝ. Promote it with haveI, then apply Mathlib's Cardinal.not_countable_real to Set.countable_univ. The resulting contradiction discharges the negation. Pure term-mode wrapper; no project lemmas.
why it matters
Anchors the size half of "the continuum is not δ-forced." Downstream, delta_algebraic_closure_stays_countable packages Algebraic.countable, √2 algebraic, and this fact as a checked triple. generated_ne_univ_real uses it to show no countable seed under countably many finite-arity rules exhausts ℝ. prc_continuum_not_forced discharges the continuum-not-forced interface from δ-native countability plus Mathlib, with no project axioms. continuum_scale_family_uncountable cites the same uncountability to show the collapsed calibration orbit is not a discrete impostor list.
In the Recognition forcing picture this keeps the continuum out of the T0–T8 discrete skeleton (eight-tick, D=3, φ-ladder): distinction and native cost stay countable/algebraic while ℝ remains an ambient completion, not a forced carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.