PeriodWitness
plain-language theorem explainer
A period witness certifies that a unit residue a modulo nonzero N returns to 1 after r native multiplications, with r nonzero. Factorization and period-existence surfaces cite it as the minimal closing certificate for a residue orbit. It is a pure Prop structure with three fields and no proof body; minimality of r is deliberately not required.
Claim. Fix a nonzero modulus $N$ and distinction numbers $a,r$. A period witness for $(N,a,r)$ is the conjunction of three assertions: $r \neq 0$; $a$ is $\delta$-coprime to $N$ (a unit residue); and the native power $a^r$ has the same residue as $1$ modulo $N$.
background
In the primitive recognition calculus, integers are carried as DistinctionNat values and modular arithmetic is native: residues are compared by sameResidue, which equates the residue maps of two arguments modulo nonzero $N$. A residue is a unit when it is $\delta$-coprime to $N$ (unitResidue).
Native exponentiation is the recursive orbit power orbitPow a r: $a^0 = 1$ and $a^{k+1} = a^k \cdot a$. The period-spectrum module sits in the factorization layer of PrimitiveRecognitionCalculus; its job is to turn closed multiplicative orbits into certified arithmetic data (periods, then proper divisors) without smuggling classical number-theory readouts into the interface.
Upstream, the unit-group and residue-orbit modules supply the coprimality and congruence predicates; the orbit power is defined in this same module.
proof idea
No proof: this is a Prop-valued structure (definitional certificate). The three fields are exactly the mathematical conditions above. Downstream theorems inhabit the type by supplying exponent_nonzero, base_unit, and returns_one (for example via the Euler-exponent return lemma).
why it matters
This is the atomic certificate for the period-existence surface. period_exists_for_unitResidue builds a witness at the Euler exponent for every unit residue when $N \ge 2$; periodWitness_nonempty_of_unitResidue packages nonemptiness; PeriodExistenceCertificate records the universal return-to-one law.
It also feeds factorization: ProperDivisorFromPeriod pairs a witness with an exposed proper divisor (the classical $\gcd(a^{r/2}-1,N)$ route is allowed but not assumed derived), and CertifiedPeriodReadout stores an exponent together with its witness for physical readout. In RS terms this is the discrete order-finding step that later connects residue orbits to factor certificates, not yet the eight-tick or $\varphi$-ladder physics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.