sameResidue_symm
plain-language theorem explainer
Residue equality modulo a nonzero DistinctionNat is symmetric: if a and b share a residue class, so do b and a. Anyone assembling a ResidueOrbitCertificate (or any modular arithmetic on the native orbit type) cites this. The proof unfolds the definition to propositional equality and applies Eq.symm.
Claim. Let $N,a,b$ be values of the base-neutral finite orbit type, with $N \neq 0$. If the residue of $a$ modulo $N$ equals the residue of $b$ modulo $N$, then the residue of $b$ modulo $N$ equals the residue of $a$ modulo $N$.
background
DistinctionNat is the inductive, base-neutral finite orbit of repeated distinction (K2.12): zero and successor, with decidable equality. Residues live on this type rather than on ordinary naturals, so modular bookkeeping stays inside the Recognition calculus.
The predicate sameResidue N hN a b is defined as equality of the native residues: residue N hN a = residue N hN b. It is the native stand-in for congruence modulo N when N is nonzero. The present lemma is the symmetry half of the equivalence relation that residue classes induce.
The module sits in the factorization layer of PrimitiveRecognitionCalculus, importing chart-transition infrastructure and Mathlib, and packaging residue arithmetic for later orbit certificates.
proof idea
One-step tactic proof. Unfold sameResidue in the hypothesis and the goal, reducing both sides to equality of residue values. Then apply the symmetry of propositional equality (h.symm). No auxiliary lemmas beyond the definition are required.
why it matters
Feeds residue_orbit_certificate, which packages residue display, the mod-equality characterization, and the equivalence laws (refl, symm, trans) into a single certificate structure. Downstream that certificate is the interface other factorization and orbit results expect when they treat residue classes as an equivalence relation on DistinctionNat.
In the broader Recognition stack this is scaffolding hygiene rather than a forcing-chain step: it keeps native modular arithmetic on the distinction orbit coherent so later factorization and chart-transition arguments can quote a closed equivalence without dropping to Mathlib naturals. No T0–T8 landmark is discharged here; the lemma is local algebraic glue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.