orbitPow_unitResidue
plain-language theorem explainer
If a residue class a is coprime to the modulus N in the native distinction arithmetic, every orbit power a^k remains coprime to N. Factorization and period-spectrum arguments cite this to keep multiplicative orbits inside the unit group. The proof is a short bridge: transport to ordinary naturals, apply the classical power-closure of coprimality, and transport back.
Claim. Let $N$ and $a$ be distinction-naturals. If $a$ is a unit residue modulo $N$ (equivalently, $\gcd(a,N)=1$ after reading off ordinary naturals), then for every distinction-natural exponent $k$ the orbit power $a^{\circ k}$ is again a unit residue modulo $N$.
background
In the Primitive Recognition Calculus factorization layer, arithmetic is carried by DistinctionNat (logic-native naturals) rather than bare Nat. The map toNat reads off the ordinary iteration count. Residues modulo a nonzero orbit modulus $N$ are the native remainders; a residue is a unit residue when it is invertible in the multiplicative monoid modulo $N$, characterized by coprimality after toNat.
Orbit powers are the δ-native exponential: orbitPow a 0 = 1 and orbitPow a (k+1) = (orbitPow a k) · a. The companion lemma orbitPow_toNat states that this agrees with ordinary exponentiation on the underlying naturals: $(a^{\circ k}).\mathrm{toNat} = a.\mathrm{toNat}^{k.\mathrm{toNat}}$.
The local module builds a period spectrum for unit residues: exponents that return a unit to $1$ modulo $N$, used to extract nontrivial factorizations from proper period divisors.
proof idea
Term-mode, three steps. Rewrite the goal with unitResidue_iff_nat_coprime so both hypothesis and conclusion become ordinary coprimality statements. Rewrite the powered residue via orbitPow_toNat, replacing the native orbit power by $a.\mathrm{toNat}^{k.\mathrm{toNat}}$. Finish by unitResidue_pow_closed on the transported hypothesis and $k.\mathrm{toNat}$, which is the classical fact that powers of a unit remain units (coprimes stay coprime under exponentiation).
why it matters
The sole downstream consumer is period_spectrum_certificate, whose field pow_preserves_unit is discharged exactly by this lemma: every orbit power of a unit residue stays a unit residue. That certificate packages the display law for orbit powers, unit preservation, and the extraction of a nontrivial factorization from a proper period divisor.
In the broader Recognition stack this sits in the foundation factorization path that turns multiplicative order data into arithmetic structure, upstream of mass-ladder and spectrum constructions. It is not itself a T0–T8 forcing step; it is bookkeeping that keeps the period spectrum inside $(\mathbb{Z}/N\mathbb{Z})^\times$ so period witnesses remain legitimate unit-group data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.