period_existence_certificate
plain-language theorem explainer
Packages Euler's theorem and period-witness existence for unit residues in the distinction-number residue layer into one certificate surface. Anyone wiring the δ-factorization character-theory master certificate cites this. The proof is two short introductions that discharge the certificate fields by the matching lemmas.
Claim. A period-existence certificate holds: (i) for every nonzero modulus $N$ and unit residue $a$, the orbit power $a$ raised to the Euler period exponent of $N$ is the identity residue modulo $N$; (ii) if moreover $N\ge 2$, a period witness of that same exponent exists for $a$.
background
In the Primitive Recognition Calculus factorization layer, distinction numbers carry a residue arithmetic modulo a nonzero modulus $N$. A unit residue is one coprime to $N$; the period exponent is the Euler totient of $N.toNat$. Orbit powers iterate the residue multiplicatively, and same-residue compares two distinction numbers in that layer.
Upstream, Euler's theorem in the δ residue layer states that a unit residue raised to the Euler exponent returns to the identity residue. A companion result packages the concrete period as a nonempty PeriodWitness once $N\ge 2$. The local module assembles those facts into a single Prop-valued certificate surface for downstream factorization certificates.
proof idea
Certificate assembly by field. The first field introduces $N$, $a$, and the nonzero and unit-residue hypotheses, then applies eulerPeriod_returns_one. The second field introduces the same data plus the $N\ge 2$ bound and applies periodWitness_nonempty_of_unitResidue, itself a one-line Nonempty wrapper around the constructive period-existence lemma for unit residues. No new arithmetic is proved here.
why it matters
Closes the period-existence surface of the factorization stack and is consumed by the δ-factorization character-theory master certificate, which bundles chart transition, residue orbit, unit group, and period spectrum. Period closure for unit residues is the arithmetic reason residue orbits can return to the identity, the discrete-period theme that later meets the eight-tick octave (T7) in the forcing chain. Without this certificate the master character-theory surface cannot be inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.