unitResidue_one
plain-language theorem explainer
The multiplicative identity of the distinction orbit is always a unit residue modulo any modulus N. Anyone assembling the residue unit group in the primitive recognition calculus cites this fact. The argument is a two-step rewrite to ordinary Nat coprimality of 1, then Mathlib's coprime-one lemma.
Claim. For every finite distinction orbit $N$, the orbit element $1$ is $\delta$-coprime to $N$. Equivalently, $1$ is a unit residue representative modulo $N$.
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. The orbit element written one satisfies one.toNat = 1.
In this module a residue representative $a$ is declared a unit modulo $N$ when it is $\delta$-coprime to $N$. That predicate is definitionally coprime a N, and the bridge lemma equates it with ordinary Nat.Coprime on the two toNat images. The local setting is the factorization layer of the primitive recognition calculus: building the multiplicative monoid of units in the residue ring before any physical constants appear.
proof idea
Term-mode, three lines. Rewrite the goal with the bridge unitResidue_iff_nat_coprime, then simplify the left factor by one_toNat so the goal becomes Nat.Coprime 1 N.toNat. Discharge by Mathlib's Nat.coprime_one_left. No case split on $N$ is required.
why it matters
This is the identity axiom for the residue unit structure. Downstream, the bundled identity one N : UnitResidue N takes its isUnit field from this theorem, and the certificate unit_group_certificate records one_is_unit := unitResidue_one alongside the display bridge and multiplicative closure. Without it the unit group of residues cannot be assembled as a Lean structure. In the broader Recognition stack this sits in Foundation arithmetic-from-logic scaffolding that later supports factorization and orbit divisibility; it does not yet touch the forcing chain T5–T8 or the J-cost, but it is a necessary monoid fact on the way there.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.