ProperDivisorFromPeriod
plain-language theorem explainer
Packages a certified period witness for modulus N with a proper divisor of N exposed by that period data. Factorization and physical-readout layers cite it as the minimal certificate that a period finder actually produced a nontrivial factor. It is a pure data structure: fields record the witness, the divisor, and the four proper-divisor side conditions.
Claim. For nonzero modulus $N$ and orbit elements $a,r$, a proper-divisor-from-period certificate is a period witness (nonzero exponent $r$ returning the unit residue of $a$ to $1$ modulo $N$) together with a divisor $d$ of $N$ such that $d \neq 0$, $d$ is not a unit, and $d \neq N$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (the δ-native stand-in for natural numbers). Native divisibility says $a$ divides $b$ when some orbit product recovers $b$; the only multiplicative unit is the one-step orbit.
A period witness certifies a nonzero exponent $r$ such that the orbit power of a unit residue $a$ returns to $1$ modulo nonzero $N$. Minimality of $r$ is optional at the interface; the essential output is that return-to-one fact.
This module sits in the factorization/period-spectrum layer: period data is not automatically a factor. Classical number theory would often take $\gcd(a^{r/2}-1,N)$; here the structure stores an explicit proper-divisor certificate rather than deriving the readout inside the type.
proof idea
No proof body: this is a structure definition (data certificate). The fields are the period witness, the candidate divisor, and four propositions: nonzero, non-unit, not equal to the modulus, and native divisibility of $N$. Downstream theorems read those fields and discharge factorization obligations from them.
why it matters
This is the hand-off type between period finding and δ-native factorization. The theorem period_divisor_to_nontrivialFactorization consumes one such certificate and obtains a nontrivial factorization of $N$ via the proper-divisor lemma. CertifiedFactorReadout in the physical period-readout module requires exactly this structure as its factor_witness, so any physical period-finder interface must produce it.
In the Recognition stack this keeps period-spectrum claims honest: a period alone does not factor $N$; only a period plus an exposed proper divisor does. That separation matters for later spectrum and readout certificates that assemble factorization evidence without smuggling classical gcd steps into the interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.