unitResidue_iff_nat_coprime
plain-language theorem explainer
A residue class representative a is a unit modulo N in the δ-layer exactly when the underlying natural numbers a.toNat and N.toNat are coprime. Anyone working on the native unit group, Euler periods, or period-gap factorization cites this bridge. The proof unfolds the unit-residue predicate and applies the existing δ-coprime-to-Nat equivalence.
Claim. For finite distinction orbits $N$ and $a$, the residue representative $a$ is a unit modulo $N$ (i.e., $\delta$-coprime to $N$) if and only if $\gcd(a^{\mathrm{toNat}}, N^{\mathrm{toNat}}) = 1$ in ordinary natural numbers.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, equipped with a verifier map toNat into Lean Nat. In the factorization layer, residues live on this orbit type rather than on bare naturals.
A residue representative is declared a unit modulo $N$ when it is $\delta$-coprime to $N$: the predicate unitResidue $N$ $a$ is definitionally coprime $a$ $N$. The Euclidean layer already proves that native $\delta$-coprimeness is equivalent to ordinary Nat.Coprime after toNat (coprime_iff_nat_coprime).
This module packages that equivalence under the unit-residue name so downstream unit-group and period arguments can stay in the $\delta$ vocabulary while still invoking Mathlib coprimeness facts.
proof idea
One-line term proof. Unfold unitResidue (which is definitionally coprime $a$ $N$), then apply the upstream lemma coprime_iff_nat_coprime $a$ $N$, which rewrites $\delta$-coprimeness as Nat.Coprime on the toNat images via gcd_toNat and the unit characterization of gcd $= 1$.
why it matters
This is the display bridge for the native unit group. unit_group_certificate records it as unit_display, and the closure lemmas unitResidue_one, unitResidue_mul_closed, and unitResidue_pow_closed all rewrite through it to reach Mathlib Nat.Coprime facts.
Downstream, Euler's theorem in the $\delta$ residue layer (eulerPeriod_returns_one) converts a unitResidue hypothesis into Nat.Coprime before applying the classical Euler exponent. orbitPow_unitResidue preserves unit status under orbit powers the same way. The even-period-gap factorization path (nontrivialFactorization_of_evenPeriodGapWitness) uses the forward direction to guarantee the witness base is positive and coprime, reducing period-based factoring to a single existence statement.
In the Recognition foundation this sits inside PrimitiveRecognitionCalculus factorization: arithmetic recovered from distinction orbits, not postulated as bare Nat. It does not itself touch T5–T8 or the J-cost, but it is infrastructure for period spectra that later feed recognition timing structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.