residueMul
plain-language theorem explainer
Defines residue-class multiplication of two orbit positions modulo a nonzero orbit modulus, returning the product as a native residue on the orbit. Anyone building modular arithmetic on DistinctionNat orbits cites this. The body is a one-line wrapper: take the ordinary product, then reduce by the native residue map.
Claim. Fix a nonzero orbit modulus $N$ and orbit positions $a,b$. The residue-level product of $a$ and $b$ modulo $N$ is the native residue of the ordinary product $a\cdot b$ modulo $N$, represented again as an orbit position.
background
The ambient type is DistinctionNat: the base-neutral finite orbit of repeated distinction (K2.12), an inductive copy of the naturals with zero and successor. Arithmetic on these orbits is the substrate for the primitive recognition calculus factorization layer.
The native residue map sends an orbit position $a$ to its remainder modulo a nonzero modulus $N$. That remainder is again a DistinctionNat, so residue arithmetic stays inside the orbit language rather than jumping to ordinary Nat.
This module sits in the Factorization.ResidueOrbit development, which packages residue display, same-residue equivalence, and additive/multiplicative structure on residues as a certificate layer above chart transitions.
proof idea
One-line definitional wrapper. Apply the native residue map to the ordinary product $a * b$ under the given nonzero modulus $N$. No further lemmas are invoked at the definition site; correctness relative to ordinary modular multiplication is discharged later by unfolding and the residue-to-Nat bridge.
why it matters
Gives the multiplicative half of residue arithmetic on orbits, parallel to the additive companion. Downstream, residueMul_toNat_mod proves that the toNat image is ordinary modular multiplication: $(\mathrm{residueMul},N,a,b).\mathrm{toNat} = (a.\mathrm{toNat}\cdot b.\mathrm{toNat}) \bmod N.\mathrm{toNat}$. The ResidueOrbitCertificate structure records the residue-display and same-residue laws that this operation supports. In the Recognition foundation stack this is scaffolding for factorization and chart-transition bookkeeping on finite distinction orbits, not yet a physics-facing constant or forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.