periodExponent
plain-language theorem explainer
Maps a distinction-orbit modulus N to Euler's totient φ(N), re-embedded as an orbit position. Anyone proving period existence or Euler's theorem in the δ-residue layer cites this as the canonical period exponent. The body is a two-map wrapper: display N as Nat, take Mathlib totient, rebuild the orbit.
Claim. For a distinction-orbit position $N$, the period exponent is $\varphi(N^{\mathrm{disp}})$ re-encoded as a distinction-orbit position, where $\varphi$ is Euler's totient and $N^{\mathrm{disp}}$ is the ordinary natural-number display of $N$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, isomorphic to the verifier naturals via toNat / ofNat. Those maps are pure display bridges; arithmetic lives on Nat, then returns to the orbit language.
This module sits in PrimitiveRecognitionCalculus Factorization PeriodExistence, which imports the period spectrum and builds certificates that unit residues eventually return to the identity residue under orbit powering. The classical tool for that return is Euler's totient: for modulus $m\ge 1$, $\varphi(m)$ counts units mod $m$, and $a^{\varphi(m)}\equiv 1\pmod{m}$ when $\gcd(a,m)=1$.
periodExponent is the orbit-native packaging of that exponent: read N with toNat, apply Nat.totient, wrap with ofNat.
proof idea
Definitional one-liner, not a proof. Compose three existing maps: DistinctionNat.toNat (verifier display), Mathlib Nat.totient, and DistinctionNat.ofNat (rebuild the orbit). No lemmas are invoked at the definition site; downstream theorems unfold this abbreviation and reason on the Nat totient.
why it matters
Supplies the concrete exponent used by every period-existence result in this file. eulerPeriod_returns_one states Euler's theorem in the δ residue layer: a unit residue raised to this exponent returns to the identity residue. period_exists_for_unitResidue packages that return, plus non-vanishing of the exponent for $N\ge 2$, into a PeriodWitness. periodWitness_nonempty_of_unitResidue and the PeriodExistenceCertificate structure then surface the whole package as a Prop certificate.
In the Recognition forcing chain this is infrastructure for discrete period structure (the eight-tick octave at T7 is the physical landmark that period existence eventually supports). It does not itself force period 8; it only names the classical Euler exponent inside the orbit calculus so later factorization and spectrum results can cite a single object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.