residue
plain-language theorem explainer
Native residue of an orbit element a modulo a nonzero distinction modulus N. It is the object-level Euclidean remainder on DistinctionNat, the base-neutral finite orbit of repeated distinction. Anyone working modular arithmetic on orbits (period-8 Clifford structure, discrete RCL uniqueness, factorization gaps) cites this. Proof is a one-line alias of remainder.
Claim. For a nonzero modulus $N$ in the distinction naturals and any $a$ in the same type, the residue of $a$ modulo $N$ is the object-level remainder of $a$ upon division by $N$.
background
DistinctionNat is the inductive type of base-neutral finite orbits of repeated distinction (K2.12): zero and successor, with decidable equality. It is the native carrier for discrete modular structure in the Primitive Recognition Calculus, before any embedding into ordinary naturals.
The Euclidean layer supplies an object-level division algorithm on that carrier. The remainder of $n$ by nonzero $d$ is the second component of the native divMod pair; it is the unique $r$ with $r < d$ in the orbit order such that $n = q\cdot d + r$ for some quotient $q$.
This module sits in the factorization layer of the Primitive Recognition Calculus and imports chart-transition structure. Residue is the named modular reduction used by congruence, residue addition/multiplication, and same-residue equivalence throughout the spine.
proof idea
One-line wrapper: residue N hN a is defined to be remainder a N hN. No extra proof obligations; the nonzero hypothesis is threaded unchanged into the Euclidean remainder.
why it matters
Residue is the modular primitive for the discrete Recognition spine. Downstream it appears in Bott periodicity (period-minimal residue classes modulo 8, tying to the eight-tick octave T7), discrete RCL uniqueness on GoldenInt sequences, even-period gap factorization witnesses, Clifford bridge structure, and curvature/cosmology kernels that need native modular reduction.
Without a named residue on DistinctionNat, congruence and period-minimality statements would re-open the Euclidean remainder at every call site. The definition keeps the factorization and Delta-spine layers uniform: same residue classes, residue rings under add/mul, and the period-8 residue filter used for Clifford rank identity all share one object-level reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.