IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodSpectrum
Defines δ-native orbit exponentiation on the unit group and packages period data into a spectrum certificate. A proper divisor of a period is converted into a nontrivial factorization witness. Downstream period-existence and period-factor modules import this layer. The content is mostly definitions and short inductive lemmas on orbit powers, plus the certificate construction.
claimOn the unit group of the recognition residue, define orbit powering $u^{\delta}$ by a discrete orbit exponent $\delta$, with the usual $u^{0}=1$ and $u^{n+1}=u\cdot u^{n}$ laws. A period witness records that some positive exponent returns the identity. From a proper divisor of such a period one obtains a nontrivial factorization certificate (the period spectrum certificate).
background
This module sits in the Primitive Recognition Calculus factorization stack, immediately above the unit-group layer. The ambient objects are multiplicative units of a recognition residue; periods are positive exponents that close an orbit back to the identity.
The central operation is orbit powering: exponentiation of a unit by a discrete orbit exponent $\delta$, written in the native $\delta$-language rather than bare $\mathbb{N}$. Supporting facts record the zero and successor recurrences, the bridge to ordinary toNat exponents, and compatibility with the unit residue.
A period witness is a structured proof that some positive exponent is a period. From a proper divisor of that period the module builds a nontrivial factorization, packaged as a period-spectrum certificate. That certificate is the hand-off object for later existence and factor arguments.
proof idea
Definition-heavy module, not a single deep theorem. orbitPow is introduced by the usual recursive clauses on the orbit exponent; zero, successor, toNat, and unit-residue lemmas are short inductive or rewriting facts. PeriodWitness and ProperDivisorFromPeriod are data wrappers. The nontrivial step is period_divisor_to_nontrivialFactorization, which turns a proper period divisor into a factorization witness, then re-exported as PeriodSpectrumCertificate / period_spectrum_certificate for downstream use.
why it matters in Recognition Science
Supplies the period-spectrum interface used by three factorization modules: FiniteMulCharacter, PeriodExistence, and PeriodFactor. In the Recognition forcing chain, discrete periods feed the eight-tick octave (T7) and the factorization of recognition residues that underwrite later mass and coupling ladders. Without a clean bridge from "period has a proper divisor" to "nontrivial factorization," existence and factor theorems cannot state their certificates. This file is that bridge: orbit arithmetic plus the spectrum certificate, nothing more.
scope and limits
- Does not prove that a period exists; only structures witnesses and divisors.
- Does not classify all periods or compute the eight-tick octave.
- Does not construct multiplicative characters; that is FiniteMulCharacter.
- Does not assert uniqueness of the factorization extracted from a divisor.
- Does not treat continuous or real exponents; only discrete orbit exponents.