DeltaForced
plain-language theorem explainer
A type is δ-forced when it admits an injection into the naturals: an explicit countable certificate. This is the formal stand-in for “finitely generated, hence enumerable, from the act of distinction.” Downstream lemmas use it to mark ℕ, ℤ, ℚ as forced and ℝ as not. The body is a one-line Prop abbreviation of nonempty embedding into ℕ.
Claim. A type $X$ is $\delta$-forced when there exists an injection $X \hookrightarrow \mathbb{N}$ (equivalently, when the type of embeddings $X \hookrightarrow \mathbb{N}$ is inhabited).
background
In the Primitive Recognition Calculus, physical status is tied to what can be generated by successive acts of distinction. The module treats that generation as an explicit certificate: a map into $\mathbb{N}$ that is injective, so every element is named by a natural number without collision.
The companion name “physically real” is defined as exactly this property: the ontological reading is that the demarcation line is the physical one, while all mathematical content sits in the $\delta$-forced predicate. Upstream, the demarcation theorem states that the $\delta$ tower $(\mathbb{N},\mathbb{Z},\mathbb{Q})$ is physically real and the continuum $\mathbb{R}$ is not; the forced-tower side is choice-free, and the $\mathbb{R}$ side uses classical uncountability of the display-tier object.
Thus $\delta$-forced is the local Prop that packages “has a countable certificate” before any closure or tower lemmas are proved.
proof idea
One-line definitional abbreviation: DeltaForced X is Nonempty (X ↪ ℕ). No tactics or lemmas; the mathematical content is the type of embeddings into $\mathbb{N}$ being inhabited. Downstream proofs unpack the nonempty witness as an explicit injection.
why it matters
This definition is the hinge of the forced-realm story in Primitive Recognition Calculus. Every concrete certificate theorem (deltaForced_nat, deltaForced_int, deltaForced_rat) and the closure lemmas (deltaForced_prod, deltaForced_sum, deltaForced_subtype) land on it. countable_of_deltaForced and deltaForced_iff_countable connect the certificate language to Mathlib countability (forward direction choice-free; reverse uses choice).
The demarcation theorem then reads: $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$ are physically real and $\mathbb{R}$ is not, because only the former carry $\delta$-certificates. That split is the formal “continuum is display tier, not forced.” In the broader Recognition chain it supports the claim that physically real structure is finitely generated from distinction, before continuum display objects appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.