unitResidue
plain-language theorem explainer
A residue representative a is a unit modulo N exactly when a is δ-coprime to N (gcd is a unit). Anyone working the multiplicative residue layer cites this: finite characters, Euler-period existence, and even-period gap witnesses for factorization. The body is a one-line alias of object-level coprimality on distinction-naturals.
Claim. For distinction-naturals $N$ and $a$, $a$ is a unit residue modulo $N$ if and only if $a$ is object-level coprime to $N$, i.e. $\gcd(a,N)$ is a unit in the distinction-nat sense.
background
The ambient carrier is DistinctionNat: the base-neutral finite orbit of repeated distinction (K2.12), an inductive copy of the naturals used throughout the primitive recognition calculus so that residue and orbit constructions stay object-level rather than classical Nat.
Object-level coprimality is the predicate coprime a b := unit (gcd a b). A residue class representative is then declared a unit modulo $N$ precisely when that coprimality holds against the modulus. This sits in the factorization layer that builds multiplicative structure on residues (orbits under multiplication, periods, characters) without leaving the δ-native arithmetic.
The module imports the residue-orbit infrastructure; the local goal is to name the unit condition once so every later certificate (period return to 1, character multiplicativity, even half-period gaps) can quantify over the same Prop.
proof idea
Definitional one-liner: the predicate is definitionally equal to object-level coprimality of $a$ with $N$. No tactics, no lemmas unfolded beyond the alias itself. Downstream proofs treat it as the unit-membership gate and discharge it via the existing gcd/unit API on distinction-naturals.
why it matters
This is the gate predicate for the multiplicative monoid of residues. EvenPeriodGapWitness requires base_unit : unitResidue N base so that the even full period and half-power avoidance of $\pm 1$ are stated only for units, matching the configuration Shor-style period finding needs after period recovery.
Finite multiplicative characters are defined and certified only on unit residues: multiplicativity of the principal character, scaled list sums, and non-principal orthogonality all take unitResidue hypotheses on the multiplier and on list members. Period-existence certificates (eulerPeriod_returns_one, PeriodExistenceCertificate) likewise restrict to units so that some power returns to the identity in the residue monoid.
In the Recognition stack this is scaffolding for the factorization/period side of the primitive calculus, not a T0–T8 forcing step, but it is the shared interface those factorization theorems hang on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.