UnitResidue
plain-language theorem explainer
Bundles a finite-orbit integer with a proof it is δ-coprime to a fixed modulus N, giving the carrier type for residues invertible modulo N. Anyone building multiplicative characters, Euler totient counts, or the unit group on DistinctionNat cites this. It is a plain structure definition: value field plus the unitResidue predicate, no proof obligations beyond the field type.
Claim. For a fixed modulus $N$ in the finite distinction orbit, a unit residue is a pair $(a, h)$ where $a$ is again in that orbit and $h$ asserts that $a$ is $\delta$-coprime to $N$ (i.e., $\gcd(a,N)=1$ in the native sense).
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, used throughout the Primitive Recognition Calculus in place of ordinary $\mathbb{N}$ when one wants native, base-independent counting.
In the factorization layer, the native residue of $a$ modulo a nonzero orbit modulus $N$ is the remainder of $a$ by $N$. A residue representative is declared a unit modulo $N$ precisely when it is $\delta$-coprime to $N$ (the predicate unitResidue). That is the only invertibility notion available before a full ring structure is built.
The module sits under Factorization.UnitGroup and imports ResidueOrbit. Its purpose, per the structure doc-comment, is to supply the carrier for finite multiplicative character theory on these orbits.
proof idea
No proof body: this is a structure declaration. The first field is an element of DistinctionNat; the second is a proposition that the unit-residue predicate holds for that element relative to the parameter $N$. Downstream constructors (one, mul) inhabit the structure by supplying a value and discharging the coprimality field via the closedness lemmas unitResidue_one and unitResidue_mul_closed.
why it matters
This is the typed carrier on which the unit-group operations are defined. Downstream, one builds the identity unit residue (value = DistinctionNat.one), and mul multiplies two unit residues while preserving the unit predicate. The projection lemmas one_val and mul_val then expose the underlying orbit multiplication.
In the Recognition framework this is scaffolding for finite multiplicative character theory on distinction orbits: the algebraic surface needed before one can state Euler-type counts, Dirichlet characters, or residue-class Fourier analysis in RS-native arithmetic. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure orbit arithmetic supporting later factorization and recognition-stability arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.