divides_antisymm
plain-language theorem explainer
Antisymmetry of native divisibility on the finite distinction orbit: if a divides b and b divides a, then a equals b. Cited by the orbit-divisibility certificate and by reduced-sign canonical denominator uniqueness. The proof is a short transport of Nat.dvd_antisymm through the injective toNat display and the native/display divisibility equivalence.
Claim. Let $a,b$ be positions in the finite distinction orbit $\mathrm{DistinctionNat}$. If $a$ divides $b$ and $b$ divides $a$ in the native sense (each is a multiplicative multiple of the other by some orbit position), then $a=b$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the native carrier for orbit arithmetic in the Primitive Recognition Calculus.
Native divisibility is defined existentially: $a$ divides $b$ when there exists an orbit position $k$ with $a\cdot k=b$. The display map $\mathrm{toNat}$ sends orbit positions to ordinary naturals. Upstream, $\mathrm{toNat}$ is injective (equal Nat displays come from equal orbit positions), and native divisibility is equivalent to ordinary Nat divisibility of the displays.
This module builds the multiplicative order structure on that orbit so later PRC cost and ratio uniqueness arguments can reason natively rather than only after display.
proof idea
Term-mode transport. Apply injectivity of $\mathrm{toNat}$ so it suffices to prove equality of the Nat displays. Convert both native divisibility hypotheses via the iff that native divides is equivalent to Nat divides on displays, then invoke Mathlib's $\mathrm{Nat.dvd_antisymm}$ on those two Nat divisibility facts.
why it matters
Closes the antisymmetry leg of the native divisibility preorder so the orbit divisibility surface can be certified as a coherent structure. Downstream, $\mathrm{orbit_divisibility_certificate}$ packages display equivalence, reflexivity, and transitivity; antisymmetry is the remaining order axiom that makes mutual divisibility imply equality of orbit positions.
Also used in $\mathrm{PRCReducedSignCanonical_den_eq_of_crossEq}$, which forces equal denominators for reduced-sign-canonical ratio orbits under cross-equality. That step needs mutual divisibility of denominators to collapse to identity on DistinctionNat, not merely on displayed Nats.
In the broader RS foundation this is pure orbit arithmetic scaffolding under Primitive Recognition Calculus, not a forcing-chain (T0–T8) landmark itself; it keeps later uniqueness proofs native to the $\delta$-orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.