period_exists_for_unitResidue
plain-language theorem explainer
Every unit residue modulo N (with N at least 2) admits a certified period witness whose exponent is the Euler totient of N. Anyone building the period spectrum or unit-group orbit calculus in the primitive recognition layer cites this. The proof is a three-field structure term: nonzero totient, the unit hypothesis, and Euler return-to-one.
Claim. Let $N$ and $a$ be distinction naturals with $N \neq 0$ and ordinary value $N \ge 2$. If $a$ is a unit residue modulo $N$ (i.e., $\delta$-coprime to $N$), then the Euler exponent $\varphi(N)$ is a period witness for $a$: it is nonzero, $a$ is a unit, and $a^{\varphi(N)}$ returns to the identity residue modulo $N$.
background
In the primitive recognition calculus, integers are carried as DistinctionNat orbit positions; toNat reads the iteration count into ordinary Nat. Residues live in the $\delta$-layer: a representative $a$ is a unit modulo $N$ when it is coprime to $N$.
A PeriodWitness packages the essential period data for a base $a$ and exponent $r$: $r \neq 0$, $a$ is a unit residue, and the orbit power $a^r$ is the same residue as $1$ modulo $N$. Minimality is optional at this interface; existence of some returning exponent is the load-bearing claim.
The candidate exponent is the Euler totient of the display of $N$, re-embedded as a distinction natural (periodExponent). Upstream, eulerPeriod_returns_one is Euler's theorem in this layer: every unit residue raised to that totient returns to the identity residue. Separately, periodExponent_ne_zero records that $\varphi(n) > 0$ whenever $n \ge 2$.
proof idea
Term-mode construction of the PeriodWitness structure. The three fields are filled directly:
exponent_nonzerobyperiodExponent_ne_zerofrom the hypothesis $N.\mathrm{toNat} \ge 2$;base_unitby the given unit-residue hypothesis;returns_onebyeulerPeriod_returns_one, which rewrites into ordinary modular arithmetic and applies coprimality plus Euler's theorem onNat.
No further case analysis; the structure is inhabited once those three facts are supplied.
why it matters
This is the existence half of the period-existence surface for unit residues: every coprime base has a concrete, certified returning exponent equal to $\varphi(N)$. Downstream, periodWitness_nonempty_of_unitResidue is the one-line Nonempty wrapper around this term, and the module's PeriodExistenceCertificate packages the surface for export.
In the broader Recognition stack this sits in Foundation factorization, feeding the period spectrum used by orbit and unit-group reasoning. It is classical number theory internalized to the distinction-nat residue layer, not yet the eight-tick octave (T7) or spatial dimension forcing (T8); those consume period structure later. Closing this existence step lets later modules treat period witnesses as available data rather than open hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.