IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ResidueOrbit
Defines native residues of integers modulo a nonzero orbit modulus N, together with the equivalence relation of sharing a residue class. Supplies the additive and multiplicative structure on residue classes and the basic congruence lemmas. Downstream unit-group and factorization work cites this layer for modular arithmetic on orbit charts. Mostly definitional scaffolding with elementary congruence proofs.
claimFor nonzero orbit modulus $N$ and integer $a$, the native residue $\mathrm{res}_N(a)$ is the representative of $a$ in $\mathbb{Z}/N\mathbb{Z}$. Write $a \equiv b \pmod{N}$ when $\mathrm{res}_N(a)=\mathrm{res}_N(b)$. The relation is an equivalence compatible with addition and multiplication, inducing well-defined operations $+_N$ and $\cdot_N$ on residues.
background
This module sits in the factorization layer of Primitive Recognition Calculus, immediately above chart transitions. Orbit moduli $N$ label discrete periods on recognition charts; residues are the native coordinates of an integer relative to such a period.
The core objects are the residue map sending $a$ to its class modulo $N$, and the relation of sharing the same residue. That relation is proved reflexive, symmetric, and transitive, and is characterized by ordinary modular equality of the underlying natural numbers. Addition and multiplication of residues are defined so that they commute with reduction modulo $N$.
The setting is elementary modular arithmetic specialized to the orbit-modulus language used by later factorization and unit-group constructions. No Recognition-cost or $J$-functional structure appears here; the module is pure discrete bookkeeping for chart coordinates.
proof idea
Definition module with short congruence lemmas. Residues and the same-residue relation are introduced definitionally. Reflexivity, symmetry, and transitivity of same-residue follow from the corresponding properties of equality after reduction modulo $N$. Compatibility with addition and multiplication is the standard fact that $a\equiv a'$ and $b\equiv b'$ imply $a+b\equiv a'+b'$ and $ab\equiv a'b'$ mod $N$. The induced residue operations are checked by reducing the toNat representatives modulo $N$. No deep algebraic machinery is required.
why it matters in Recognition Science
Unit-group constructions in the factorization stack import this module to obtain modular coordinates on orbit charts. Residues supply the ambient additive and multiplicative monoid in which units (invertible residue classes) are later carved out. Without a stable residue layer, chart transitions cannot be composed with modular arithmetic, and the discrete factorization of recognition periods stalls.
In the broader Recognition foundation this is infrastructure rather than a forcing-chain step: it does not touch $J$-uniqueness, $\varphi$, the eight-tick octave, or $D=3$. It does, however, make the discrete side of Primitive Recognition Calculus usable for later number-theoretic arguments about periods and invertible chart elements.
scope and limits
- Does not define units or invertibility in the residue monoid.
- Does not treat zero or non-orbit moduli; $N$ is assumed nonzero.
- Does not connect residues to $J$-cost, $\varphi$-ladders, or physical constants.
- Does not prove unique factorization or Chinese-remainder decompositions.
- Does not address continuous chart geometry beyond discrete reduction mod $N$.
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