Clock arithmetic

On a clock with $k$ hours, counting wraps around: after $k - 1$ comes $0$ again. Two numbers land on the same position exactly when they have the same remainder after division by $k$. Mathematicians write

("$a$ is congruent to $b$ modulo $k$") when $a$ and $b$ leave the same remainder. So $9 + 5 = 14 \equiv 2 \pmod{12}$, and $9 + 29 = 38 \equiv 2 \pmod{12}$ as well.

/-- On a 12-hour clock, 5 hours after 9 o'clock is 2 o'clock: `(9 + 5) mod 12 = 2`. -/
theorem clock_wraps : (9 + 5) % 12 = 2 := by decide

Clock arithmetic has its own multiplication too, and something remarkable happens. On a 7-hour clock, $3 \cdot 5 = 15 \equiv 1$, so $5$ acts like "one third"! On a 4-hour clock, though, $2$ has no partner at all: $2 \cdot x$ is always $0$ or $2$.

/-- Modulo 7, the number 3 has an inverse, namely 5: `3 · 5 = 15 = 2 · 7 + 1`. -/
theorem three_inv_mod_seven : (3 * 5) % 7 = 1 := by decide

/-- Modulo 4, the number 2 has **no** inverse: `2 · x` is always even, so it is never `1`
more than a multiple of 4. `decide` checks all four possibilities `x = 0, 1, 2, 3`. -/
theorem two_no_inv_mod_four : ∀ x : Fin 4, (2 * x.val) % 4 ≠ 1 := by decide

The pattern you can see in the experiment is a theorem: $a$ has a multiplicative partner modulo $k$ exactly when $a$ and $k$ have no common factor except $1$. The table is evidence for small $k$; the proof, which uses Bézout's identity, comes in number theory. When $k$ is prime, every non-zero number has a partner — so arithmetic on a prime clock behaves like arithmetic with fractions. These number systems are called $\Z/k\Z$, and for prime $k$ they are examples of finite fields.

/-- Modulo 5 (a prime), every non-zero number has an inverse:
`1·1 = 1`, `2·3 = 6`, `3·2 = 6`, `4·4 = 16`, and each of these leaves remainder 1.
`decide` checks every `a` and searches for each `b`. -/
theorem inverses_mod_five : ∀ a : Fin 5, a.val ≠ 0 → ∃ b : Fin 5, (a.val * b.val) % 5 = 1 := by
  decide

Modular arithmetic is not only a curiosity. It underlies calendars and check digits on identity numbers, and it is the foundation of much of modern cryptography.