periodExponent_ne_zero
plain-language theorem explainer
The Euler exponent of any distinction orbit of size at least 2 is a nonzero orbit position. Anyone building period witnesses for unit residues in the δ-residue layer cites this non-vanishing fact. The argument reduces a zero-equality through the display map and contradicts positivity of Euler's totient for n ≥ 2.
Claim. For every distinction-orbit integer $N$ with display $|N| \ge 2$, the Euler exponent $\varphi(|N|)$, viewed as an orbit position, is not the zero orbit.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive zero/successor type that serves as the native counting object of the primitive recognition calculus. The display map toNat reads off the iteration count as an ordinary natural number (with toNat zero = 0).
The period exponent of $N$ is defined as the classical Euler totient of the display, re-embedded as an orbit position: $\mathrm{ofNat}(\varphi(|N|))$. It is the candidate period length for multiplicative action in the residue layer modulo $N$. Residues themselves are native remainders in DistinctionNat.
This module assembles period existence for unit residues from Euler's theorem in the δ-residue layer. Before an exponent can appear in a period witness, it must be certified nonzero.
proof idea
Short term-mode proof by contradiction. Assume the period exponent equals zero. Apply congruence under the display map, then rewrite with the definition of the period exponent together with toNat_ofNat and toNat_zero, obtaining $\varphi(|N|)=0$. Positivity of the totient for $|N|\ge 1$ (here $\ge 2$ by hypothesis) is supplied by Nat.totient_pos; omega closes the contradiction.
why it matters
Direct input to period_exists_for_unitResidue, which packages a certified period witness for every unit residue modulo $N\ge 2$ with period equal to the Euler exponent. That parent theorem discharges its exponent_nonzero field exactly by this lemma (alongside the unit-residue hypothesis and the Euler return-to-identity fact).
In the Recognition framework this is arithmetic scaffolding for the residue-orbit factorization layer: nonzero Euler periods underwrite multiplicative return-to-identity before those dynamics are lifted toward recognition events and the eight-tick octave (T7). Without non-vanishing, the period-existence certificate cannot even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.