demarcation
plain-language theorem explainer
The natural numbers, integers, and rationals are physically real in the Recognition sense, while the real continuum is not. Physically real means δ-forced: the type admits an explicit injection into ℕ. Anyone citing the floor demarcation or continuum-as-purchase spine results needs this package. The proof is a four-conjunct term pairing the three choice-free tower certificates with classical uncountability of ℝ.
Claim. A type is physically real precisely when it is $\delta$-forced (admits an injection into $\mathbb{N}$). Then $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ are physically real, and $\mathbb{R}$ is not.
background
In the Primitive Recognition Calculus, a type $X$ is $\delta$-forced when it carries an explicit countable certificate: a nonempty type of injections $X \hookrightarrow \mathbb{N}$. That is the formal content of being finitely generated, hence enumerable, from the act of distinction. The ontological alias PhysicallyReal is definitionally identical to $\delta$-forced; the name records the thesis that this mathematical cut is the physical one.
The forced tower is built choice-free: $\mathbb{N}$ is trivially $\delta$-forced, $\mathbb{Z}$ via an explicit even/odd certificate into $\mathbb{N}$, and $\mathbb{Q}$ via a paired certificate (the top of the companion-algebra tower $\mathbb{N}\delta \to \mathbb{Z}\delta \to \mathbb{Q}_\delta$). The continuum cut is separate: a $\delta$-certificate for $\mathbb{R}$ would force Countable $\mathbb{R}$, contradicting $\mathfrak{c} > \aleph_0$.
The module keeps the choice-free core (the tower) apart from classical display-tier facts about $\mathbb{R}$. Closure under pair, subtype, and sum is treated later and is not part of this primary demarcation.
proof idea
One-line term proof: the four conjuncts are exactly the four prior theorems deltaForced_nat, deltaForced_int, deltaForced_rat, and not_deltaForced_real, packaged by anonymous constructor. Because PhysicallyReal is definitionally DeltaForced, no further transport is needed. The three tower lemmas supply explicit injections; the continuum lemma reduces a hypothetical certificate to Countable ℝ and contradicts aleph0 < continuum via Cardinal.mk_real.
why it matters
This is the packaged floor demarcation of the Recognition foundation: the δ-tower is physically real and the continuum is not. Downstream, PublicSpine.floor_demarcation_holds tags the full package as classicalExtension (because the ℝ half uses uncountability), and continuum_is_purchase isolates the continuum cut alone under the same tag. Prefer forced_tower_holds plus continuum_is_purchase when the classical half should stay separate from the choice-free core.
In framework terms the result draws the line between what distinction can force (enumerable structure generated from primitive recognition) and what must be purchased as a classical display-tier extension. It does not itself invoke T5–T8 or the RCL; it sits under the primitive calculus that those later forcing steps presuppose when they treat discrete certificates versus continuum objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.