Clock arithmetic: remainders and modular arithmetic

Four questions that look unrelated:

1. The overnight train from Mumbai leaves at 21:00 and the journey takes 30 hours. At what time does it arrive?
2. 1 January 2026 was a Thursday. What day of the week was it 100 days later?
3. In Dar es Salaam, a friend says she will meet you at saa moja asubuhi — “hour one in the morning”. When should you be there?
4. What is the last digit of $7^{2026}$, a number with more than 1700 digits?

Every one of them is answered the same way: throw away whole cycles and keep the remainder. A day has 24 hours, a week has 7 days, a clock face has 12 hours, and last digits repeat every 10. This lesson turns that trick into an arithmetic of its own, proves why it works, and finds something surprising hiding in its multiplication tables.

Take the number line $0, 1, 2, 3, \dots$ and wind it around a circle with 12 equally spaced marks. The numbers $0, 1, \dots, 11$ go once around; then $12$ lands on top of $0$, $13$ on top of $1$, and so on.

Two numbers land on the same mark exactly when they differ by a whole number of trips around — a multiple of 12. So to find where a number lands, divide by 12 and keep the remainder. Adding means walking forwards around the circle. Nothing else about the number matters.

You know division with remainder: for whole numbers $a$ and $n \ge 1$ there is exactly one way to write

For example $38 \bmod 12 = 2$ because $38 = 3 \cdot 12 + 2$, and $100 \bmod 7 = 2$ because $100 = 14 \cdot 7 + 2$.

When $a$ and $b$ leave the same remainder on division by $n$, mathematicians write $a \equiv b \pmod n$ and say “$a$ is congruent to $b$ modulo $n$”. So $38 \equiv 2 \pmod{12}$ and $9 + 29 \equiv 2 \pmod{12}$. It is the notation of the clock: “lands on the same mark”.

Here are two complete multiplication tables. Look along each row.

Modulo 5, every non-zero row is a shuffle of $0, 1, 2, 3, 4$: each remainder appears exactly once. Modulo 6 the rows of $2$, $3$ and $4$ repeat themselves, and strange things happen: $2 \cdot 3 \equiv 0$ although neither factor is $0$.

Modulo 5: $2 \cdot 3 = 6 \equiv 1$, so $2$ and $3$ are partners, and $4 \cdot 4 = 16 \equiv 1$. Modulo 6, only $1$ and $5$ have partners — the rows of $2, 3, 4$ never contain a $1$.

The shortcut “throw away multiples of $n$ whenever you like” rests on two theorems.

Together these say: the remainder of a sum or product depends only on the remainders of its parts. That is exactly why the clock arithmetic of the last section is consistent — and why you may reduce at any moment in a long calculation.

Look again at the tables. Modulo 6, only $1$ and $5$ have partners; modulo 5, every non-zero remainder does. Modulo 12 (try it in the explorer below) only $1, 5, 7, 11$ do. What decides?

So $2, 3, 4, 6, 8, 9, 10$ have no partners modulo $12$, and $2, 4, 5, 6, 8$ have none modulo $10$. The converse is also true — if $a$ and $n$ have no common factor greater than 1, then $a$ has a partner modulo $n$ — but its proof needs Euclid's algorithm, which you will meet in divisibility and the gcd. Here we prove the most important case.

The same reasoning explains the zero products. If $n = r \cdot s$ with $1 \lt r, s \lt n$, then $r \cdot s \equiv 0 \pmod n$ although $r, s \not\equiv 0$. Modulo a prime that cannot happen, by Euclid's lemma. Prime clocks behave like ordinary fractions: you can divide by anything except $0$.

In Lean, a % n is the remainder of a on division by n. First, division with remainder and the range of a remainder (both quoted from Lean's library), and the train and weekday examples, which Lean checks by computing:

/-- **Division with remainder.** Every `a` is `n` times its quotient plus its remainder:
`n · (a / n) + a % n = a`. This applies core Lean's `Nat.div_add_mod`. -/
theorem div_add_mod (a n : Nat) : n * (a / n) + a % n = a := Nat.div_add_mod a n

/-- A remainder on division by `n > 0` is always one of `0, 1, …, n - 1`: `a % n < n`.
This applies core Lean's `Nat.mod_lt`. -/
theorem mod_lt (a : Nat) {n : Nat} (hn : 0 < n) : a % n < n := Nat.mod_lt a hn

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

/-- Number the days Monday = 0, Tuesday = 1, …, Sunday = 6. Then 100 days after a Monday is
day `100 mod 7 = 2`, a Wednesday. -/
theorem week_example : (0 + 100) % 7 = 2 := by decide

Theorems 1 and 2 are proved exactly as in the human proofs: split a and b into quotient and remainder, regroup, and use the fact that adding a multiple of n does not change a remainder (Nat.mul_add_mod). The calc blocks are the displayed equations of the proofs.

/-- **The remainder of a sum depends only on the remainders.**
`(a + b) mod n = ((a mod n) + (b mod n)) mod n`.
The lesson's proof: write `a = n·q₁ + r₁` and `b = n·q₂ + r₂`. Then
`a + b = n·(q₁ + q₂) + (r₁ + r₂)`, and adding a multiple of `n` never changes a remainder
(`Nat.mul_add_mod`). -/
theorem add_mod_of_division (a b n : Nat) : (a + b) % n = (a % n + b % n) % n := by
  -- The two divisions with remainder.
  have ha := Nat.div_add_mod a n
  have hb := Nat.div_add_mod b n
  -- Regroup: `a + b` is a multiple of `n` plus `r₁ + r₂`.
  have hsum : a + b = n * (a / n + b / n) + (a % n + b % n) := by
    calc a + b = (n * (a / n) + a % n) + (n * (b / n) + b % n) := by rw [ha, hb]
      _ = n * (a / n + b / n) + (a % n + b % n) := by rw [Nat.mul_add]; omega
  rw [hsum, Nat.mul_add_mod]

/-- **The remainder of a product depends only on the remainders.**
`(a · b) mod n = ((a mod n) · (b mod n)) mod n`.
Proof: with `a = n·q₁ + r₁` and `b = n·q₂ + r₂`, expanding gives
`a · b = n·(q₁·b + r₁·q₂) + r₁·r₂`, a multiple of `n` plus `r₁ · r₂`. -/
theorem mul_mod_of_division (a b n : Nat) : (a * b) % n = (a % n * (b % n)) % n := by
  have ha := Nat.div_add_mod a n
  have hb := Nat.div_add_mod b n
  have hprod : a * b = n * (a / n * b + a % n * (b / n)) + a % n * (b % n) := by
    calc a * b = (n * (a / n) + a % n) * b := by rw [ha]
      _ = n * (a / n) * b + a % n * b := Nat.add_mul _ _ _
      _ = n * (a / n) * b + a % n * (n * (b / n) + b % n) := by rw [hb]
      _ = n * (a / n * b + a % n * (b / n)) + a % n * (b % n) := by
        rw [Nat.mul_add (a % n), Nat.mul_add n, Nat.mul_assoc, ← Nat.add_assoc,
          Nat.mul_left_comm (a % n) n]
  rw [hprod, Nat.mul_add_mod]

/-- The same fact for sums, quoted from core Lean's library (`Nat.add_mod`). Compare
`add_mod_of_division`, which proves it here from division with remainder. -/
theorem add_mod_library (a b n : Nat) : (a + b) % n = (a % n + b % n) % n := Nat.add_mod a b n

Zero products, Theorem 4, and a use of it:

/-- On a 12-hour clock a product can be `0` although neither factor is:
`3 · 4 = 12 ≡ 0 (mod 12)` while `3 mod 12 = 3` and `4 mod 12 = 4`. -/
theorem zero_product_mod_twelve : (3 * 4) % 12 = 0 ∧ 3 % 12 ≠ 0 ∧ 4 % 12 ≠ 0 := by decide

/-- **A common factor blocks a partner.** If some `d > 1` divides both `a` and `n`, then no `b`
has `a · b mod n = 1`.
Proof: `d` divides `a · b`, and `d` divides `n`, so `d` divides the remainder `a · b mod n`
(the remainder is `a · b` minus a multiple of `n`). If that remainder were `1`, then `d` would
divide `1`, so `d = 1`, contradicting `d > 1`. -/
theorem no_partner_of_common_factor {a n d : Nat} (hd : 1 < d) (hda : d ∣ a) (hdn : d ∣ n)
    (b : Nat) : (a * b) % n ≠ 1 := by
  intro h
  -- `d` divides `a · b` …
  have hab : d ∣ a * b := Nat.dvd_mul_right_of_dvd hda b
  -- … so it divides the remainder of `a · b` on division by `n`, which is `1`.
  have h1 : d ∣ (a * b) % n := (Nat.dvd_mod_iff hdn).mpr hab
  rw [h] at h1
  have : d = 1 := Nat.eq_one_of_dvd_one h1
  omega

/-- `4` has no partner modulo `10`: `4` and `10` share the factor `2`. This is
`no_partner_of_common_factor` with `d = 2`. -/
theorem four_no_partner_mod_ten (b : Nat) : (4 * b) % 10 ≠ 1 :=
  no_partner_of_common_factor (d := 2) (by decide) (by decide) (by decide) b

Lean has clock arithmetic built in: Fin 12 is the set of numbers $0, \dots, 11$, and its * multiplies and then takes the remainder on division by 12. For one particular clock, decide can simply try every case — 144 products for the 12-hour clock:

/-- On a 12-hour clock exactly `1, 5, 7, 11` have a multiplicative partner. Lean's `Fin 12`
is clock arithmetic: its numbers are `0, …, 11` and `*` multiplies and takes the remainder.
`decide` checks all 144 products. -/
theorem partners_mod_twelve :
    ∀ a : Fin 12, (∃ b : Fin 12, a * b = 1) ↔ (a = 1 ∨ a = 5 ∨ a = 7 ∨ a = 11) := by
  decide

/-- Modulo the prime `7`, every non-zero remainder has a partner
(`1·1`, `2·4`, `3·5`, `6·6` all leave remainder `1`). `decide` checks every case. -/
theorem partners_mod_seven : ∀ a : Fin 7, a ≠ 0 → ∃ b : Fin 7, a * b = 1 := by decide

/-- Modulo `7`, multiplying by a non-zero `a` never sends two different remainders to the
same place: each row of the multiplication table is a shuffle of `0, …, 6`. (This is the
property check digits rely on.) -/
theorem row_is_shuffle_mod_seven :
    ∀ a x y : Fin 7, a ≠ 0 → a * x = a * y → x = y := by decide

These three are checked case by case for one modulus each; Theorem 5 for every prime is not formalised here (it needs Euclid's lemma, which is formalised in the lesson on divisibility). Finally, the repeating patterns, proved for all $k$ by induction — the formal version of “and so on for ever”:

/-- The powers of `2` modulo `7` repeat `1, 2, 4, 1, 2, 4, …`. In particular
`2^(3k) mod 7 = 1` for every `k`.
Proof by induction: `2^(3(k+1)) = 2^(3k) · 8`, and `8 mod 7 = 1`, so by
`mul_mod_of_division` the remainder is `1 · 1 = 1`. -/
theorem pow_three_mod_seven (k : Nat) : 2 ^ (3 * k) % 7 = 1 := by
  induction k with
  | zero => decide
  | succ k ih =>
    calc 2 ^ (3 * (k + 1)) % 7 = (2 ^ (3 * k) * 8) % 7 := by
          rw [Nat.mul_succ, Nat.pow_add]
      _ = (2 ^ (3 * k) % 7 * (8 % 7)) % 7 := mul_mod_of_division _ _ _
      _ = 1 := by rw [ih]

/-- The last digit of `7^(4k + 2)` is always `9`: the last digits of `7, 49, 343, 2401, …`
repeat `7, 9, 3, 1`. Proof: `7^4 = 2401` leaves remainder `1` on division by `10`, so
`7^(4k) mod 10 = 1` by induction, and `7^2 = 49`. For example, `7^2026` ends in `9`. -/
theorem last_digit_seven_pow (k : Nat) : 7 ^ (4 * k + 2) % 10 = 9 := by
  have h4 : ∀ j : Nat, 7 ^ (4 * j) % 10 = 1 := by
    intro j
    induction j with
    | zero => decide
    | succ j ih =>
      calc 7 ^ (4 * (j + 1)) % 10 = (7 ^ (4 * j) * 2401) % 10 := by
            rw [Nat.mul_succ, Nat.pow_add]
        _ = (7 ^ (4 * j) % 10 * (2401 % 10)) % 10 := mul_mod_of_division _ _ _
        _ = 1 := by rw [ih]
  calc 7 ^ (4 * k + 2) % 10 = (7 ^ (4 * k) * 49) % 10 := by rw [Nat.pow_add]
    _ = (7 ^ (4 * k) % 10 * (49 % 10)) % 10 := mul_mod_of_division _ _ _
    _ = 9 := by rw [h4 k]

/-- `10^k mod 9 = 1` for every `k`, because `10 = 9 + 1` leaves remainder `1`. This is why a
number and the sum of its digits leave the same remainder on division by `9`
("casting out nines"). -/
theorem ten_pow_mod_nine (k : Nat) : 10 ^ k % 9 = 1 := by
  induction k with
  | zero => decide
  | succ k ih =>
    calc 10 ^ (k + 1) % 9 = (10 ^ k * 10) % 9 := by rw [Nat.pow_succ]
      _ = (10 ^ k % 9 * (10 % 9)) % 9 := mul_mod_of_division _ _ _
      _ = 1 := by rw [ih]

In Mathlib, the integers modulo $n$ form the ring ZMod n, congruence is Nat.ModEq, and the partner of a number coprime to $n$ is built by ZMod.unitOfCoprime.

"""Clock arithmetic by machine: reduce-first rules, partners and zero products.

For every modulus n from 2 to 30 the experiment builds the multiplication
table modulo n and finds which remainders a have a partner b with
a * b mod n = 1. It compares that list with the remainders that share no
factor greater than 1 with n, and it searches for "zero products" a * b = 0
with neither factor 0. It also checks the reduce-first rules for sums and
products on a finite range. Everything is exact integer arithmetic over finite
ranges: exhaustive evidence for those n, not a proof for every n.
"""

import math

def partners(n):
    """Remainders a in 0..n-1 that have some b with a * b mod n == 1."""
    if n < 1:
        raise ValueError("n must be positive")
    return [a for a in range(n) if any(a * b % n == 1 for b in range(n))]

def partner_of(a, n):
    """The b in 0..n-1 with a * b mod n == 1, or None if there is none."""
    for b in range(n):
        if a * b % n == 1:
            return b
    return None

def coprime_remainders(n):
    """Remainders a in 0..n-1 with gcd(a, n) == 1 (no common factor > 1)."""
    return [a for a in range(n) if math.gcd(a, n) == 1 and n > 1]

def zero_products(n):
    """Pairs (a, b) of non-zero remainders with a * b mod n == 0."""
    return [(a, b) for a in range(1, n) for b in range(1, n) if a * b % n == 0]

def reduce_first_failures(n_max, a_max):
    """Count cases and failures of the sum and product rules (n = 1..n_max)."""
    cases = failures = 0
    for n in range(1, n_max + 1):
        for a in range(a_max):
            for b in range(a_max):
                cases += 1
                if (a + b) % n != (a % n + b % n) % n:
                    failures += 1
                if (a * b) % n != (a % n) * (b % n) % n:
                    failures += 1
    return cases, failures

def is_prime(n):
    """Trial division (n >= 2)."""
    return n >= 2 and all(n % d for d in range(2, math.isqrt(n) + 1))

def main():
    cases, bad = reduce_first_failures(30, 120)
    print(f"Reduce-first rules, a, b < 120, n <= 30: {cases} cases, {bad} failures")
    print()
    print("Who has a partner?")
    for n in (10, 11, 12):
        pairs = ", ".join(f"{a}*{partner_of(a, n)}" for a in partners(n))
        print(f"  mod {n:<2}: {pairs}")
    same = all(partners(n) == coprime_remainders(n) for n in range(2, 31))
    print(f"  partners = remainders coprime to n, for n = 2..30: {same}")
    full = [n for n in range(2, 31) if len(partners(n)) == n - 1]
    print("  n for which every non-zero remainder has a partner:")
    print(f"    {full}")
    primes = [n for n in range(2, 31) if is_prime(n)]
    print(f"  these n are exactly the primes up to 30: {full == primes}")
    print()
    print("Zero products (a * b = 0 with a, b non-zero):")
    for n in (7, 10, 12):
        zs = zero_products(n)
        shown = ", ".join(f"{a}*{b}" for a, b in zs if a <= b)
        print(f"  mod {n:<2}: {shown or 'none'}")
    no_zero = [n for n in range(2, 31) if not zero_products(n)]
    print(f"  n <= 30 with no zero products: {no_zero}")
    print()
    print("Epistemic status: exhaustive, exact evidence for the moduli and ranges")
    print("shown, nothing more. The reduce-first rules and 'a common factor blocks")
    print("a partner' are proved in the lesson for every n; 'coprime implies a")
    print("partner' is proved later with Euclid's algorithm.")

if __name__ == "__main__":
    main()

The output agrees with Theorems 4 and 5 and with the converse we have not proved yet: the remainders with partners are exactly those sharing no factor with $n$, and the moduli with no zero products are exactly the primes. For $n \le 30$ that is exhaustive evidence; for larger $n$ it is the theorems that do the work.

"""Repeating patterns: last digits of powers, weekdays and calendar cycles.

Remainders of powers must eventually repeat, because there are only n
possible remainders. The experiment finds the repeating cycle of base^k mod n
for some bases (for n = 10 these are last digits), uses a cycle to get the
last digit of a huge power without computing the power, and checks the answer
against Python's exact pow. It then steps two calendar cycles forward day by
day until they line up again (the Chinese 10-stem and 12-branch cycle, and the
Maya 260-day and 365-day counts) and compares with the least common multiple.
All arithmetic is exact; each check covers only the cases printed.
"""

import math

def power_cycle(base, n):
    """Return (start, cycle) for the remainders base^k mod n, k = 0, 1, 2, ...

    ``start`` is the first k where the repeating part begins and ``cycle``
    lists one full period of remainders.
    """
    if n < 1:
        raise ValueError("n must be positive")
    seen = {}
    values = []
    r = 1 % n
    k = 0
    while r not in seen:
        seen[r] = k
        values.append(r)
        r = r * base % n
        k += 1
    start = seen[r]
    return start, values[start:]

def remainder_from_cycle(base, exponent, n):
    """base^exponent mod n read off the cycle (no huge power is computed)."""
    start, cycle = power_cycle(base, n)
    if exponent < start:
        return pow(base, exponent, n)
    return cycle[(exponent - start) % len(cycle)]

def realign(p, q):
    """Step a p-cycle and a q-cycle together; first day > 0 both are at 0."""
    day, a, b = 0, 0, 0
    while True:
        day, a, b = day + 1, (a + 1) % p, (b + 1) % q
        if a == 0 and b == 0:
            return day

WEEKDAYS = ["Monday", "Tuesday", "Wednesday", "Thursday", "Friday",
            "Saturday", "Sunday"]

def weekday_after(start, days):
    """Name of the weekday ``days`` days after the weekday named ``start``."""
    return WEEKDAYS[(WEEKDAYS.index(start) + days) % 7]

def main():
    print("Cycles of remainders of powers (k = 0, 1, 2, ...):")
    for base, n in [(2, 10), (3, 10), (7, 10), (2, 7), (4, 12)]:
        start, cycle = power_cycle(base, n)
        print(f"  {base}^k mod {n:<2}: starts repeating at k = {start}, "
              f"cycle {cycle}")
    predicted = remainder_from_cycle(7, 2026, 10)
    exact = pow(7, 2026) % 10
    digits = len(str(pow(7, 2026)))
    print(f"Last digit of 7^2026 from the cycle: {predicted}; exact: {exact}")
    print(f"  (7^2026 has {digits} digits; the cycle needed only 4 numbers)")
    print()
    print("Weekdays: 1 January 2026 was a Thursday.")
    for days in (7, 100, 365):
        print(f"  {days:>3} days later: {weekday_after('Thursday', days)}")
    print()
    print("Two cycles running side by side, stepped one at a time:")
    for p, q, name in [(10, 12, "Chinese stems and branches (years)"),
                       (260, 365, "Maya tzolk'in and haab' (days)")]:
        print(f"  {name}:")
        print(f"    {p} and {q} realign after {realign(p, q)} steps;"
              f" lcm({p}, {q}) = {math.lcm(p, q)}")
    print()
    print("Epistemic status: exact computations, each checked only for the")
    print("cases printed. That powers must repeat is a proof (there are only n")
    print("remainders); that a cycle of length 4 continues forever for 7^k mod 10")
    print("is proved in the lesson from 7^4 = 2401 and the product rule.")

if __name__ == "__main__":
    main()

The Chinese calendar names years by pairing one of 10 heavenly stems with one of 12 earthly branches, both advancing each year; the pairs repeat after $60$ years, not $120$, because $60$ is the first number that is a multiple of both $10$ and $12$. The Maya ran a 260-day count and a 365-day count side by side; the pair of dates repeats only after $18\,980$ days, about 52 years — the Calendar Round.

In the Add tab, choose the number of hours $k$, a starting time and an amount to add; the hand jumps to the remainder. Try $k = 24$ and add $30$ (the overnight train), then $k = 7$ (a week) and add $16$. In the Multiply tab, look for a $1$ in each row. Which rows have one for $k = 7$, $k = 11$ and $k = 13$? For $k = 10$ and $k = 12$? Press the button to reveal the pattern, then check it against Theorems 4 and 5.

A calendar is a number grid with 7 columns. Every number in one column leaves the same remainder on division by 7. Mark the multiples of 7 and the multiples of 3: which columns do the multiples of 3 visit, and when does the pattern repeat?

Dividing by $n$ sorts every whole number — and every integer — into exactly $n$ families: the set of numbers with remainder $0$, the set with remainder $1$, and so on up to remainder $n - 1$. Modulo 2 the families are the even and the odd numbers. These sets do not overlap and together they contain every integer: they form a partition. Theorems 1 and 2 say something remarkable about them: if you add a member of one family to a member of another, the family of the answer does not depend on which members you picked. That is why we can add and multiply the families themselves. The Remainder families trail explores this; at university it becomes the idea of an equivalence relation and a quotient (see equivalence relations).

• China. The Sunzi Suanjing (Master Sun's Mathematical Manual, between the 3rd and 5th centuries CE) asks for a number of things that leaves remainder 2 when counted by threes, 3 when counted by fives and 2 when counted by sevens (answer: 23). In 1247 Qin Jiushao's Mathematical Treatise in Nine Sections gave a general method for such problems, today called the Chinese remainder theorem. Calendar-makers needed exactly this kind of calculation to find when several astronomical cycles line up.
• India. Āryabhaṭa (499 CE) described the kuṭṭaka (“pulveriser”), a method for solving equations such as $a x + c = b y$ in whole numbers — in modern terms, finding partners modulo $b$. Brahmagupta (628 CE) and later Indian astronomers refined it.
• Mesoamerica. The Maya combined a 260-day ritual count (13 numbers × 20 day-names) with a 365-day year; the same combination of dates recurs after 18,980 days, about 52 years.
• East Asia. The 60-fold cycle of heavenly stems and earthly branches was used to count days in Shang-dynasty China more than 3000 years ago, and later to name years.
• Europe. Carl Friedrich Gauss introduced the notation $a \equiv b \pmod n$ and the word modulus in his Disquisitiones Arithmeticae (1801), turning a collection of tricks into a theory.
• East Africa. Swahili timekeeping, counting hours from sunrise, is a living example of shifting a clock by a constant modulo 12.

• Joseph H. Silverman, A Friendly Introduction to Number Theory (1997; 4th edition 2012), chapters on congruences — very readable for a strong secondary-school student.
• Øystein Ore, Number Theory and Its History (1948), for the history from Sunzi to Gauss.
• George Gheverghese Joseph, The Crest of the Peacock: Non-European Roots of Mathematics (1991; 3rd edition 2011), on Chinese remainder problems, the Indian kuṭṭaka and Maya calendars.
• Carl Friedrich Gauss, Disquisitiones Arithmeticae (1801; English translation by Arthur A. Clarke, 1966), where congruences began as a theory.