periodWitness_nonempty_of_unitResidue
plain-language theorem explainer
Every unit residue class modulo N (N ≥ 2) admits a nonempty type of certified period witnesses at the Euler exponent φ(N). Number theorists and RS factorization authors cite it to turn constructive period data into a Nonempty certificate. The proof is a one-line term wrapper that packages the existing PeriodWitness constructor.
Claim. Let $N$ and $a$ be distinction-naturals with $N \neq 0$, $N \ge 2$ in ordinary $\mathbb{N}$, and $a$ a unit residue modulo $N$. Then the type of period witnesses for $a$ modulo $N$ at exponent $\varphi(N)$ (Euler totient of the display of $N$) is nonempty.
background
In the Primitive Recognition Calculus factorization layer, residues live on distinction-naturals (orbit positions built from logic-nats via toNat). A unit residue means $a$ is invertible in the residue monoid modulo $N$: it is coprime to $N$ in the displayed naturals.
A period witness is a certified triple: a nonzero exponent $r$, a proof that the base is a unit residue, and a proof that the orbit power $a^r$ returns to the residue $1$ modulo $N$. Minimality is optional at this interface; the essential output is return-to-one at a nonzero exponent.
The period exponent of $N$ is the Euler totient $\varphi(N.{\rm toNat})$ re-embedded as a distinction-natural. Upstream, every unit residue is already known to return to one under that exponent (Euler's theorem in this discrete setting), and a full PeriodWitness structure is constructed from that fact.
proof idea
One-line term proof. The constructor of Nonempty is applied to the value produced by period_exists_for_unitResidue, which already assembles a PeriodWitness at periodExponent N from three pieces: nonzero Euler exponent (periodExponent_ne_zero), the given unit-residue hypothesis, and return-to-one (eulerPeriod_returns_one). No extra arithmetic is done here.
why it matters
This lemma is the Nonempty bridge between the constructive period witness and the module's period-existence certificate surface. Downstream, period_existence_certificate packages Euler return-to-one and period existence into a single certificate structure; its period_exists field is discharged by inhabiting Nonempty via this theorem.
In the Recognition framework the result sits in the arithmetic factorization of the primitive recognition calculus: unit residues generate finite multiplicative orbits whose periods are controlled by the totient. That discrete period structure feeds the eight-tick octave bookkeeping (T7) and the broader forcing chain's demand that recognition registers close after finitely many ticks. It does not itself force $D=3$ or the J-cost uniqueness (T5), but it supplies the certified finite-order data those layers assume when residues appear in factorization identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.