residueMul_toNat_mod
plain-language theorem explainer
Residue multiplication on distinction orbits, read out by the iteration-count map, equals ordinary natural-number multiplication modulo the modulus. Anyone building modular arithmetic on the native orbit type cites this display lemma. The proof is a two-line unfold-and-rewrite through the residue and multiplication recovery maps.
Claim. For a nonzero distinction-orbit modulus $N$ and any distinction orbits $a,b$, the iteration count of the residue of the product $a\cdot b$ equals $(|a|\cdot|b|)\bmod |N|$, where $|\cdot|$ is the forward map from orbit positions to $\mathbb{N}$.
background
Distinction orbits are the native counting type of the primitive recognition calculus: each value is an iterated step from the identity, and toNat reads off that iteration count. Multiplication on orbits is defined so that it recovers ordinary Nat multiplication under this map (the recovery theorem toNat_mul).
The residue layer factors orbits by a nonzero modulus $N$. The native residue of $a$ is the remainder of $a$ by $N$; residue_toNat states that this remainder displays as ordinary modular reduction: $(\mathrm{residue},N,a).\mathrm{toNat}=a.\mathrm{toNat}\bmod N.\mathrm{toNat}$. Residue-level multiplication is then defined by taking the residue of the ordinary product: $\mathrm{residueMul},N,a,b:=\mathrm{residue},N,(a\cdot b)$.
This module sits in the factorization/residue-orbit layer of Primitive Recognition Calculus, building modular arithmetic that stays on orbit positions rather than jumping to Nat prematurely.
proof idea
Term-mode proof by definitional reduction. Unfold residueMul to expose residue N hN (a * b). Rewrite with residue_toNat, which turns the outer residue into modular reduction of (a * b).toNat. Then apply toNat_mul to replace (a * b).toNat by a.toNat * b.toNat. The goal is then definitionally the claimed congruence.
why it matters
Feeds the residue-orbit certificate (residue_orbit_certificate), which packages display lemmas and congruence laws so the residue layer can be used as a certified modular arithmetic interface on distinction orbits. Without this identity, residue multiplication would not be known to match ordinary modular multiplication under the iteration-count readout.
In the broader Recognition foundation, arithmetic is recovered from logic/orbit structure rather than assumed as a primitive. This lemma is a small but necessary bridge: it keeps multiplication inside the residue chart while guaranteeing agreement with the classical % operation. It pairs with the sibling addition display residueAdd_toNat_mod and the same-residue congruence laws that the certificate also records.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.