sameResidue_trans
plain-language theorem explainer
Residues modulo a nonzero distinction-orbit N are transitive: if a and b share a residue and b and c share one, then a and c do. Anyone building congruence or orbit-factorization arguments on DistinctionNat cites this. The proof unfolds the residue-equality definition and applies ordinary equality transitivity.
Claim. Let $N,a,b,c$ be elements of the base-neutral finite orbit of repeated distinction, with $N \neq 0$. If the residue of $a$ modulo $N$ equals the residue of $b$ modulo $N$, and the residue of $b$ equals that of $c$, then the residue of $a$ equals the residue of $c$.
background
DistinctionNat is the inductive type of finite orbits of repeated distinction (K2.12): zero and successor, base-neutral and decidably equal. It is the native carrier for discrete recognition steps before any embedding into ordinary naturals.
In the ResidueOrbit factorization layer, residue extracts the remainder of a DistinctionNat against a nonzero modulus $N$. The relation sameResidue asserts native equality of those residues: residue $N,a$ = residue $N,b$. It is the congruence predicate used throughout chart transitions and orbit certificates in PrimitiveRecognitionCalculus.
This module sits under Foundation factorization: residues organize the discrete orbit into residue classes so later certificates can treat modular arithmetic without leaving the recognition-native type.
proof idea
Term-mode proof in two steps. Unfold sameResidue in the two hypotheses and the goal, exposing three equalities of residue values. Then apply Eq.trans (written hab.trans hbc) to chain residue $a$ = residue $b$ with residue $b$ = residue $c$ into residue $a$ = residue $c$. No arithmetic lemmas are needed; only propositional equality on the residue type.
why it matters
Feeds residue_orbit_certificate, which packages residue display, the mod-equality characterization, and the equivalence-relation laws (refl, symm, and this transitivity) into a single ResidueOrbitCertificate structure. Without transitivity the certificate cannot claim that sameResidue is an equivalence, and downstream factorization or chart-transition arguments lose a clean congruence.
In the broader Recognition stack this is scaffolding for discrete modular structure on distinction orbits, not a forcing-chain landmark (T5–T8). It keeps residue arithmetic internal to DistinctionNat so later mass-ladder or eight-tick constructions can quote a certified equivalence rather than ad-hoc equality chasing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.