period_divisor_to_nontrivialFactorization
plain-language theorem explainer
A proper-divisor certificate extracted from a period witness on a nonzero distinction natural N immediately yields a nontrivial factorization of N. Period-spectrum and physical-readout factoring both cite this bridge. The proof is a one-line application of the proper-divisor factorization lemma to the four divisor fields on the certificate.
Claim. Let $N$ be a nonzero distinction natural. Given a proper-divisor-from-period certificate for $N$ (a period witness at base $a$ and period $r$, together with a divisor $d$ that is nonzero, nonunit, not equal to $N$, and divides $N$), $N$ admits a nontrivial factorization.
background
Distinction naturals are the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, used throughout the primitive recognition calculus in place of ordinary $\mathbb{N}$ when the arithmetic must stay chart-independent.
A period witness records that some power of a base $a$ returns to the unit residue modulo $N$. The structure ProperDivisorFromPeriod packages such a witness with an explicit proper divisor $d$ of $N$. The divisor may arise from the classical $\gcd(a^{r/2}-1,N)$ route, but the structure stores the certificate rather than deriving the readout on the spot.
Upstream, nontrivialFactorization_of_proper_divisor is the reusable $\delta$-native endpoint: any proper nonunit divisor of nonzero $N$ supplies a nontrivial factorization. The present theorem is the period-spectrum face of that endpoint.
proof idea
One-line term proof. Unpack the four divisor fields on the proper-divisor-from-period certificate (nonzero, nonunit, not equal to the modulus, and divides $N$) and feed them, together with $N \neq 0$, into nontrivialFactorization_of_proper_divisor. No new arithmetic is performed.
why it matters
This is the extraction step that turns a period-spectrum readout into a factorization inside the primitive recognition calculus. Downstream, period_spectrum_certificate installs it as the period_divisor_extracts_factorization field of the period-spectrum interface certificate, and certifiedFactorReadout_to_nontrivialFactorization applies it to a certified physical factor readout by projecting to the factor witness.
In the broader RS stack the period spectrum sits on the eight-tick octave and the $\phi$-ladder (T6–T7): periods are read as discrete orbit returns, and factoring those returns is how composite distinction counts split. The theorem does not itself force $\phi$ or $D=3$; it only closes the divisibility bridge once a proper divisor has been certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.