residueAdd
plain-language theorem explainer
Defines residue-class addition on DistinctionNat orbits: add two orbit positions, then reduce modulo a nonzero modulus N. Anyone building modular arithmetic on the recognition orbit (factorization, residue certificates) cites this. The body is a one-line composition of native addition with the residue map.
Claim. For a nonzero orbit modulus $N$ and orbit positions $a,b$, the residue-level sum is the native residue of $a+b$ modulo $N$: $\mathrm{res}_N(a+b)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive Peano-like type with zero and successor, used as the native carrier for recognition orbits rather than bare naturals.
The residue map takes a nonzero modulus $N$ and an orbit position $a$ to the native remainder of $a$ modulo $N$. That remainder lives again in DistinctionNat, so modular arithmetic can stay on the orbit without leaving the recognition calculus.
This module sits in the factorization layer of PrimitiveRecognitionCalculus: residues and same-residue relations are the orbit-level stand-ins for classical modular arithmetic, later displayed back to ordinary toNat congruences.
proof idea
Pure definitional wrapper. Apply the residue map to the ordinary DistinctionNat sum $a+b$; no extra lemmas or tactics. Downstream theorems unfold this abbreviation and rewrite with residue_toNat and toNat_add.
why it matters
Gives the additive operation on residue classes needed for the residue-orbit layer. The immediate consumer is residueAdd_toNat_mod, which proves the display identity $(\mathrm{res}_N(a+b)).\mathrm{toNat}=(a.\mathrm{toNat}+b.\mathrm{toNat})\bmod N.\mathrm{toNat}$. That identity, together with the parallel multiplication and same-residue facts, feeds the ResidueOrbitCertificate structure that packages the whole residue-orbit layer as a Prop certificate.
In the broader Recognition stack this is scaffolding for arithmetic-from-logic: once residues behave like classical modular arithmetic on the orbit, factorization and chart-transition arguments can stay inside DistinctionNat before embedding back through the LogicNat comparison chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.