period_spectrum_certificate
plain-language theorem explainer
Packages the period-spectrum interface: orbit powers match ordinary natural powers, units stay units under powering, and a proper period-divisor yields a nontrivial factorization of N. Factorization and character-theory work in the primitive recognition calculus cites it. The proof is a three-field certificate assembly from existing lemmas.
Claim. There is a period-spectrum certificate: for all distinction-naturals $a,k$, the orbit power satisfies $(\mathrm{orbitPow}\,a\,k).\mathrm{toNat}=a.\mathrm{toNat}^{k.\mathrm{toNat}}$; if $a$ is a unit residue modulo $N$ then so is every orbit power of $a$; and any proper divisor extracted from a period witness for $N\neq 0$ produces a nontrivial factorization of $N$.
background
In the factorization layer of the primitive recognition calculus, integers are carried as distinction-naturals with a native residue and divisibility API. Orbit powering orbitPow is the iterated multiplicative action used to read periods of residues; its display theorem states that the underlying ordinary natural is just ordinary exponentiation.
A unit residue modulo $N$ is a residue coprime to $N$. The unit-group layer already shows that ordinary powers of unit residues remain units; the orbit-power version is the same fact transported through the display equality. A ProperDivisorFromPeriod witness packages a proper divisor of $N$ read off a period (nonzero, nonunit, and not equal to the modulus).
The certificate structure PeriodSpectrumCertificate is the Prop-level interface bundling display, unit preservation, and the extraction of a nontrivial factorization from such a period divisor. The module sits under Foundation factorization, importing the unit-group development.
proof idea
Three-field structure instance. The pow_display field is filled by the existing theorem orbitPow_toNat (induction on the exponent). The pow_preserves_unit field is discharged by orbitPow_unitResidue, which rewrites through the display equality and applies unit-residue power-closure. The period_divisor_extracts_factorization field is a direct application of period_divisor_to_nontrivialFactorization, itself a thin wrapper around nontrivial factorization from a proper divisor. No new arithmetic is proved here.
why it matters
This is the period-spectrum slot in the master factorization/character-theory certificate. Downstream, delta_factorization_character_theory_certificate assembles chart transition, residue orbit, unit group, and this period-spectrum certificate into one Prop. Without the period-to-factorization bridge, period readouts would not feed the δ-native factorization layer.
In the broader Recognition stack this is foundation scaffolding for character-theoretic factorization, not a forcing-chain landmark (T5–T8) itself. It closes the period-spectrum interface so master certificates can treat period extraction as a black box when building nontrivial factorizations from residue dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.