intToNat
plain-language theorem explainer
Explicit certificate map from integers to naturals: nonnegatives to evens, negatives to odds. Cited wherever ℤ is shown δ-forced in the Primitive Recognition Calculus, and as the numerator leg of the ℚ certificate. Pure case-split definition on the integer constructors; injectivity is proved separately.
Claim. Define $f:\mathbb{Z}\to\mathbb{N}$ by $f(k)=2k$ when $k\ge 0$, and $f(-(k+1))=2k+1$ when $k\ge 0$ (nonnegatives to evens, negatives to odds).
background
In Primitive Recognition Calculus, a type is δ-forced when it carries an explicit injective certificate into $\mathbb{N}$ (orbit positions built by ofNat). The module builds a choice-free tower $\mathbb{N}\delta\to\mathbb{Z}\delta\to\mathbb{Q}_\delta$.
Integers need a concrete embedding before they can sit in that tower. The standard even/odd coding works: nonnegative integers land on even naturals, and negSucc k (the Lean encoding of $-(k+1)$) lands on odds. Upstream, ofNat only builds DistinctionNat positions from verifier Nats; the present map supplies the integer-to-Nat leg those positions will later receive.
proof idea
Definition by cases on the two Int constructors. Int.ofNat k maps to $2k$; Int.negSucc k maps to $2k+1$. No proof body and no lemmas applied; the companion injectivity theorem handles uniqueness of preimages by the same case split plus arithmetic.
why it matters
Packages the integer leg of the forced tower. Downstream, deltaForced_int is the one-line witness $\langle f, f\text{-inj}\rangle$ that $\mathbb{Z}$ is DeltaForced, described as "ℤ is δ-forced via the explicit even/odd certificate. Choice-free." The same map is the numerator half of ratToNat, which pairs $f(q.num)$ with $q.den$ and climbs to $\mathbb{Q}_\delta$ ("top of the forced tower ... ℕδ → ℤδ → ℚδ"). Without this certificate the integer and rational δ-forced theorems have nothing to package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.