Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.UnitGroup

show as:
view Lean formalization →

Defines the multiplicative monoid of residue classes coprime to a fixed modulus N, packaged as units under the δ-coprimality relation from the residue-orbit layer. Supplies the UnitResidue carrier, closure under multiplication and powers, and a UnitGroupCertificate. Period-spectrum constructions import this to restrict dynamics to invertible residues.

claimA residue representative $r$ is a unit modulo $N$ when it is $\delta$-coprime to $N$. The set of such residues forms a multiplicative monoid (with identity $1$), closed under multiplication and powers; a certificate packages this monoid structure for downstream use.

background

In the Primitive Recognition Calculus factorization stack, residues live in orbits modulo a fixed $N$. The upstream ResidueOrbit module supplies the orbit and $\delta$-coprimality language used to decide invertibility.

This module isolates the units: a residue is a unit when it is $\delta$-coprime to $N$, equivalently when the underlying natural is coprime to $N$. The carrier UnitResidue is that subtype, with monoid operations one and mul that preserve the unit predicate, and lemmas that powers of units remain units.

The local setting is pure number-theoretic scaffolding inside Foundation: no physical constants yet, only the algebraic substrate needed before period spectra and recognition clocks are built.

proof idea

Mostly definitional and elementary monoid closure. The unit predicate is tied to natural coprimality by an iff lemma; identity and multiplication are shown to stay inside the subtype; power-closure follows by induction on the monoid operation. A thin certificate structure bundles the carrier and operations for import by later modules. No deep analytic argument; standard subtype-monoid packaging over the residue orbit.

why it matters in Recognition Science

PeriodSpectrum imports this module to restrict attention to invertible residues when extracting periodic structure from recognition orbits. Without a clean unit monoid, period and spectrum constructions would continually re-prove coprimality closure. In the broader RS foundation chain this sits under Primitive Recognition Calculus factorization: units are the invertible ticks that can generate full octaves and forcing-compatible clocks once the eight-tick and $D=3$ layers are attached higher up. It is infrastructure, not a forcing step itself.

scope and limits

used by (1)

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 (12)