Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodSpectrum

show as:
view Lean formalization →

Defines δ-native orbit powering on unit residues and packages period data into spectrum certificates. A period witness yields a proper divisor and hence a nontrivial factorization when the period is composite. Downstream factorization and character modules import this layer to turn multiplicative periods into concrete factors. The development is mostly definitional scaffolding plus short inductive lemmas on the orbit power map.

claimOn the unit group of residues, define orbit powering $g^{\circ k}$ by a $\delta$-native orbit exponent $k$, with base cases $g^{\circ 0}=1$ and $g^{\circ(n+1)}=g\cdot g^{\circ n}$. A period witness is a positive integer $T$ with $g^{\circ T}=1$ in the unit residue. From a proper divisor of such a $T$ one obtains a nontrivial factorization. A period-spectrum certificate packages these data so that composite periods force nontrivial factors.

background

This module sits in the Primitive Recognition Calculus factorization stack, immediately above the unit-group layer. Residues that are units form a multiplicative monoid; the orbit of a unit under repeated multiplication is the natural place to read periods.

Orbit powering is the $\delta$-native exponential: iterate the group operation according to an orbit exponent rather than a bare natural number, with the usual zero and successor recurrences, and a comparison lemma that recovers ordinary toNat powering on unit residues. A period witness is then a positive exponent at which the orbit returns to the identity.

The factorization link is elementary number theory in this language: if $T$ is a period and $d$ is a proper divisor of $T$, the corresponding intermediate power is a nontrivial factor of the ambient integer (or of the order data carried by the residue). The spectrum certificate is the bundled form of that implication used by later modules.

proof idea

Definition-heavy module. Orbit power is introduced by recursion on the exponent (zero/succ), then related to ordinary natural powering on unit residues by a short comparison lemma. Period witnesses and proper-divisor-from-period are structure/Prop packages. The bridge lemma period_divisor_to_nontrivialFactorization unpacks a proper divisor of a witnessed period into a nontrivial factorization certificate. The top-level period_spectrum_certificate assembles those pieces into a single reusable certificate object. No deep analytic argument; the work is inductive bookkeeping and packaging for importers.

why it matters in Recognition Science

Period spectra are the bridge from multiplicative order data on unit residues to concrete integer factorizations inside the Recognition factorization pipeline. Three downstream modules import this file: FiniteMulCharacter (characters on finite multiplicative groups need controlled periods), PeriodExistence (existence of periods must land on the spectrum certificate), and PeriodFactor (extracts factors from periods). In the broader RS foundation, factorization of orders and periods feeds the discrete octave and ladder bookkeeping that later forces the eight-tick structure and related arithmetic constraints. Without a clean period-to-factor map, those later steps cannot cite a single certificate object.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)