residue_toNat
plain-language theorem explainer
The native residue of an orbit position a modulo a nonzero modulus N, read out as a Lean natural, is ordinary modular reduction of the two verifier naturals. Anyone building residue arithmetic or congruence certificates on DistinctionNat cites this bridge. The proof is a one-line unfold of residue followed by the Euclidean remainder readout.
Claim. For every nonzero orbit modulus $N$ and every orbit position $a$, the verifier natural of the native residue of $a$ modulo $N$ equals $a$'s verifier natural reduced modulo $N$'s verifier natural: $\mathrm{toNat}(\mathrm{residue}(N,a)) = \mathrm{toNat}(a)\bmod \mathrm{toNat}(N)$.
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 rather than from bare Nat. Its verifier map toNat sends zero to 0 and successor to Nat.succ, so every orbit position has a unique Lean natural readout.
The native residue of a modulo nonzero N is defined as the Euclidean remainder of a by N. Upstream, remainder_toNat already records that this remainder's toNat equals ordinary Nat modular reduction. The present lemma simply specializes that fact to the residue abbreviation used throughout the factorization layer.
Local setting is the ResidueOrbit module inside PrimitiveRecognitionCalculus.Factorization: native residues, same-residue congruence, and residue addition/multiplication, all kept on DistinctionNat and only displayed to Nat when a certificate or bridge is needed.
proof idea
One-line wrapper. Unfold the definition residue (which is exactly remainder a N hN), then apply the upstream theorem remainder_toNat a N hN, whose second component of divMod_toNat already gives (remainder n d hd).toNat = n.toNat % d.toNat.
why it matters
This is the display bridge that lets every later residue fact talk to ordinary modular arithmetic. Downstream, residueAdd_toNat_mod and residueMul_toNat_mod rewrite residue addition and multiplication to (a.toNat + b.toNat) % N.toNat and the product analogue by calling residue_toNat after unfolding. sameResidue_iff_mod_eq uses the same readout to equate native residue equality with equality of Nat residues. The package is sealed in residue_orbit_certificate, whose residue_display field is exactly this theorem.
In the Recognition foundation stack this sits under arithmetic-from-logic and the Euclidean orbit layer: it does not touch the forcing chain (T5–T8) or the J-cost directly, but it is the modular-arithmetic primitive needed before factorization and chart-transition arguments can certify congruence on orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.