prc_continuum_not_forced
plain-language theorem explainer
Distinction alone does not force the real continuum: the δ-native index is countable (bijective with ℕ), the forced field is ℚ (countable, no √2), while ℝ fills that gap and is uncountable, hence unnamable by any δ-act sequence. Auditors of the Recognition Science forcing chain cite this as the negative T0 resolution. The proof discharges the seven-field continuum-not-forced structure from DistinctionNat ≃ ℕ and standard Mathlib cardinality facts.
Claim. The distinction-native index is equivalent to $\mathbb{N}$; the forced field $\mathbb{Q}$ is countable and satisfies $\neg\exists q\in\mathbb{Q},\, q^2=2$; there is an injective strictly monotone ring map $\mathbb{Q}\to\mathbb{R}$; the completion $\mathbb{R}$ contains a square root of $2$, is uncountable, and for every $f:\mathbb{N}\to\mathbb{R}$ some real lies outside the image of $f$.
background
In Primitive Recognition Calculus, a single distinction act δ generates a native index type equivalent to the natural numbers. From that index one obtains the integer surface and the rational field as the arithmetic genuinely forced by distinction. Cost-forcing arguments (J-uniqueness, calibration) live on a continuous completion of that field, classically $\mathbb{R}$.
The structure inhabited here records the honest split between forced and assumed. The forced field $\mathbb{Q}$ is countable and has a concrete algebraic gap: no rational squares to 2. The real completion fills the gap ($\sqrt{2}$ exists) but is uncountable, so no sequence of δ-acts can name all of its points. The cardinality gap $\aleph_0 < \mathfrak{c}$ is the exact quantitative obstruction.
Doc-comment of the structure: "T0 resolved, NEGATIVE: distinction does not force the continuum... the obstruction is exact and quantitative, a cardinality gap."
proof idea
Structure constructor discharging seven fields, each by a short Mathlib or project fact.
- δ-index countable: the existing equivalence
DistinctionNat ≃ ℕ. - Forced field countable: typeclass inference on $\mathbb{Q}$.
- Forced field has gap: classical
rat_no_sqrt_two. - Shared rational field:
Rat.castHom ℝ, rewritten to the coercion and fedRat.cast_strictMono(injective + strictly monotone). - Completion fills gap: witness
Real.sqrt 2withReal.sq_sqrt. - Completion uncountable:
real_not_countable. - Completion unnamable: by contradiction; a surjection $\mathbb{N}\to\mathbb{R}$ would make the range equal $\mathbb{R}$ and countable, contradicting
Cardinal.not_countable_real.
No project-local axioms; pure assembly of δ-native countability with standard real/rational facts.
why it matters
Negative answer to the program's last load-bearing foundation question (T0): δ does not force the continuum on which the rest of the forcing chain runs. J-uniqueness (T5), φ as self-similar fixed point (T6), the eight-tick octave (T7), and D=3 (T8) all live on the continuous completion; this theorem shows that completion is an assumption, measured exactly by $\aleph_0 < \mathfrak{c}$.
Primary consumer is prc_full_stratification, which installs this object as the completion_not_forced stratum in the terminal honest accounting: "δ forces {number tower, rational field}; the completion and a single cost unit are assumed; on the completion the cost form is forced." Sibling witnesses (sqrt_two_isAlgebraic) and ladder limits (costLambda_successor_increment_tendsto) sit in the same stratification. After this result, residual freedom collapses to the completion commitment plus one positive calibration unit; nothing of the continuum is forced by distinction alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.