sameResidue_add
plain-language theorem explainer
Residue equality modulo a nonzero distinction orbit is compatible with addition: if a ≡ b and c ≡ d (mod N), then a+c ≡ b+d (mod N). Anyone building modular arithmetic on DistinctionNat cites this. The proof rewrites to Nat modular arithmetic via the residue–mod equivalence and applies Nat.add_mod twice.
Claim. Let $N,a,b,c,d$ be distinction orbits with $N \neq 0$. If $a$ and $b$ have the same residue modulo $N$, and $c$ and $d$ have the same residue modulo $N$, then $a+c$ and $b+d$ have the same residue modulo $N$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the primitive counting object of the recognition calculus. Its verifier map toNat sends an orbit to ordinary Nat by counting steps.
In the ResidueOrbit module one works modulo a nonzero orbit $N$. The residue of an orbit is its class under that modulus; sameResidue N hN a b is native equality of those residues. The bridge lemma sameResidue_iff_mod_eq states this is equivalent to $a.\mathrm{toNat} \bmod N.\mathrm{toNat} = b.\mathrm{toNat} \bmod N.\mathrm{toNat}$.
Addition on DistinctionNat is already known to match Nat addition under toNat (recovery theorem toNat_add from ArithmeticFromLogic / OrbitArithmetic). The present result is the corresponding compatibility of residue equality with that addition.
proof idea
Tactic proof. Rewrite the two hypotheses and the goal through sameResidue_iff_mod_eq, so everything is a statement about Nat remainders. Replace (a+c).toNat and (b+d).toNat by sums of toNats via toNat_add. Then a three-line calc chain: apply Nat.add_mod to factor the left sum modulo $N$, substitute the two residue equalities, and apply the symmetric form of Nat.add_mod on the right.
why it matters
This is one of the algebraic closure facts needed to treat residues of distinction orbits as a genuine modular arithmetic, not merely a display of Nat remainders. It is consumed by residue_orbit_certificate, which packages residue display, the mod-equivalence, reflexivity/symmetry of same-residue, and related laws into a single certificate structure for the factorization layer.
In the Recognition Science foundation stack this sits under PrimitiveRecognitionCalculus factorization: orbits and their residues are the discrete substrate from which later forcing (T5–T8, eight-tick structure, dimension) is built. Without add-compatibility, residue classes would not form a ring-like object and chart transitions / factorization certificates could not treat modular identities as native.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.