dpair
plain-language theorem explainer
Local Cantor pairing of two naturals into one natural, branched on a < b. Defined in-house so injectivity can be proved without Classical.choice (Mathlib's Nat.pair pulls choice via Nat.sqrt). Downstream certificates that embed rationals into naturals for the delta-forced development cite this encoding. The body is a pure if-definition.
Claim. For $a,b\in\mathbb{N}$, the pairing is $\langle a,b\rangle = b^2+a$ if $a<b$, and $\langle a,b\rangle = a^2+a+b$ otherwise. This is the classical Cantor pairing, written so its case split is explicit.
background
The module develops the claim that physically real quantities are forced to live on a discrete delta ladder. To push that claim down to rationals and integers, one needs an explicit, choice-free injection $\mathbb{Q}\to\mathbb{N}$ (and $\mathbb{Z}\to\mathbb{N}$). Pairing is the standard tool: encode two naturals as one.
Mathlib already has Nat.pair, which is the same arithmetic function. Its injectivity lemmas, however, route through Nat.sqrt and thereby through classical choice. The Recognition stack wants constructive certificates, so this module redefines the pairing with an explicit if a < b branch whose injectivity can be discharged by elementary case analysis on square blocks $[m^2,(m+1)^2)$.
Sibling infrastructure includes intToNat (an injection $\mathbb{Z}\to\mathbb{N}$) and the composite ratToNat, which pairs the forced numerator with the denominator.
proof idea
Pure definition: no proof obligations. The formula is the standard Cantor pairing written with a single comparison. When $a<b$ the code lands in the lower triangle of the $b$-th square block as $b^2+a$; otherwise it lands as $a^2+a+b$. Downstream injectivity (dpair_inj2) will case on the two branches and show the blocks tile $\mathbb{N}$ without overlap.
why it matters
This is the encoding primitive for the delta-forced chain in PrimitiveRecognitionCalculus.DeltaForced. Immediate consumers are dpair_inj2 (choice-free injectivity), ratToNat (certificate $\mathbb{Q}\to\mathbb{N}$ by pairing intToNat q.num with q.den), and ratToNat_inj (which reduces to dpair_inj2 plus intToNat_inj).
Without a constructive pairing, the later theorems that every physically real rational is delta-forced would either stay classical or fail to typecheck in the choice-free fragment. The definition itself is not a forcing step (T0–T8), but it is the bookkeeping hinge that lets those forcing results reach $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.