ratToNat
plain-language theorem explainer
Maps each rational to a natural by Cantor-pairing the integer-to-natural encoding of its numerator with its positive denominator. Anyone assembling the choice-free δ-forced tower ℕ → ℤ → ℚ cites this certificate. The body is a one-line composition of the local pairing and the signed-integer encoding.
Claim. Define a map $\mathbb{Q}\to\mathbb{N}$ by sending $q$ to the Cantor pair of the natural encoding of its integer numerator with its denominator: $\mathrm{cert}(q)=\pi(\iota(q.\mathrm{num}), q.\mathrm{den})$, where $\iota:\mathbb{Z}\to\mathbb{N}$ sends nonnegatives to evens and negatives to odds, and $\pi$ is the local square-block pairing.
background
In the Primitive Recognition Calculus, a type is δ-forced when it carries an explicit injective certificate into $\mathbb{N}$. That certificate is the constructive witness that the type sits in the forced arithmetic tower rather than the continuum display tier.
The integer certificate sends $\mathrm{ofNat},k$ to $2k$ and $\mathrm{negSucc},k$ to $2k+1$. The local pairing $\mathrm{dpair}(a,b)$ is the classical Cantor map written with an if so that injectivity stays choice-free: if $a<b$ then $b^2+a$, else $a^2+a+b$. Mathlib's Nat.pair is the same function, but its injectivity lemmas pull classical choice through Nat.sqrt.
This definition simply feeds the numerator through the integer certificate and pairs the result with the denominator, producing an explicit $\mathbb{Q}\to\mathbb{N}$ certificate.
proof idea
One-line definitional composition: apply the integer-to-natural certificate to q.num, then feed that natural together with q.den into the local Cantor pairing. No tactics or lemmas are invoked at the definition site; injectivity is proved separately.
why it matters
This is the top certificate in the forced tower constructed in the companion algebra paper ($\mathbb{N}\delta\to\mathbb{Z}\delta\to\mathbb{Q}_\delta$). Downstream, deltaForced_rat packages it with its injectivity proof into DeltaForced ℚ, and ratToNat_inj discharges injectivity by unpacking the pair and invoking integer-certificate injectivity plus rational equality from matching num/den.
In the Recognition framework this marks the boundary of what is δ-forced: rationals carry a choice-free certificate; the reals do not, because a certificate would make $\mathbb{R}$ countable. That split is the formal statement that the continuum is display-tier, not foundation-tier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.