unitResidue_pow_closed
plain-language theorem explainer
If a distinction-orbit residue is coprime to the modulus N, every natural power of that residue stays coprime to N. Factorization and period-spectrum arguments cite this to keep powered orbit points inside the unit residues. The proof rewrites the unit-residue hypothesis to Nat.Coprime and applies Mathlib's left-power closure.
Claim. Let $N$ and $a$ be distinction-orbit naturals. If $a$ is a unit residue modulo $N$ (i.e. $\delta$-coprime to $N$, equivalently $\gcd(a^{\mathrm{toNat}}, N^{\mathrm{toNat}})=1$), then for every $k\in\mathbb{N}$ one has $\gcd\bigl((a^{\mathrm{toNat}})^k,\, N^{\mathrm{toNat}}\bigr)=1$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, equipped with a forward map toNat that reads off the iteration count as an ordinary natural number. Residues and moduli in this module are carried as DistinctionNat values and compared after that reading.
A residue representative $a$ is a unit residue modulo $N$ when it is $\delta$-coprime to $N$. The bridge lemma equates that predicate with ordinary Nat.Coprime on the underlying naturals: unit residue holds iff $\gcd(a^{\mathrm{toNat}}, N^{\mathrm{toNat}})=1$.
The local setting is the factorization layer of Primitive Recognition Calculus: unit residues are the intended carrier for finite multiplicative character theory on the distinction orbit, so the unit class must be closed under the monoid operations that appear in orbit powers and period spectra.
proof idea
Term-mode, two steps. First rewrite the hypothesis unitResidue N a along the bridge unitResidue_iff_nat_coprime, obtaining Nat.Coprime a.toNat N.toNat. Then apply Mathlib's Nat.Coprime.pow_left k to that coprimality fact, which yields Nat.Coprime (a.toNat ^ k) N.toNat directly. No case split on $k$ and no induction in this file.
why it matters
Closes unit residues under natural powers, the missing monoid piece beside the one-element and binary-product closures in the same module. Downstream, orbitPow_unitResidue invokes it after translating orbit powers back to toNat, so powered orbit points remain unit residues. The unit-group certificate structure also sits on this closure family, packaging display, identity, and multiplicative closure for the carrier used by finite multiplicative character theory.
In the Recognition stack this is pure foundation arithmetic: it does not touch J-cost, the forcing chain T5–T8, or physical constants. It supplies the algebraic hygiene needed before period spectra and character sums can be stated on the distinction orbit without leaving the unit class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.