IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ResidueOrbit
Defines the native residue of an integer a modulo a nonzero orbit modulus N, together with the congruence relation sameResidue and the induced addition and multiplication on residue classes. Factorization and unit-group arguments in the Primitive Recognition Calculus cite this layer whenever they reduce statements mod N. The module is definitional: residues, equivalence lemmas, and ring operations on classes.
claimFor nonzero orbit modulus $N$ and integer $a$, the native residue $\mathrm{res}_N(a)$ is the canonical representative of $a$ modulo $N$. Write $a \equiv b \pmod{N}$ when $\mathrm{res}_N(a)=\mathrm{res}_N(b)$. This relation is an equivalence compatible with addition and multiplication, and the residue classes carry well-defined operations $+_N$ and $\cdot_N$ with $\mathrm{toNat}(x+_N y)\equiv \mathrm{toNat}(x)+\mathrm{toNat}(y)\pmod{N}$.
background
In the Primitive Recognition Calculus factorization stack, orbit moduli are the discrete periods that appear when recognition charts are reduced along cyclic factors. ChartTransition supplies the chart-change infrastructure; this module installs the arithmetic of residues relative to a fixed nonzero modulus $N$.
The central objects are the native residue map (sending $a$ to its representative mod $N$), the predicate sameResidue (congruence of two integers mod $N$), and the induced binary operations residueAdd and residueMul on residue values. Standard facts are recorded: sameResidue is reflexive, symmetric, and transitive; it is compatible with $+$ and $\cdot$; and converting a residue sum back to a natural recovers ordinary addition modulo $N$.
Notation is RS-native but mathematically ordinary modular arithmetic: residues live in a finite carrier of size $N$, and all subsequent unit-group and factorization lemmas treat that carrier as $\mathbb{Z}/N\mathbb{Z}$.
proof idea
Definition module with supporting lemmas, not a single theorem. residue and the sameResidue relation are introduced first; residue_toNat and sameResidue_iff_mod_eq connect them to ordinary modular equality. Equivalence properties (refl, symm, trans) and compatibility (sameResidue_add, sameResidue_mul) are proved by reducing to Mathlib modular arithmetic. residueAdd and residueMul package the induced operations; residueAdd_toNat_mod records the expected congruence for the sum.
why it matters in Recognition Science
UnitGroup imports this module, so every later statement about multiplicative units of residue classes, invertibility mod $N$, and factorization of recognition orbits sits on these definitions. In the broader Foundation chain, discrete orbit periods feed the eight-tick octave structure (T7) and the chart-factorization path that isolates self-similar scales; clean residue arithmetic is the bookkeeping layer those arguments need. Without a native residue type and congruence lemmas, unit-group and factorization developments would repeatedly re-prove modular facts inline.
scope and limits
- Does not construct the multiplicative unit group or prove invertibility criteria.
- Does not choose or force a specific orbit modulus $N$ from physics.
- Does not address continuous chart transitions beyond the imported ChartTransition layer.
- Does not claim uniqueness of residue representatives beyond the native map defined here.
- Does not connect residues to mass ladders, $J$-cost, or coupling constants.
used by (1)
depends on (1)
declarations in this module (15)
-
def
residue -
def
sameResidue -
theorem
residue_toNat -
theorem
sameResidue_iff_mod_eq -
theorem
sameResidue_refl -
theorem
sameResidue_symm -
theorem
sameResidue_trans -
theorem
sameResidue_add -
theorem
sameResidue_mul -
def
residueAdd -
def
residueMul -
theorem
residueAdd_toNat_mod -
theorem
residueMul_toNat_mod -
structure
ResidueOrbitCertificate -
theorem
residue_orbit_certificate