one
plain-language theorem explainer
Packages the multiplicative identity as a unit residue modulo a distinction orbit N. Anyone assembling the finite unit group or multiplicative characters on residues will cite it. The construction is a structure instance: value is the native one-step orbit, and unit-hood is discharged by the coprimality lemma for one.
Claim. For each distinction number $N$, the multiplicative identity $1$ is a unit residue modulo $N$: its underlying value is the one-step orbit, and it satisfies the unit-residue predicate (equivalently, $\gcd(1,N)=1$).
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, used as the native carrier instead of ordinary naturals. In the orbit-divisibility layer, the native unit predicate asserts that an element equals the one-step orbit; nontrivial factorization requires both factors nonzero and non-unit.
Unit residues are the carrier for finite multiplicative character theory. A unit residue modulo $N$ is a pair: a DistinctionNat value together with a proof that it is a unit residue of $N$. The predicate is equivalent to ordinary coprimality of the underlying naturals. This definition sits in the factorization/unit-group module that builds that carrier and its monoid operations.
proof idea
Definitional structure instance, not a tactic proof. The value field is set to DistinctionNat.one. The isUnit field is filled by applying unitResidue_one, which rewrites the unit-residue predicate to nat-coprimality and invokes Nat.coprime_one_left on N.toNat.
why it matters
Supplies the monoid identity inside UnitResidue, the carrier the module advertises for finite multiplicative character theory. Sibling constructions (multiplication of unit residues, power-closure, and the unit-group certificate) need a canonical one to state associativity, identity laws, and certificate packing. In the Recognition foundation stack this is bookkeeping on the distinction orbit, not a forcing-chain step (T5–T8); it keeps residue arithmetic native to DistinctionNat so later character sums and factorization statements do not drop into plain Nat prematurely. No downstream theorems are wired yet in the graph; the immediate consumers are the in-module mul and certificate definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.