IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.UnitGroup
Defines the multiplicative monoid of residue classes coprime to a modulus N (units modulo N) inside the primitive recognition calculus factorization layer. Residues are units precisely when they are δ-coprime to N. Supplies closure under multiplication and powers, a bundled UnitResidue type with one and mul, and a UnitGroupCertificate. Downstream period-spectrum work imports this monoid structure.
claimA residue $r$ is a unit modulo $N$ when it is $\delta$-coprime to $N$. The set of such residues is closed under multiplication and under taking powers; it forms a monoid with identity $1$. The module packages this as a type $\mathrm{UnitResidue}$ with operations $\mathrm{one}$, $\mathrm{mul}$, and a certificate that the unit-group axioms hold.
background
This module sits in the factorization branch of the Primitive Recognition Calculus, under Foundation. It imports the residue-orbit layer, which tracks how residues move under the recognition dynamics modulo $N$.
A residue representative is declared a unit modulo $N$ exactly when it is $\delta$-coprime to $N$ (the recognition-native coprimality predicate). The predicate unitResidue and the equivalence unitResidue_iff_nat_coprime connect that notion to ordinary integer coprimality. Closure lemmas record that the unit residues are stable under multiplication and under powers, so they form a multiplicative monoid.
The bundled type UnitResidue carries the monoid operations one and mul (with value projections one_val, mul_val). UnitGroupCertificate / unit_group_certificate package the verified monoid (unit-group) structure for downstream use.
proof idea
Definition-and-closure module rather than a single deep theorem. The core predicate identifies units via $\delta$-coprimality; an iff lemma ties that to Nat.Coprime. Separate lemmas prove the set is closed under multiplication and under powers, and that $1$ is a unit. The bundled UnitResidue type and its one/mul operations are thin wrappers around those facts. The certificate assembles the monoid laws into one exportable object for importers.
why it matters in Recognition Science
Period-spectrum analysis (module PeriodSpectrum) imports this unit-group layer. Multiplicative order and period spectra only make sense on the units modulo $N$; without a certified monoid of $\delta$-coprime residues, orbit periods cannot be defined cleanly inside the factorization stack.
In the broader Recognition Science foundation, factorization of recognition dynamics modulo $N$ feeds the discrete skeleton that later supports the eight-tick octave (T7) and related forcing steps. This module is infrastructure: it does not itself force $\varphi$ or $D=3$, but it supplies the algebraic carrier on which period and spectrum statements are stated.
scope and limits
- Does not construct the full group of units as a Mathlib `Group`; it certifies a monoid of δ-coprime residues.
- Does not compute Euler totients, discrete logs, or explicit generators.
- Does not prove uniqueness of inverses beyond what the certificate records.
- Does not address continuous or real-modulus analogues; N is discrete.
- Does not derive physical constants or forcing-chain steps T5–T8.