PRCContinuumNotForced
plain-language theorem explainer
Distinction does not force the continuum: the native index of repeated distinction is countable, the forced field is the rationals (countable, missing √2), while the reals are uncountable and fill that gap. Anyone citing the Recognition Science stratification of forced versus assumed structure needs this negative T0 result. The declaration is a Prop bundle of seven cardinality and ordered-field facts that witness the gap; a companion theorem discharges each field from Mathlib and the native index equivalence.
Claim. The continuum is not forced by primitive distinction. Precisely: the native distinction index is equinumerous with $\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 homomorphism $\mathbb{Q}\to\mathbb{R}$; $\mathbb{R}$ contains a square root of $2$, is uncountable, and every map $\mathbb{N}\to\mathbb{R}$ misses some real.
background
In the Primitive Recognition Calculus, distinction proceeds one act at a time. The inductive native index (zero and successor) is the base-neutral finite orbit of repeated distinction and is equinumerous with the naturals. Every object generated by iterating distinction is therefore countable.
The δ-forced arithmetic carrier is the rationals: countable, and not real-closed (no square root of two). The continuous completion $\mathbb{R}$ embeds $\mathbb{Q}$ as an ordered field and fills algebraic gaps, but is uncountable. Almost every real is never named by any sequence of distinction acts. The module develops native cost uniqueness and the honest split between what distinction forces and what must be assumed for continuous J-forcing.
Upstream, the native distinction index supplies countability of the δ-generated carrier. Mathlib cardinality, the nonexistence of a rational square root of two, and the ordered embedding of $\mathbb{Q}$ into $\mathbb{R}$ supply the remaining field facts. Completeness is thereby marked as an added principle (the trace-closure boundary), not a δ-consequence.
proof idea
This is a structure definition bundling a Prop, not a proved theorem. Seven fields record the obstruction: countable distinction index; countable forced field; missing $\sqrt{2}$ in $\mathbb{Q}$; ordered-field embedding $\mathbb{Q}\hookrightarrow\mathbb{R}$; existence of $\sqrt{2}$ in $\mathbb{R}$; uncountability of $\mathbb{R}$; and diagonal unnamability (every $\mathbb{N}\to\mathbb{R}$ sequence misses a point).
No proof body lives here. The companion theorem builds an inhabitant by supplying the native-index equivalence with $\mathbb{N}$, Mathlib's countable instance on $\mathbb{Q}$, the standard no-rational-square-root-of-two fact, the rational cast homomorphism with injectivity and strict monotonicity, and the usual real-analysis facts on $\sqrt{2}$ and uncountability of $\mathbb{R}$.
why it matters
This is the negative resolution of T0 in the forcing chain: distinction does not force the continuum. The J-forcing argument (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$ via the Recognition Composition Law) lives on the continuous completion; this structure records that completeness is a genuine posit beyond distinction, measured exactly by the cardinality gap $\aleph_0<\mathfrak{c}$.
Downstream, the companion theorem discharges every field with no project-local axioms. The full stratification structure packages the result as the completion boundary and the carrier-strictly-below-completion clause (reals have $\sqrt{2}$, no rational orbit does), establishing the honest terminal claim: δ forces the discrete tower and the rational field; $\mathbb{R}$ is the first genuine addition. The maximal reading that distinction forces everything including the continuum is false; J-forcing is conditional on the completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.