ratToNat_inj
plain-language theorem explainer
The explicit certificate map from rationals to naturals (Cantor-pair the integer certificate of the numerator with the denominator) is injective. Anyone building the forced tower ℕδ → ℤδ → ℚδ cites this. The proof is a short term chain: unpack the pairing equality, apply choice-free pairing injectivity and integer-certificate injectivity, then reassemble the rational by structure eta.
Claim. The map $\mathbb{Q}\to\mathbb{N}$ sending $q$ to the Cantor pair of the integer-to-natural certificate of $q$'s numerator with $q$'s denominator is injective: equal certificates imply equal rationals.
background
In the Primitive Recognition Calculus, a type is δ-forced when it carries an explicit injective certificate into ℕ. The module builds a choice-free tower of such certificates: naturals are self-certifying, integers use the parity encoding (nonnegatives to evens, negatives to odds), and rationals pair those pieces.
The local pairing dpair is the classical Cantor square pairing, redefined so injectivity avoids Mathlib's Classical.choice path through Nat.sqrt. Its injectivity lemma states that equal pairs force both coordinates equal, by tiling square blocks and ruling out cross-branch collisions arithmetically.
The integer certificate intToNat is already known injective. Structure-eta equality for ℚ (rat_eq_of) says two rationals with equal numerator and denominator are definitionally equal once the nonzero-denominator and reducedness proofs are irrelevant. Together these give a fully constructive rational certificate.
proof idea
Assume two rationals have the same ratToNat value. Unfolding, that equality is an equality of dpair applications on (intToNat num, den). Apply dpair_inj2 to split into numerator-certificate equality and denominator equality. Feed the former through intToNat_inj to recover numerator equality, then invoke rat_eq_of to conclude the rationals are equal. Pure term-mode chaining; no case splits at this layer.
why it matters
This injectivity is the last algebraic step before deltaForced_rat, which packages ⟨ratToNat, ratToNat_inj⟩ as the δ-forced witness for ℚ. Downstream doc-comment: "ℚ is δ-forced via the explicit paired certificate. This is the top of the forced tower constructed in the companion algebra paper (ℕδ → ℤδ → ℚδ). Choice-free."
In the Recognition framework the forced tower marks which number systems are recognition-native rather than display-tier. The same module immediately contrasts that ℝ admits no certificate (a certificate would force countability). The result therefore closes the discrete half of the foundation before continuum display is separated off. It sits under the Primitive Recognition Calculus rather than the T0–T8 forcing chain, but supplies the arithmetic substrate those later uniqueness results assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.