Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodExistence

show as:
view Lean formalization →

Establishes that every unit residue class modulo N has a multiplicative period given by Euler's totient. The module packages the Euler exponent as an orbit position on the display, proves it is nonzero, and shows a^φ(N) ≡ 1 for units a. Downstream factorization certificates import this as the existence half of the period spectrum.

claimFor $N \ge 1$ and residue $a$ coprime to $N$, the Euler exponent $\varphi(N)$ is a positive multiplicative period: $a^{\varphi(N)} \equiv 1 \pmod{N}$. The module supplies a nonempty period witness and a named existence certificate for use in the factorization chain.

background

In the Primitive Recognition Calculus, factorization of recognition orbits is organized by a period spectrum: the discrete times at which a residue returns to the identity under multiplication modulo $N$. The upstream PeriodSpectrum module fixes the language of that spectrum; this module supplies the classical existence engine.

The central quantity is the Euler exponent of $N$, identified with the totient $\varphi(N)$ and treated as an orbit position on the display. For unit residues (classes coprime to $N$), Euler's theorem guarantees return to $1$ after $\varphi(N)$ steps. The eight-tick octave (forcing step T7) is the special case $N=8$ in the broader RS chain; here the argument is for general $N$.

Sibling definitions name the exponent, prove it is nonzero, record the return-to-one identity, and package a nonempty witness type plus a certificate structure for downstream import.

proof idea

The module is a short classical number-theory layer, not a deep RS derivation. It defines the period exponent as $\varphi(N)$, cites Mathlib for $\varphi(N) > 0$ when $N \ge 1$, and applies Euler's theorem to obtain $a^{\varphi(N)} \equiv 1 \pmod{N}$ for units $a$. Nonemptiness of the period-witness type is then immediate from that identity. A thin certificate wrapper bundles the statements for the MasterCertificate import path. No novel forcing or J-cost algebra appears here.

why it matters in Recognition Science

MasterCertificate imports this module to close the existence side of the factorization period story: without a guaranteed period for every unit residue, the spectrum cannot be certified complete. In the Recognition framework the period lattice underpins discrete tick structure; T7 forces the eight-tick octave as the fundamental closed chain, and general Euler periods supply the arithmetic backbone for composite displays. The certificate object is the handoff point into the factorization master bundle, so later uniqueness or minimality results can assume existence rather than reprove it.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)