IMO 1985 Q2

Fix a natural number $n ≥ 3$ and define $N=\{1, 2, 3, \dots, n-1\}$. Fix another natural number $j ∈ N$ coprime to $n$. Each number in $N$ is now colored with one of two colors, say red or black, so that:

1. $i$ and $n-i$ always receive the same color, and
2. $i$ and $|j-i|$ receive the same color for all $i ∈ N, i ≠ j$.

Prove that all numbers in $N$ must receive the same color.

Solution

Let $a \sim b$ denote that $a$ and $b$ have the same color. Because $j$ is coprime to $n$, every number in $N$ is of the form $kj\bmod n$ for a unique $1 ≤ k < n$, so it suffices to show that $kj\bmod n \sim (k-1)j\bmod n$ for $1 < k < n$. In this range of $k$, $kj\bmod n ≠ j$, so

• if $kj\bmod n > j$, $kj\bmod n \sim kj\bmod n - j = (k-1)j\bmod n$ using rule 2;
• if $kj\bmod n < j$, $kj\bmod n \sim j - kj\bmod n \sim n - j + kj\bmod n = (k-1)j\bmod n$ using rule 2 then rule 1.

def Imo1985Q2.Condition (n j : ℕ) (C : ℕ → Fin 2) : Prop

The conditions on the problem's coloring C. Although its domain is all of ℕ, we only care about its values in Set.Ico 1 n.

Equations

• Imo1985Q2.Condition n j C = ((∀ i ∈ Set.Ico 1 n, C i = C (n - i)) ∧ ∀ i ∈ Set.Ico 1 n, i ≠ j → C i = C (↑j - ↑i).natAbs)

theorem Imo1985Q2.C_mul_mod {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : n.Coprime j) {C : ℕ → Fin 2} (hC : Condition n j C) {k : ℕ} (hk : k ∈ Set.Ico 1 n) : C (k * j % n) = C j

For 1 ≤ k < n, k * j % n has the same color as j.

theorem Imo1985Q2.result {n j : ℕ} (hn : 3 ≤ n) (hj : j ∈ Set.Ico 1 n) (cpj : n.Coprime j) {C : ℕ → Fin 2} (hC : Condition n j C) {i : ℕ} (hi : i ∈ Set.Ico 1 n) : C i = C j