toNat_inj
plain-language theorem explainer
Equal verifier Nat displays of two distinction-orbit positions force the positions themselves to be equal. Anyone transporting arithmetic or factorization facts between the δ-orbit and Lean Nat cites this injectivity. The proof applies the ofNat builder to both sides and rewrites with the ofNat∘toNat identity.
Claim. Let $a,b$ be positions on the distinction orbit $\mathrm{DistinctionNat}$. If their verifier displays agree, $a^{\mathrm{toNat}}=b^{\mathrm{toNat}}$ as ordinary natural numbers, then $a=b$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with constructors zero and succ, introduced as K2.12 in the Primitive Recognition Calculus. It is the native carrier for orbit arithmetic before any radix or place-value chart is chosen.
The verifier display toNat reads an orbit position as a Lean Nat by counting successors; the inverse builder ofNat reconstructs the orbit from a Nat. Upstream, ofNat_toNat (K4.5) states that transport from the δ-orbit to Lean Nat and back is the identity: ofNat (toNat n) = n for every orbit position n.
This module develops the arithmetic of that orbit (addition, cancellation, and the display bridge). Injectivity of the display is the missing half of the equivalence needed before factorization and residue facts can move freely between the two presentations.
proof idea
Term-mode, three steps. From a.toNat = b.toNat, apply congrArg DistinctionNat.ofNat to obtain ofNat (a.toNat) = ofNat (b.toNat). Rewrite both sides with the upstream identity ofNat_toNat, which collapses each side to a and b respectively. The rewritten equality is exactly a = b. No induction is needed here; the work was already done in ofNat_toNat.
why it matters
This is the injectivity half of the δ/Nat display equivalence. Downstream factorization modules use it constantly: two_six_product_eq_three_four applies it to exhibit the concrete factor-pair ambiguity $2\cdot 6=3\cdot 4$ on the orbit; nontrivialFactorization_of_proper_divisor and prime_divisor_is_coordinate_base rely on it when reading divisors back as orbit positions; toNat_ne_zero_of_ne_zero and the classical prime-coordinate transport close zero-tests and Mathlib factor lists through the same bridge. Sibling cancellation laws (add_left_cancel, add_right_cancel) sit immediately after it in the module.
In the Recognition framework it is bookkeeping rather than a forcing-chain step, but without it the period-readout factoring story and the claim that the readout is a complete factor oracle cannot move statements off Lean Nat back onto the native orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.