IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodExistence
Module proving that every unit residue class modulo N has a positive multiplicative period, realized by the Euler totient. It packages φ(N) as an orbit position (period exponent), shows it is nonzero, and that raising a unit to that power returns 1. Downstream factorization certificates import this existence package rather than re-proving Euler's theorem.
claimFor modulus $N \ge 1$ and residue $a$ coprime to $N$, the Euler totient $\varphi(N)$ is a positive integer period: $a^{\varphi(N)} \equiv 1 \pmod{N}$. The module records $\varphi(N)$ as the period exponent, proves it is nonzero, and supplies a nonempty witness of period existence for every unit residue, together with a named existence certificate.
background
In the Primitive Recognition Calculus factorization layer, multiplicative orbits of residues modulo $N$ are the combinatorial skeleton for period spectra. A unit residue is a class $a \bmod N$ with $\gcd(a,N)=1$. Classical Euler theory says the multiplicative group $(\mathbb{Z}/N\mathbb{Z})^\times$ is finite of order $\varphi(N)$, so every unit has finite order dividing $\varphi(N)$.
The sibling module PeriodSpectrum sets up the spectrum of candidate periods. This module isolates the existence half: a concrete positive exponent that always works. The doc-comment frames the Euler exponent of $N$ as an orbit position, namely the totient of the display modulus.
Notation: period exponent means $\varphi(N)$; returning to one means $a^e \equiv 1 \pmod{N}$ for that exponent $e$.
proof idea
Definition layer first: periodExponent is the totient of the modulus. Non-vanishing is the standard $\varphi(N) \ge 1$ for $N \ge 1$. The return-to-one fact is Euler's theorem for unit residues. Existence and nonempty witness lemmas package that theorem as a period witness in the factorization API. A certificate structure and its inhabitant bundle the lemmas for import by master certificates. Overall shape: thin Mathlib-backed Euler package, not a bespoke number-theory development.
why it matters in Recognition Science
MasterCertificate imports this module to discharge period-existence obligations inside the factorization certificate chain of Primitive Recognition Calculus. Without a guaranteed positive period for every unit residue, orbit and spectrum constructions upstream cannot close. In the broader Recognition forcing story, discrete periodic structure (eight-tick octave, T7) needs finite multiplicative return times on residue displays; this module supplies the classical arithmetic existence step those displays rely on. It does not itself force $\varphi$-values or link to $J$-cost uniqueness (T5); it only guarantees that unit orbits close.
scope and limits
- Does not compute explicit orders of individual units, only existence via $\varphi(N)$.
- Does not treat non-units; residues sharing a factor with $N$ are out of scope.
- Does not derive the eight-tick octave or $D=3$; pure modular arithmetic existence.
- Does not bound minimal periods or classify the period spectrum beyond existence.
- Does not connect totients to $J$-cost, $\phi$-ladder masses, or $\alpha$ bounds.