PeriodSpectrumCertificate
plain-language theorem explainer
Bundles three interface facts for the period-spectrum lane of δ-native factorization: orbit exponentiation matches ordinary powers on the Nat readout, powers of unit residues stay units, and a proper divisor extracted from a period witness yields a nontrivial factorization of N. Cited by the master factorization character-theory ledger and discharged by period_spectrum_certificate. Pure Prop structure; no proof body.
Claim. A period-spectrum certificate is the conjunction of: (i) for all orbit values $a,k$, the $\delta$-native power $a^{\circ k}$ satisfies $\mathrm{toNat}(a^{\circ k})=\mathrm{toNat}(a)^{\mathrm{toNat}(k)}$; (ii) if $a$ is coprime to $N$, then every $a^{\circ k}$ is coprime to $N$; (iii) whenever a period witness for $(N,a,r)$ is paired with a proper divisor of $N$ (nonzero, nonunit, not equal to $N$, and dividing $N$), one obtains a nontrivial factorization of $N$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero/succ), with toNat the verifier map into ordinary naturals. Factorization work is done in this δ-native arithmetic rather than on Lean Nat directly.
orbitPow a k is δ-native exponentiation: $a^{\circ 0}=1$ and $a^{\circ(k+1)}=a^{\circ k}\cdot a$. A residue is a unit modulo $N$ when it is δ-coprime to $N$ (unitResidue). A PeriodWitness records that some base $a$ has multiplicative order dividing $r$ in the unit group modulo $N$; ProperDivisorFromPeriod packages such a witness with an explicit proper divisor of $N$ (the classical $\gcd(a^{r/2}-1,N)$ style readout is allowed but not assumed derived here).
The local module sits under factorization character theory: period spectrum is the bridge from unit-group orbit data to concrete nontrivial factors via period divisors.
proof idea
Definitional Prop structure with three fields and no proof body. Inhabitants are assembled by supplying proofs of the three conjuncts. The sibling theorem period_spectrum_certificate fills them by orbitPow_toNat (Nat display of powers), orbitPow_unitResidue (units closed under orbit powers), and the lemma that a ProperDivisorFromPeriod certificate implies nontrivialFactorization N.
why it matters
This certificate is one slot of DeltaFactorizationCharacterTheoryCertificate, the master ledger for the factorization character-theory lane (alongside chart transition, residue orbit, unit group, and finite multiplicative characters). It isolates the period-spectrum interface so downstream factorization arguments can assume power display, unit stability, and period-to-factor extraction without re-proving them.
In Recognition Science terms this is foundation scaffolding for arithmetic-from-logic factorization, not yet a T0–T8 forcing step. It supports the path from δ-orbits and unit residues to nontrivial factors of $N$, which is the number-theoretic substrate later physics constants sit on. The companion period_spectrum_certificate theorem is the concrete discharge of this interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.