sameResidue
plain-language theorem explainer
Two distinction-orbit naturals share the same residue modulo a nonzero modulus N exactly when their native remainders agree. Anyone working the factorization or period layer cites this as the native congruence relation. The body is a one-line definitional equality of the residue map.
Claim. Fix a nonzero modulus $N$ in the distinction-orbit naturals. Elements $a$ and $b$ are residue-equal modulo $N$ when $\mathrm{residue}_N(a)=\mathrm{residue}_N(b)$, i.e. their native remainders coincide.
background
The ambient carrier is the base-neutral finite orbit of repeated distinction (DistinctionNat): an inductive copy of the naturals with constructors zero and succ, used so that modular arithmetic stays inside the recognition calculus rather than jumping to Nat.
The residue map sends $a$ to its native remainder modulo a nonzero orbit modulus $N$. Equality of those remainders is the native congruence relation on the residue layer. The module sits under Primitive Recognition Calculus factorization, importing chart-transition infrastructure and building the residue-orbit surface used by period existence and multiplicative characters.
proof idea
Definitional, not a proof. The predicate is literally equality of the two applications of the residue map: $\mathrm{residue}_N(a)=\mathrm{residue}_N(b)$. No tactics or lemmas fire at the definition site; downstream lemmas (reflexivity, symmetry, transitivity, add/mul compatibility, and the bridge to ordinary modular equality) unpack this equality.
why it matters
This is the congruence relation the whole residue-orbit and period stack is written in. Period witnesses require that some nonzero exponent returns a unit residue to the identity under this relation. Euler's theorem in the $\delta$ residue layer is stated as residue-equality of $a^{\varphi(N)}$ with $1$. Even-period gap witnesses (the Shor-style configuration) assert a full period returns to one while the half-power avoids $\pm 1$. Finite multiplicative characters are required to respect this relation on orbit representatives. The residue-orbit certificate packages a display lemma that same-residue is ordinary modular equality after toNat. Without a native Prop for residue equality, those structures would leak into raw Nat congruence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.