deltaForced_int
plain-language theorem explainer
The integers admit an explicit injection into the naturals, so they are δ-forced (countably certified from distinction). Anyone citing the forced tower ℕ→ℤ→ℚ or the physical demarcation against ℝ needs this middle rung. The proof is a one-line term packing the even/odd encoding with its injectivity lemma. Choice-free throughout.
Claim. The integers are $\delta$-forced: there exists an injective map $\mathbb{Z}\hookrightarrow\mathbb{N}$. Equivalently, $\mathbb{Z}$ carries an explicit countable certificate built from the act of distinction.
background
In the Primitive Recognition Calculus, a type $X$ is $\delta$-forced when it carries a nonempty injection $X\hookrightarrow\mathbb{N}$. That is the formal content of being finitely generated, hence enumerable, from distinction. By thesis, physically real coincides with $\delta$-forced; the mathematical content lives entirely in the injection certificate.
The certificate used here is the standard even/odd pairing on $\mathbb{Z}$: nonnegatives map to evens ($k\mapsto 2k$) and negatives (via $\mathrm{negSucc}$) map to odds ($k\mapsto 2k+1$). This is the middle step of the forced tower $\mathbb{N}\delta\to\mathbb{Z}\delta\to\mathbb{Q}_\delta$ from the companion algebra paper, kept entirely choice-free.
proof idea
Term-mode construction of a nonempty embedding. The witness is the pair consisting of the explicit map $\mathrm{intToNat}$ (ofNat $k\mapsto 2k$, negSucc $k\mapsto 2k+1$) together with the already-proved injectivity lemma $\mathrm{intToNat_inj}$. That lemma case-splits on the two constructors of $\mathbb{Z}$; parity separates the branches and arithmetic closes equalities. No tactics run at this theorem site itself.
why it matters
Supplies the $\mathbb{Z}$ conjunct of $\mathrm{forcedTower}$ (physically real $\mathbb{N}\wedge\mathbb{Z}\wedge\mathbb{Q}$, choice-free) and of $\mathrm{demarcation}$ (same plus $\neg$ physically real $\mathbb{R}$). Downstream docs stress that the positive tower is isolated from the classical uncountability of $\mathbb{R}$ so the constructive residue of "built, not posited" stays clean. This is the middle rung of the $\delta$ tower after naturals and before rationals; it anchors the framework claim that physical reality tracks $\delta$-forced types while the continuum remains display-tier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.