PeriodExistenceCertificate
plain-language theorem explainer
Prop bundle certifying period existence for unit residues in δ-native arithmetic: the Euler totient exponent returns every unit residue to 1 mod N, and for N≥2 a PeriodWitness at that exponent is nonempty. Downstream character-theory and factorization ledgers cite it as the period-existence surface. Pure interface structure; no proof body.
Claim. A period-existence certificate asserts two facts. (1) For every nonzero modulus $N$ and every unit residue $a$ modulo $N$, the orbit power $a^{\varphi(N)}$ is residue-equal to $1$ modulo $N$. (2) Whenever $N\ge 2$ and $a$ is a unit residue modulo $N$, there exists a period witness for $a$ at the Euler exponent $\varphi(N)$ (a nonzero exponent returning the unit residue to $1$).
background
In the primitive recognition calculus, natural numbers appear as DistinctionNat (orbit positions built from identity and step). Residues modulo a nonzero $N$ are compared by native residue equality. A residue representative $a$ is a unit modulo $N$ when it is δ-coprime to $N$.
Orbit exponentiation is the δ-native power map: iterate multiplication of $a$ by itself along an orbit exponent. The period exponent of $N$ is the Euler totient of its display value, re-embedded as a distinction natural. A period witness packages a nonzero exponent $r$, a unit base, and the return-to-one fact $a^r \equiv 1 \pmod N$ in residue language. Minimality of $r$ is optional at this interface.
This module sits in the factorization lane of the foundation stack, importing the period-spectrum layer that defines witnesses and orbit powers.
proof idea
Definitional Prop structure with no proof body. It only names two fields that later theorems must supply: the Euler return-to-one statement for all unit residues, and nonempty existence of a period witness at the totient exponent when $N\ge 2$. The inhabiting theorem period_existence_certificate fills both fields by applying the sibling lemmas eulerPeriod_returns_one and the witness-nonemptiness argument for unit residues.
why it matters
This certificate is the period-existence surface of the factorization character-theory lane. The master ledger DeltaFactorizationCharacterTheoryCertificate aggregates chart transition, residue orbit, unit group, period spectrum, and finite multiplicative character certificates; period existence is the bridge from unit-group structure to a concrete Euler exponent that closes orbits back to 1.
In Recognition Science terms, closed residue orbits under the eight-tick and factorization stack supply the discrete periods that later force octave structure (T7) and related arithmetic constraints. The structure itself does not force those landmarks; it only freezes the interface that the inhabiting theorem and the master certificate consume.
Open work sits one level up: discharging the full master certificate and connecting period spectrum to finite multiplicative characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.