Division and Modulo from Recursive Normalization
Thiago Henrique Ramos da Mata · Zenodo (CERN European Organization for Nuclear Research) · 2026
We define integer division and modulo by recursively normalizing quotient–remainder states and verify the construction in Scala Stainless. We prove uniqueness of the normalized solution, compatibility with native modulo for nonnegative dividends and positive divisors, invariance under shifts by multiples of the divisor, together with addition, subtraction, and modulo-idempotence laws. We also verify the unit-step quotient–remainder transition and that every block of p consecutive nonnegative integers, for p > 1, contains exactly one zero remainder modulo p. Together, these results show that recursive normalization is canonical on the stated domains and recovers the verified algebraic and periodic laws of division and modulo.