deltaForced_nat
plain-language theorem explainer
Natural numbers are δ-forced: they admit an explicit injection into ℕ, namely the identity. Anyone building the forced tower (ℕ, ℤ, ℚ) or the discrete/continuum demarcation cites this base case. The proof is the reflexive embedding of ℕ into itself, choice-free.
Claim. The type of natural numbers is $\delta$-forced: there exists an injection $\mathbb{N}\hookrightarrow\mathbb{N}$. Equivalently, $\mathbb{N}$ carries a countable certificate and is therefore (by the module thesis) physically real.
background
In this module a type $X$ is δ-forced when it carries an explicit countable certificate: a nonempty type of injections $X\hookrightarrow\mathbb{N}$. The doc-comment states the formal content as "finitely generated, hence enumerable, from the act of distinction."
The ontological reading equates physically real with δ-forced; the mathematical content sits entirely in the injection certificate. The local setting is the primitive recognition calculus: which types can be forced from distinction alone, without classical choice.
ℕ is the base of the forced tower. Downstream results package ℕ, ℤ, and ℚ as the choice-free physically real tower, then contrast them with ℝ.
proof idea
One-line term proof. Instantiate the δ-forced predicate by the reflexive embedding $\mathrm{id}:\mathbb{N}\hookrightarrow\mathbb{N}$ (Mathlib Function.Embedding.refl). No lemmas beyond the definition of the embedding and the Nonempty wrapper are required.
why it matters
This is the base conjunct of the forced tower. Downstream, forcedTower assembles $\mathrm{PhysicallyReal},\mathbb{N}\land\mathrm{PhysicallyReal},\mathbb{Z}\land\mathrm{PhysicallyReal},\mathbb{Q}$ choice-free from this fact plus the integer and rational certificates; the doc-comment calls that "the exact formal residue of 'the δ tower ℕδ → ℤδ → ℚδ is built, not posited.'"
demarcation then adds classical uncountability of ℝ to draw the line: the δ tower is physically real; the continuum is not. In Recognition Science terms this is foundation-level ontology for what can appear as a finitely generated distinction structure before continuum display objects enter. It does not itself invoke T5–T8 or the J-cost, but it underwrites which number systems the later calculus is allowed to treat as forced rather than posited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.