intToNat_inj
plain-language theorem explainer
The explicit certificate ℤ→ℕ that sends nonnegatives to evens and negatives to odds is injective. Anyone establishing that ℤ (and then ℚ) is δ-forced cites this lemma. The proof is four-way case analysis on the Int constructors, with omega discharging the parity equalities and contradictions.
Claim. The map $f:\mathbb{Z}\to\mathbb{N}$ given by $f(k)=2k$ for $k\ge 0$ and $f(-(k+1))=2k+1$ for $k\ge 0$ is injective: $f(a)=f(b)$ implies $a=b$.
background
In the Primitive Recognition Calculus, a type is δ-forced when it admits an explicit injective certificate into ℕ. That certificate is the bridge from discrete recognition data to the number systems used downstream; the construction is required to be choice-free.
The local certificate for integers is the even/odd encoding: nonnegative integers land on even naturals, and negative integers (via negSucc) land on odds. This is the standard parity bijection written as a total function ℤ→ℕ, kept under local control so later injectivity and pairing lemmas do not pull classical choice through Mathlib square-root machinery.
The same module builds the forced tower ℕδ → ℤδ → ℚδ. Injectivity of this integer certificate is the middle rung of that tower.
proof idea
Tactic proof by intro a b h and nested cases on the two Int constructors (ofNat / negSucc), giving four branches.
Same-sign branches: the hypothesis is 2·ka = 2·kb or 2·ka+1 = 2·kb+1; omega recovers ka = kb, then rewrite.
Mixed-sign branches: the hypothesis equates an even to an odd (2·ka = 2·kb+1 or the reverse); exfalso plus omega closes the contradiction.
No external lemmas beyond arithmetic; the argument is pure constructor analysis plus linear integer arithmetic.
why it matters
This injectivity is the witness half of the δ-forced structure on ℤ: deltaForced_int packages ⟨intToNat, intToNat_inj⟩ and records that ℤ is δ-forced via the explicit even/odd certificate, choice-free.
It is also consumed by ratToNat_inj, which reduces rational equality to a Cantor pairing of numerator certificates and denominators; after dpair_inj2, the numerator step is exactly this lemma. That places the result at the middle of the forced tower ℕδ → ℤδ → ℚδ named in the companion algebra paper.
In the broader Recognition stack, δ-forced number systems are the discrete substrate on which cost, orbit, and physical-reality predicates sit. Keeping the certificate constructive avoids classical choice leaking into later uniqueness and forcing arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.