dpair_inj2
plain-language theorem explainer
The local Cantor pairing on natural numbers is injective: equal codes force equal coordinates. Anyone encoding pairs, or rationals via numerator and denominator, into ℕ without classical choice cites this. The proof is a four-way case split on the two if-branches, ruling out cross-branch collisions by square-block arithmetic and recovering both coordinates on the diagonal.
Claim. Let $\mathrm{pair}:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ be given by $\mathrm{pair}(x,y)=y^2+x$ if $x<y$, and $\mathrm{pair}(x,y)=x^2+x+y$ otherwise. If $a,b,c,d\in\mathbb{N}$ satisfy $\mathrm{pair}(a,b)=\mathrm{pair}(c,d)$, then $a=c$ and $b=d$.
background
In the Primitive Recognition Calculus, physically real quantities are forced to live on a discrete delta lattice. Encoding rationals into naturals is a bookkeeping step toward that forcing, and it must stay choice-free so later constructive arguments do not inherit classical residue.
The local pairing is defined by a single if: when the first coordinate is strictly smaller, the code sits in the lower half of the square block of side equal to the second coordinate; otherwise it sits in the complementary half of the square of side equal to the first. Explicitly, $\mathrm{pair}(a,b)=b^2+a$ if $a<b$, else $a^2+a+b$. The two branches tile each half-open square interval $[m^2,(m+1)^2)$.
Mathlib's standard Nat.pair is the same function, but its injectivity lemmas route through Nat.sqrt and pull Classical.choice. The local definition keeps reduction under control and lets injectivity be proved by elementary arithmetic alone.
proof idea
Split on whether $a<b$ and whether $c<d$ (four cases via Nat.lt_or_ge).
On each diagonal (both pairs in the same branch), rewrite the pairing definition, then trichotomize the shared large coordinate. Strict inequality of those coordinates produces a square-bound contradiction: $(m+1)^2=m^2+2m+1$ cannot fit inside the opposing square, discharged by ring, Nat.mul_le_mul, and omega. Equality of the large coordinates recovers the small one by omega.
Cross cases (one pair in each branch) are impossible. After rewriting both sides, trichotomy on the remaining free coordinates again yields square-block inequalities that omega refutes, or an immediate numeric contradiction after substitution. No external injectivity lemma is used; the argument is pure case analysis on the if-definition.
why it matters
This lemma is the pairing half of a choice-free injection from rationals into naturals. Its sole direct consumer is ratToNat_inj, which composes it with integer-to-nat injectivity and a structure-eta equality for reduced fractions: equal rational codes imply equal numerators and denominators, hence equal rationals.
Inside DeltaForced, that rational injection supports the claim that physically real quantities are delta-forced (the sibling bridge physicallyReal_iff_deltaForced). Keeping the pairing constructive matters for the broader Primitive Recognition Calculus stack, where later growth, eta-completion, and trace-logic arguments prefer not to smuggle classical choice through a routine encoding.
The result is pure arithmetic scaffolding rather than a forcing-chain landmark (T5–T8), but it closes a concrete classical leak at the foundation of the delta-forcing pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.