IMO 2010 Q5

Each of the six boxes $B_1, B_2, B_3, B_4, B_5, B_6$ initially contains one coin. The following two types of operations are allowed:

1. Choose a non-empty box $B_j, 1 ≤ j ≤ 5$, remove one coin from $B_j$ and add two coins to $B_{j+1}$;
2. Choose a non-empty box $B_k, 1 ≤ k ≤ 4$, remove one coin from $B_k$ and swap the contents (possibly empty) of the boxes $B_{k+1}$ and $B_{k+2}$.

Determine if there exists a finite sequence of operations of the allowed types, such that the five boxes $B_1, B_2, B_3, B_4, B_5$ become empty, while box $B_6$ contains exactly $2010^{2010^{2010}}$ coins.

Solution

We follow the solution from https://web.evanchen.cc/exams/IMO-2010-notes.pdf.

From the initial state we can reach (0, 0, 5, 11, 0, 0); we now ignore the first two boxes. On any three adjacent boxes reading (n, 0, 0) with n > 0 we can change them to (0, 2^n, 0):

(n, 0, 0) →(move 1) (n-1, 2, 0)
          →(2× move 1) (n-1, 0, 4) →(move 2) (n-2, 4, 0)
          →(4× move 1) (n-2, 0, 8) →(move 2) (n-3, 8, 0)
          → ...
          →(2^(n-1)× move 1) (1, 0, 2^n) →(move 2) (0, 2^n, 0)

Thus we can get more than enough coins, all in box 4, as follows:

(5, 11, 0, 0) → (5, 0, 2^11, 0) →(move 2) (4, 2^11, 0, 0)
              → (4, 0, 2^2^11, 0) →(move 2) (3, 2^2^11, 0, 0)
              → ...
              → (1, 0, 2^2^2^2^2^11, 0) →(move 2) (0, 2^2^2^2^2^11, 0, 0)

We now ignore the third box. Let T = 2010^2010^2010 be the target number of coins; since T < 2^2^2^2^2^11 and T is divisible by 4 we can drop coins from box 4 by using move 2 to swap the empty boxes 5 and 6 until we have (T/4, 0, 0). Then we can repeatedly use move 1 to get (0, T/2, 0) and finally (0, 0, T).

inductive Imo2010Q5.Reachable : (Fin 6 → ℕ) → Prop

The predicate defining states of boxes reachable by the given moves.

• base : Reachable 1

  The starting position with one coin in each box

• move1 {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 5) (pB : 0 < B i) : Reachable (B - Pi.single i 1 + Pi.single (i + 1) 2)

  Remove a coin from $B_j$ and add two coins to $B_{j+1}$

• move2 {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) : Reachable (B ∘ ⇑(Equiv.swap (i + 1) (i + 2)) - Pi.single i 1)

  Remove a coin from $B_k$ and swap $B_{k+1}$ and $B_{k+2}$

theorem Imo2010Q5.single_succ {k : ℕ} {i : Fin 6} : Pi.single (i + 1) k i = 0

theorem Imo2010Q5.single_succ' {k : ℕ} {i : Fin 6} : Pi.single i k (i + 1) = 0

theorem Imo2010Q5.single_add_two {k : ℕ} {i : Fin 6} : Pi.single (i + 2) k i = 0

@[irreducible]

theorem Imo2010Q5.Reachable.push {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 5) : Reachable (B - Pi.single i (B i) + Pi.single (i + 1) (2 * B i))

Empty $B_i$ and add twice its coins to $B_{i+1}$ by repeatedly applying move 1.

theorem Imo2010Q5.Reachable.five_eleven : Reachable (Pi.single 2 5 + Pi.single 3 11)

(0, 0, 5, 11, 0, 0) is reachable.

theorem Imo2010Q5.Reachable.double {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 2) = 0) : Reachable (B + Pi.single (i + 1) (B (i + 1)) - Pi.single i 1)

Decrement $B_i$ and double $B_{i+1}$, assuming $B_{i+2} = 0$, by doing push, move2.

@[irreducible]

theorem Imo2010Q5.Reachable.doubles {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (zB : B (i + 2) = 0) : Reachable (Function.update (B - Pi.single i (B i)) (i + 1) (B (i + 1) * 2 ^ B i))

double as many times as possible, emptying $B_i$ and doubling $B_{i+1}$ that many times.

theorem Imo2010Q5.Reachable.exp {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 1) = 0) (zB' : B (i + 2) = 0) : Reachable (B - Pi.single i (B i) + Pi.single (i + 1) (2 ^ B i))

Empty $B_i$ and set $B_{i+1} = 2^{B_i}$, assuming $B_{i+1} = B_{i+2} = 0$.

theorem Imo2010Q5.Reachable.exp_mid {k n : ℕ} (h : Reachable (Pi.single 2 (k + 1) + Pi.single 3 n)) (hn : 0 < n) : Reachable (Pi.single 2 k + Pi.single 3 (2 ^ n))

From (0, 0, k+1, n, 0, 0) with n > 0 we can reach (0, 0, k, 2^n, 0, 0).

theorem Imo2010Q5.Reachable.reduce {m n : ℕ} (h : Reachable (Pi.single 3 n)) (hmn : m ≤ n) : Reachable (Pi.single 3 m)

If all coins are in box 4, their number can be reduced by any desired amount.

theorem Imo2010Q5.Reachable.tower_inequality {m n : ℕ} (hm : m = 2010) (hn : n = 11) : 2010 ^ 2010 ^ m ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ n

The key power tower inequality in the solution.

theorem Imo2010Q5.Reachable.quarter_target {m : ℕ} (hm : m = 2010) : Reachable (Pi.single 3 (2010 ^ 2010 ^ m / 4))

(0, 0, 0, 2010 ^ 2010 ^ 2010 / 4, 0, 0) is reachable.

theorem Imo2010Q5.result : Reachable (Pi.single 5 (2010 ^ 2010 ^ 2010))