coprime_iff_nat_coprime
plain-language theorem explainer
Native coprimality on DistinctionNat orbits is exactly ordinary Nat coprimality after the verifier map toNat. Anyone transporting Euclidean or residue arguments between the δ-orbit and Mathlib cites this bridge. The proof is a one-line simp unfolding object-level coprime as unit(gcd) and applying gcd_toNat with unit_iff_toNat_eq_one.
Claim. For finite distinction orbits $a,b$, the native predicate that $\gcd(a,b)$ is a multiplicative unit is equivalent to $\mathrm{Nat.Coprime}(|a|,|b|)$ after reading each orbit as a natural number via the iteration-count map.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive zero/succ type whose verifier representation toNat reads off the iteration count as a Lean Nat.
Native divisibility says $a$ divides $b$ when some orbit $k$ satisfies $a\cdot k=b$. The only multiplicative unit in the finite $\delta$-orbit is the one-step orbit; unit_iff_toNat_eq_one records that a unit is exactly an orbit with toNat = 1.
Object-level coprimality is defined by coprime a b := unit (gcd a b). The sibling gcd_toNat transports the native GCD to Nat.gcd, so the present lemma is the natural bridge between orbit coprimality and Mathlib's Nat.Coprime.
proof idea
One-line term-mode simp on three names: unfold coprime to unit (gcd a b), rewrite the GCD via gcd_toNat, then apply unit_iff_toNat_eq_one so the unit condition becomes equality of the transported GCD with $1$, which is the definition of Nat.Coprime.
why it matters
This is the transport hinge for the closed $\delta$-only Euclidean surface. Downstream, unitResidue_iff_nat_coprime is literally exact coprime_iff_nat_coprime; normalizeRatio_coprime reduces signed-rational normalization to Nat coprimality of numerator and denominator; coprime_divides_of_divides_mul_left uses it to move Euclid's lemma (if $a$ is coprime to $b$ and divides $b\cdot c$, then $a$ divides $c$) while keeping the statement native and confining Nat to the transport step. It also feeds orbit_euclidean_certificate, the package of divmod, remainder bounds, and GCD normalization on orbits. In the Recognition foundation this keeps arithmetic forced from distinction orbits rather than assumed as primitive Nat structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.