sameResidue_mul
plain-language theorem explainer
Multiplication preserves residue equality on DistinctionNat orbits: if a ≡ b and c ≡ d modulo nonzero N, then a·c ≡ b·d. Anyone building modular arithmetic or factorization certificates on the recognition orbit cites this. The proof rewrites to Nat modular equality and applies Nat.mul_mod twice.
Claim. Let $N,a,b,c,d$ be distinction-orbit naturals 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 \cdot c$ and $b \cdot d$ have the same residue modulo $N$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive Peano-like type with zero and succ. Its arithmetic is recovered into ordinary Nat via toNat, which counts iterations; the recovery theorem toNat_mul states that orbit multiplication matches Nat multiplication under this map.
In the ResidueOrbit factorization layer, residue of a modulo nonzero N is the canonical representative of a on the orbit of length N, and sameResidue asserts equality of those representatives. The bridge lemma sameResidue_iff_mod_eq equates that native predicate with ordinary modular equality a.toNat % N.toNat = b.toNat % N.toNat.
This module sits in PrimitiveRecognitionCalculus factorization: residues are the chart-level data for orbit arithmetic used when factoring or certifying modular structure without leaving the recognition calculus.
proof idea
Tactic proof. Rewrite the two hypotheses and the goal through sameResidue_iff_mod_eq, so the claim becomes a modular equality of Nat products. Replace both products by toNat_mul (orbit mul agrees with Nat mul). Then a three-step calc: apply Nat.mul_mod to factor residues out of the left product; substitute the rewritten hypotheses; apply the symmetric Nat.mul_mod identity to reassemble the right product.
why it matters
Residue equality must be a congruence for multiplication if residues are to support factorization and modular certificates on distinction orbits. This lemma supplies that congruence law.
It is consumed by residue_orbit_certificate, which packages residue display, same-residue iff mod, and the equivalence/congruence laws into a single ResidueOrbitCertificate structure. Without mul-congruence, that certificate cannot assert that residue arithmetic is well-defined under products.
In the broader foundation, this is plumbing between ArithmeticFromLogic (LogicNat/DistinctionNat recovery) and factorization charts: modular structure on the recognition orbit, not a physics forcing step (T5–T8), but required infrastructure for any later number-theoretic claims stated in native RS types.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.