sameResidue_iff_mod_eq
plain-language theorem explainer
Native residue equality modulo a nonzero distinction orbit N is equivalent to ordinary modular equality of the verifier Nat displays of a and b. Anyone working residue arithmetic or period-based factorization in the Primitive Recognition Calculus cites this bridge. The proof is a two-way constructor: one direction pushes residue equality through toNat via the residue display lemma; the other injects equal Nat remainders back to orbit equality.
Claim. Let $N$ be a nonzero distinction orbit and let $a,b$ be distinction orbits. The residues of $a$ and $b$ modulo $N$ are equal if and only if the Nat displays satisfy $a_{\mathrm{Nat}} \bmod N_{\mathrm{Nat}} = b_{\mathrm{Nat}} \bmod N_{\mathrm{Nat}}$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the native carrier for arithmetic built from recognition steps. Its verifier display toNat reads each orbit as an ordinary Nat; that display is injective (toNat_inj), so equal Nat values come from equal orbit positions.
In the residue layer, residue N hN a is the native remainder of a modulo nonzero N, and sameResidue is equality of those native residues. The companion lemma residue_toNat states that the Nat display of the native residue is exactly ordinary modular reduction: (residue N hN a).toNat = a.toNat % N.toNat.
This module sits in the factorization track of Primitive Recognition Calculus: residues, units, and periods are developed natively on DistinctionNat, then certified against ordinary modular arithmetic so Euler-type return and period-gap factoring can be stated without leaving the orbit language.
proof idea
Term-mode constructor on the biconditional.
Forward: from sameResidue (i.e. equal native residues), apply congrArg DistinctionNat.toNat and rewrite with residue_toNat to obtain equal Nat remainders.
Backward: unfold sameResidue, apply injectivity toNat_inj of the verifier display, and again rewrite with residue_toNat so the assumed Nat congruence becomes equality of native residues.
No induction; the work is the display lemma plus injectivity of toNat.
why it matters
This is the display bridge that lets native residue equality talk to ordinary modular arithmetic. Downstream, sameResidue_add and sameResidue_mul rewrite through it to transport congruence under native sum and product. residue_orbit_certificate packages it as the same_residue_display field of the residue-orbit certificate.
Further up the factorization track, eulerPeriod_returns_one uses the iff to reduce Euler return (a unit residue raised to the Euler exponent lands on the identity residue) to a Nat coprimality computation. nontrivialFactorization_of_evenPeriodGapWitness sits on the same stack: period-gap witnesses produce native nontrivial factorizations of N once residue arithmetic is certified.
In the Recognition foundation this is plumbing, not a forcing-chain landmark (T5–T8), but it is required infrastructure for arithmetic-from-logic factorization statements that later feed mass and period structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.