IMO 2024 Q5

Turbo the snail plays a game on a board with $2024$ rows and $2023$ columns. There are hidden monsters in $2022$ of the cells. Initially, Turbo does not know where any of the monsters are, but he knows that there is exactly one monster in each row except the first row and the last row, and that each column contains at most one monster.

Turbo makes a series of attempts to go from the first row to the last row. On each attempt, he chooses to start on any cell in the first row, then repeatedly moves to an adjacent cell sharing a common side. (He is allowed to return to a previously visited cell.) If he reaches a cell with a monster, his attempt ends and he is transported back to the first row to start a new attempt. The monsters do not move, and Turbo remembers whether or not each cell he has visited contains a monster. If he reaches any cell in the last row, his attempt ends and the game is over.

Determine the minimum value of $n$ for which Turbo has a strategy that guarantees reaching the last row on the $n$th attempt or earlier, regardless of the locations of the monsters.

We follow the solution from the official solutions. To show that $n$ is at least $3$, it is possible that the first cell Turbo encounters in the second row on his first attempt contains a monster, and also possible that the first cell Turbo encounters in the third row on his second attempt contains a monster. To show that $3$ attempts suffice, the first attempt can be used to locate the monster in the second row; if this is not at either side of the board, two more attempts suffice to pass behind that monster and from there go along its column to the last row, while if it is at one side of the board, the second attempt follows a zigzag path such that if it encounters a monster the third attempt can avoid all monsters.

Definitions for setting up the problem

@[reducible, inline]

abbrev Imo2024Q5.Cell (N : ℕ) : Type

A cell on the board for the game.

Equations

• Imo2024Q5.Cell N = (Fin (N + 2) × Fin (N + 1))

@[reducible, inline]

abbrev Imo2024Q5.InteriorRow (N : ℕ) : Type

A row that is neither the first nor the last (and thus contains a monster).

Equations

• Imo2024Q5.InteriorRow N = ↑(Set.Icc 1 ⟨N, ⋯⟩)

@[reducible, inline]

abbrev Imo2024Q5.MonsterData (N : ℕ) : Type

Data for valid positions of the monsters.

Equations

• Imo2024Q5.MonsterData N = (Imo2024Q5.InteriorRow N ↪ Fin (N + 1))

def Imo2024Q5.MonsterData.monsterCells {N : ℕ} (m : Imo2024Q5.MonsterData N) : Set (Imo2024Q5.Cell N)

The cells with monsters as a Set, given an injection from rows to columns.

Equations

• m.monsterCells = Set.range fun (x : Imo2024Q5.InteriorRow N) => (↑x, m x)

def Imo2024Q5.Adjacent {N : ℕ} (x y : Imo2024Q5.Cell N) : Prop

Whether two cells are adjacent.

Equations

• Imo2024Q5.Adjacent x y = ((↑x.1).dist ↑y.1 + (↑x.2).dist ↑y.2 = 1)

structure Imo2024Q5.Path (N : ℕ) : Type

A valid path from the first to the last row.

• cells : List (Imo2024Q5.Cell N)

  The cells on the path.

• nonempty : self.cells ≠ []
• head_first_row : (self.cells.head ⋯).1 = 0
• last_last_row : (self.cells.getLast ⋯).1 = ↑N + 1
• valid_move_seq : List.Chain' Imo2024Q5.Adjacent self.cells

noncomputable def Imo2024Q5.Path.firstMonster {N : ℕ} (p : Imo2024Q5.Path N) (m : Imo2024Q5.MonsterData N) : Option (Imo2024Q5.Cell N)

The first monster on a path, or none.

Equations

• p.firstMonster m = List.find? (fun (x : Imo2024Q5.Cell N) => decide (x ∈ m.monsterCells)) p.cells

@[reducible, inline]

abbrev Imo2024Q5.Strategy (N : ℕ) : Type

A strategy, given the results of initial attempts, returns a path for the next attempt.

Equations

• Imo2024Q5.Strategy N = (⦃k : ℕ⦄ → (Fin k → Option (Imo2024Q5.Cell N)) → Imo2024Q5.Path N)

noncomputable def Imo2024Q5.Strategy.play {N : ℕ} (s : Imo2024Q5.Strategy N) (m : Imo2024Q5.MonsterData N) (k : ℕ) : Fin k → Option (Imo2024Q5.Cell N)

Playing a strategy, k attempts.

Equations

• s.play m 0 = Fin.elim0
• s.play m k.succ = Fin.snoc (s.play m k) ((s (s.play m k)).firstMonster m)

def Imo2024Q5.Strategy.WinsIn {N : ℕ} (s : Imo2024Q5.Strategy N) (m : Imo2024Q5.MonsterData N) (k : ℕ) : Prop

The predicate for a strategy winning within the given number of attempts.

Equations

• s.WinsIn m k = (none ∈ Set.range (s.play m k))

def Imo2024Q5.Strategy.ForcesWinIn {N : ℕ} (s : Imo2024Q5.Strategy N) (k : ℕ) : Prop

Whether a strategy forces a win within the given number of attempts.

Equations

• s.ForcesWinIn k = ∀ (m : Imo2024Q5.MonsterData N), s.WinsIn m k

API definitions and lemmas about Cell

def Imo2024Q5.Cell.reflect {N : ℕ} (c : Imo2024Q5.Cell N) : Imo2024Q5.Cell N

Reflecting a cell of the board (swapping left and right sides of the board).

Equations

• c.reflect = (c.1, c.2.rev)

API definitions and lemmas about MonsterData

def Imo2024Q5.row1 {N : ℕ} (hN : 2 ≤ N) : Imo2024Q5.InteriorRow N

The row 1, in the form required for MonsterData.

Equations

• Imo2024Q5.row1 hN = ⟨1, ⋯⟩

theorem Imo2024Q5.coe_coe_row1 {N : ℕ} (hN : 2 ≤ N) : ↑↑(Imo2024Q5.row1 hN) = 1

def Imo2024Q5.row2 {N : ℕ} (hN : 2 ≤ N) : Imo2024Q5.InteriorRow N

The row 2, in the form required for MonsterData.

Equations

• Imo2024Q5.row2 hN = ⟨⟨2, ⋯⟩, ⋯⟩

def Imo2024Q5.MonsterData.reflect {N : ℕ} (m : Imo2024Q5.MonsterData N) : Imo2024Q5.MonsterData N

Reflecting monster data.

Equations

• m.reflect = { toFun := Fin.rev ∘ ⇑m, inj' := ⋯ }

theorem Imo2024Q5.MonsterData.reflect_reflect {N : ℕ} (m : Imo2024Q5.MonsterData N) : m.reflect.reflect = m

theorem Imo2024Q5.MonsterData.not_mem_monsterCells_of_fst_eq_zero {N : ℕ} (m : Imo2024Q5.MonsterData N) {c : Imo2024Q5.Cell N} (hc : c.1 = 0) : c ∉ m.monsterCells

theorem Imo2024Q5.MonsterData.le_N_of_mem_monsterCells {N : ℕ} {m : Imo2024Q5.MonsterData N} {c : Imo2024Q5.Cell N} (hc : c ∈ m.monsterCells) : ↑c.1 ≤ N

theorem Imo2024Q5.MonsterData.mk_mem_monsterCells_iff_of_le {N : ℕ} {m : Imo2024Q5.MonsterData N} {r : Fin (N + 2)} (hr1 : 1 ≤ r) (hrN : r ≤ ⟨N, ⋯⟩) {c : Fin (N + 1)} : (r, c) ∈ m.monsterCells ↔ m ⟨r, ⋯⟩ = c

theorem Imo2024Q5.MonsterData.mem_monsterCells_iff_of_le {N : ℕ} {m : Imo2024Q5.MonsterData N} {x : Imo2024Q5.Cell N} (hr1 : 1 ≤ x.1) (hrN : x.1 ≤ ⟨N, ⋯⟩) : x ∈ m.monsterCells ↔ m ⟨x.1, ⋯⟩ = x.2

theorem Imo2024Q5.MonsterData.mk_mem_monsterCells_iff {N : ℕ} {m : Imo2024Q5.MonsterData N} {r : Fin (N + 2)} {c : Fin (N + 1)} : (r, c) ∈ m.monsterCells ↔ ∃ (hr1 : 1 ≤ r) (hrN : r ≤ ⟨N, ⋯⟩), m ⟨r, ⋯⟩ = c

API definitions and lemmas about Adjacent

theorem Imo2024Q5.Adjacent.le_of_lt {N : ℕ} {x y : Imo2024Q5.Cell N} (ha : Imo2024Q5.Adjacent x y) {r : Fin (N + 2)} (hr : r < y.1) : r ≤ x.1

API definitions and lemmas about Path

theorem Imo2024Q5.Path.exists_mem_fst_eq {N : ℕ} (p : Imo2024Q5.Path N) (r : Fin (N + 2)) : ∃ c ∈ p.cells, c.1 = r

theorem Imo2024Q5.Path.exists_mem_le_fst {N : ℕ} (p : Imo2024Q5.Path N) (r : Fin (N + 2)) : ∃ c ∈ p.cells, r ≤ c.1

def Imo2024Q5.Path.findFstEq {N : ℕ} (p : Imo2024Q5.Path N) (r : Fin (N + 2)) : Imo2024Q5.Cell N

The first path element on a row.

Equations

• p.findFstEq r = (List.find? (fun (c : Imo2024Q5.Cell N) => decide (c.1 = r)) p.cells).get ⋯

theorem Imo2024Q5.Path.find_eq_some_findFstEq {N : ℕ} (p : Imo2024Q5.Path N) (r : Fin (N + 2)) : List.find? (fun (c : Imo2024Q5.Cell N) => decide (c.1 = r)) p.cells = some (p.findFstEq r)

theorem Imo2024Q5.Path.findFstEq_mem_cells {N : ℕ} (p : Imo2024Q5.Path N) (r : Fin (N + 2)) : p.findFstEq r ∈ p.cells

theorem Imo2024Q5.Path.findFstEq_fst {N : ℕ} (p : Imo2024Q5.Path N) (r : Fin (N + 2)) : (p.findFstEq r).1 = r

theorem Imo2024Q5.find?_eq_eq_find?_le {N : ℕ} {l : List (Imo2024Q5.Cell N)} {r : Fin (N + 2)} (hne : l ≠ []) (hf : (l.head hne).1 ≤ r) (ha : List.Chain' Imo2024Q5.Adjacent l) : List.find? (fun (c : Imo2024Q5.Cell N) => decide (c.1 = r)) l = List.find? (fun (c : Imo2024Q5.Cell N) => decide (r ≤ c.1)) l

theorem Imo2024Q5.Path.findFstEq_eq_find?_le {N : ℕ} (p : Imo2024Q5.Path N) (r : Fin (N + 2)) : p.findFstEq r = (List.find? (fun (c : Imo2024Q5.Cell N) => decide (r ≤ c.1)) p.cells).get ⋯

theorem Imo2024Q5.Path.firstMonster_isSome {N : ℕ} {p : Imo2024Q5.Path N} {m : Imo2024Q5.MonsterData N} : (p.firstMonster m).isSome = true ↔ ∃ x ∈ p.cells, x ∈ m.monsterCells

theorem Imo2024Q5.Path.firstMonster_eq_none {N : ℕ} {p : Imo2024Q5.Path N} {m : Imo2024Q5.MonsterData N} : p.firstMonster m = none ↔ ∀ x ∈ p.cells, x ∉ m.monsterCells

theorem Imo2024Q5.Path.one_lt_length_cells {N : ℕ} (p : Imo2024Q5.Path N) : 1 < p.cells.length

def Imo2024Q5.Path.tail {N : ℕ} (p : Imo2024Q5.Path N) : Imo2024Q5.Path N

Remove the first cell from a path, if the second cell is also on the first row.

Equations

• p.tail = { cells := if p.cells[1].1 = 0 then p.cells.tail else p.cells, nonempty := ⋯, head_first_row := ⋯, last_last_row := ⋯, valid_move_seq := ⋯ }

theorem Imo2024Q5.Path.tail_induction {N : ℕ} {motive : Imo2024Q5.Path N → Prop} (ind : ∀ (p : Imo2024Q5.Path N), motive p.tail → motive p) (base : ∀ (p : Imo2024Q5.Path N), p.cells[1].1 ≠ 0 → motive p) (p : Imo2024Q5.Path N) : motive p

theorem Imo2024Q5.Path.tail_findFstEq {N : ℕ} (p : Imo2024Q5.Path N) {r : Fin (N + 2)} (hr : r ≠ 0) : p.tail.findFstEq r = p.findFstEq r

theorem Imo2024Q5.Path.tail_firstMonster {N : ℕ} (p : Imo2024Q5.Path N) (m : Imo2024Q5.MonsterData N) : p.tail.firstMonster m = p.firstMonster m

theorem Imo2024Q5.Path.firstMonster_eq_of_findFstEq_mem {N : ℕ} {p : Imo2024Q5.Path N} {m : Imo2024Q5.MonsterData N} (h : p.findFstEq 1 ∈ m.monsterCells) : p.firstMonster m = some (p.findFstEq 1)

theorem Imo2024Q5.Path.findFstEq_fst_sub_one_mem {N : ℕ} (p : Imo2024Q5.Path N) {r : Fin (N + 2)} (hr : r ≠ 0) : (⟨↑r - 1, ⋯⟩, (p.findFstEq r).2) ∈ p.cells

theorem Imo2024Q5.Path.mem_of_firstMonster_eq_some {N : ℕ} {p : Imo2024Q5.Path N} {m : Imo2024Q5.MonsterData N} {c : Imo2024Q5.Cell N} (h : p.firstMonster m = some c) : c ∈ p.cells ∧ c ∈ m.monsterCells

def Imo2024Q5.Path.ofFn {N m : ℕ} (f : Fin m → Imo2024Q5.Cell N) (hm : m ≠ 0) (hf : (f ⟨0, ⋯⟩).1 = 0) (hl : (f ⟨m - 1, ⋯⟩).1 = ⟨N + 1, ⋯⟩) (ha : ∀ (i : ℕ) (hi : i + 1 < m), Imo2024Q5.Adjacent (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)) : Imo2024Q5.Path N

Convert a function giving the cells of a path to a Path.

Equations

• Imo2024Q5.Path.ofFn f hm hf hl ha = { cells := List.ofFn f, nonempty := ⋯, head_first_row := ⋯, last_last_row := ⋯, valid_move_seq := ⋯ }

theorem Imo2024Q5.Path.ofFn_cells {N m : ℕ} (f : Fin m → Imo2024Q5.Cell N) (hm : m ≠ 0) (hf : (f ⟨0, ⋯⟩).1 = 0) (hl : (f ⟨m - 1, ⋯⟩).1 = ⟨N + 1, ⋯⟩) (ha : ∀ (i : ℕ) (hi : i + 1 < m), Imo2024Q5.Adjacent (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)) : (Imo2024Q5.Path.ofFn f hm hf hl ha).cells = List.ofFn f

theorem Imo2024Q5.Path.ofFn_firstMonster_eq_none {N m : ℕ} (f : Fin m → Imo2024Q5.Cell N) (hm : m ≠ 0) (hf : (f ⟨0, ⋯⟩).1 = 0) (hl : (f ⟨m - 1, ⋯⟩).1 = ⟨N + 1, ⋯⟩) (ha : ∀ (i : ℕ) (hi : i + 1 < m), Imo2024Q5.Adjacent (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)) (m✝ : Imo2024Q5.MonsterData N) : (Imo2024Q5.Path.ofFn f hm hf hl ha).firstMonster m✝ = none ↔ ∀ (i : Fin m), f i ∉ m✝.monsterCells

def Imo2024Q5.Path.reflect {N : ℕ} (p : Imo2024Q5.Path N) : Imo2024Q5.Path N

Reflecting a path.

Equations

• p.reflect = { cells := List.map Imo2024Q5.Cell.reflect p.cells, nonempty := ⋯, head_first_row := ⋯, last_last_row := ⋯, valid_move_seq := ⋯ }

theorem Imo2024Q5.Path.firstMonster_reflect {N : ℕ} (p : Imo2024Q5.Path N) (m : Imo2024Q5.MonsterData N) : p.reflect.firstMonster m.reflect = Option.map Imo2024Q5.Cell.reflect (p.firstMonster m)

API definitions and lemmas about Strategy

theorem Imo2024Q5.Strategy.play_comp_castLE {N : ℕ} (s : Imo2024Q5.Strategy N) (m : Imo2024Q5.MonsterData N) {k₁ k₂ : ℕ} (hk : k₁ ≤ k₂) : s.play m k₂ ∘ Fin.castLE hk = s.play m k₁

theorem Imo2024Q5.Strategy.play_apply_of_le {N : ℕ} (s : Imo2024Q5.Strategy N) (m : Imo2024Q5.MonsterData N) {i k₁ k₂ : ℕ} (hi : i < k₁) (hk : k₁ ≤ k₂) : s.play m k₂ ⟨i, ⋯⟩ = s.play m k₁ ⟨i, hi⟩

theorem Imo2024Q5.Strategy.play_zero {N : ℕ} (s : Imo2024Q5.Strategy N) (m : Imo2024Q5.MonsterData N) {k : ℕ} (hk : 0 < k) : s.play m k ⟨0, hk⟩ = (s Fin.elim0).firstMonster m

theorem Imo2024Q5.Strategy.play_one {N : ℕ} (s : Imo2024Q5.Strategy N) (m : Imo2024Q5.MonsterData N) {k : ℕ} (hk : 1 < k) : s.play m k ⟨1, hk⟩ = (s ![(s Fin.elim0).firstMonster m]).firstMonster m

theorem Imo2024Q5.Strategy.play_two {N : ℕ} (s : Imo2024Q5.Strategy N) (m : Imo2024Q5.MonsterData N) {k : ℕ} (hk : 2 < k) : s.play m k ⟨2, hk⟩ = (s ![(s Fin.elim0).firstMonster m, (s ![(s Fin.elim0).firstMonster m]).firstMonster m]).firstMonster m

theorem Imo2024Q5.Strategy.WinsIn.mono {N : ℕ} (s : Imo2024Q5.Strategy N) (m : Imo2024Q5.MonsterData N) {k₁ k₂ : ℕ} (h : s.WinsIn m k₁) (hk : k₁ ≤ k₂) : s.WinsIn m k₂

theorem Imo2024Q5.Strategy.ForcesWinIn.mono {N : ℕ} (s : Imo2024Q5.Strategy N) {k₁ k₂ : ℕ} (h : s.ForcesWinIn k₁) (hk : k₁ ≤ k₂) : s.ForcesWinIn k₂

Proof of lower bound with constructions used therein

def Imo2024Q5.baseMonsterData (N : ℕ) : Imo2024Q5.MonsterData N

An arbitrary choice of monster positions, which is modified to put selected monsters in desired places.

Equations

• Imo2024Q5.baseMonsterData N = { toFun := fun (x : Imo2024Q5.InteriorRow N) => match x with | ⟨r, ⋯⟩ => ⟨↑r, ⋯⟩, inj' := ⋯ }

def Imo2024Q5.monsterData12 {N : ℕ} (hN : 2 ≤ N) (c₁ c₂ : Fin (N + 1)) : Imo2024Q5.MonsterData N

Positions for monsters with specified columns in the second and third rows (rows 1 and 2).

Equations

• Imo2024Q5.monsterData12 hN c₁ c₂ = (Function.Embedding.setValue (Imo2024Q5.baseMonsterData N) (Imo2024Q5.row2 hN) c₂).setValue (Imo2024Q5.row1 hN) c₁

theorem Imo2024Q5.monsterData12_apply_row2 {N : ℕ} (hN : 2 ≤ N) {c₁ c₂ : Fin (N + 1)} (h : c₁ ≠ c₂) : (Imo2024Q5.monsterData12 hN c₁ c₂) (Imo2024Q5.row2 hN) = c₂

theorem Imo2024Q5.row1_mem_monsterCells_monsterData12 {N : ℕ} (hN : 2 ≤ N) (c₁ c₂ : Fin (N + 1)) : (1, c₁) ∈ (Imo2024Q5.monsterData12 hN c₁ c₂).monsterCells

theorem Imo2024Q5.row2_mem_monsterCells_monsterData12 {N : ℕ} (hN : 2 ≤ N) {c₁ c₂ : Fin (N + 1)} (h : c₁ ≠ c₂) : (⟨2, ⋯⟩, c₂) ∈ (Imo2024Q5.monsterData12 hN c₁ c₂).monsterCells

theorem Imo2024Q5.Strategy.not_forcesWinIn_two {N : ℕ} (s : Imo2024Q5.Strategy N) (hN : 2 ≤ N) : ¬s.ForcesWinIn 2

theorem Imo2024Q5.Strategy.ForcesWinIn.three_le {N : ℕ} {s : Imo2024Q5.Strategy N} {k : ℕ} (hf : s.ForcesWinIn k) (hN : 2 ≤ N) : 3 ≤ k

Proof of upper bound and constructions used therein

def Imo2024Q5.fn0 (N : ℕ) : Fin (2 * N + 2) → Imo2024Q5.Cell N

The first attempt in a winning strategy, as a function: first pass along the second row to locate the monster there.

Equations

• Imo2024Q5.fn0 N i = if i = 0 then (0, 0) else if h : ↑i < N + 2 then (1, ⟨↑i - 1, ⋯⟩) else (⟨↑i - N, ⋯⟩, ⟨N, ⋯⟩)

theorem Imo2024Q5.injective_fn0 (N : ℕ) : Function.Injective (Imo2024Q5.fn0 N)

def Imo2024Q5.path0 {N : ℕ} (hN : 2 ≤ N) : Imo2024Q5.Path N

The first attempt in a winning strategy, as a Path.

Equations

• Imo2024Q5.path0 hN = Imo2024Q5.Path.ofFn (Imo2024Q5.fn0 N) ⋯ ⋯ ⋯ ⋯

def Imo2024Q5.fn1OfNotEdge {N : ℕ} {c₁ : Fin (N + 1)} (hc₁ : c₁ ≠ 0) : Fin (N + 3) → Imo2024Q5.Cell N

The second attempt in a winning strategy, as a function, if the monster in the second row is not at an edge: pass to the left of that monster then along its column.

Equations

• Imo2024Q5.fn1OfNotEdge hc₁ i = if h : ↑i ≤ 2 then (⟨↑i, ⋯⟩, ⟨↑c₁ - 1, ⋯⟩) else (⟨↑i - 1, ⋯⟩, c₁)

def Imo2024Q5.path1OfNotEdge {N : ℕ} {c₁ : Fin (N + 1)} (hc₁ : c₁ ≠ 0) : Imo2024Q5.Path N

The second attempt in a winning strategy, as a function, if the monster in the second row is not at an edge.

Equations

• Imo2024Q5.path1OfNotEdge hc₁ = Imo2024Q5.Path.ofFn (Imo2024Q5.fn1OfNotEdge hc₁) ⋯ ⋯ ⋯ ⋯

def Imo2024Q5.fn2OfNotEdge {N : ℕ} {c₁ : Fin (N + 1)} (hc₁ : ↑c₁ ≠ N) : Fin (N + 3) → Imo2024Q5.Cell N

The third attempt in a winning strategy, as a function, if the monster in the second row is not at an edge: pass to the right of that monster then along its column.

Equations

• Imo2024Q5.fn2OfNotEdge hc₁ i = if h : ↑i ≤ 2 then (⟨↑i, ⋯⟩, ⟨↑c₁ + 1, ⋯⟩) else (⟨↑i - 1, ⋯⟩, c₁)

def Imo2024Q5.path2OfNotEdge {N : ℕ} {c₁ : Fin (N + 1)} (hc₁ : ↑c₁ ≠ N) : Imo2024Q5.Path N

The third attempt in a winning strategy, as a function, if the monster in the second row is not at an edge.

Equations

• Imo2024Q5.path2OfNotEdge hc₁ = Imo2024Q5.Path.ofFn (Imo2024Q5.fn2OfNotEdge hc₁) ⋯ ⋯ ⋯ ⋯

def Imo2024Q5.fn1OfEdge0 (N : ℕ) : Fin (2 * N + 1) → Imo2024Q5.Cell N

The second attempt in a winning strategy, as a function, if the monster in the second row is at the left edge: zigzag across the board so that, if we encounter a monster, we have a third path we know will not encounter a monster.

Equations

• Imo2024Q5.fn1OfEdge0 N i = if h : ↑i = 2 * N then (⟨N + 1, ⋯⟩, ⟨N, ⋯⟩) else (⟨(↑i + 1) / 2, ⋯⟩, ⟨↑i / 2 + 1, ⋯⟩)

def Imo2024Q5.path1OfEdge0 {N : ℕ} (hN : 2 ≤ N) : Imo2024Q5.Path N

The second attempt in a winning strategy, as a Path, if the monster in the second row is at the left edge.

Equations

• Imo2024Q5.path1OfEdge0 hN = Imo2024Q5.Path.ofFn (Imo2024Q5.fn1OfEdge0 N) ⋯ ⋯ ⋯ ⋯

def Imo2024Q5.path1OfEdgeN {N : ℕ} (hN : 2 ≤ N) : Imo2024Q5.Path N

The second attempt in a winning strategy, as a Path, if the monster in the second row is at the right edge.

Equations

• Imo2024Q5.path1OfEdgeN hN = (Imo2024Q5.path1OfEdge0 hN).reflect

def Imo2024Q5.fn2OfEdge0 {N : ℕ} {r : Fin (N + 2)} (hr : ↑r ≤ N) : Fin (N + 2 * ↑r - 1) → Imo2024Q5.Cell N

The third attempt in a winning strategy, as a function, if the monster in the second row is at the left edge and the second (zigzag) attempt encountered a monster: on the row before the monster was encountered, move to the following row one place earlier, proceed to the left edge and then along that column.

Equations

• Imo2024Q5.fn2OfEdge0 hr i = if h₁ : ↑i + 2 < 2 * ↑r then (⟨(↑i + 1) / 2, ⋯⟩, ⟨↑i / 2 + 1, ⋯⟩) else if h₂ : ↑i + 2 < 3 * ↑r then (r, ⟨3 * ↑r - 3 - ↑i, ⋯⟩) else (⟨↑i + 3 - 2 * ↑r, ⋯⟩, 0)

theorem Imo2024Q5.fn2OfEdge0_apply_eq_fn1OfEdge0_apply_of_lt {N : ℕ} {r : Fin (N + 2)} (hr : ↑r ≤ N) {i : ℕ} (h : i + 2 < 2 * ↑r) : Imo2024Q5.fn2OfEdge0 hr ⟨i, ⋯⟩ = Imo2024Q5.fn1OfEdge0 N ⟨i, ⋯⟩

def Imo2024Q5.path2OfEdge0 {N : ℕ} (hN : 2 ≤ N) {r : Fin (N + 2)} (hr2 : 2 ≤ ↑r) (hrN : ↑r ≤ N) : Imo2024Q5.Path N

The third attempt in a winning strategy, as a Path, if the monster in the second row is at the left edge and the second (zigzag) attempt encountered a monster.

Equations

• Imo2024Q5.path2OfEdge0 hN hr2 hrN = Imo2024Q5.Path.ofFn (Imo2024Q5.fn2OfEdge0 hrN) ⋯ ⋯ ⋯ ⋯

def Imo2024Q5.path2OfEdge0Def {N : ℕ} (hN : 2 ≤ N) (r : Fin (N + 2)) : Imo2024Q5.Path N

The third attempt in a winning strategy, as a Path, if the monster in the second row is at the left edge and the second (zigzag) attempt encountered a monster, version that works with junk values of r for convenience in defining the strategy before needing to prove things about exactly where it can encounter monsters.

Equations

• Imo2024Q5.path2OfEdge0Def hN r = if h : 2 ≤ ↑r ∧ ↑r ≤ N then Imo2024Q5.path2OfEdge0 hN ⋯ ⋯ else Imo2024Q5.path2OfEdge0 hN Imo2024Q5.path2OfEdge0Def.proof_4 hN

def Imo2024Q5.path2OfEdgeNDef {N : ℕ} (hN : 2 ≤ N) (r : Fin (N + 2)) : Imo2024Q5.Path N

The third attempt in a winning strategy, as a Path, if the monster in the second row is at the right edge and the second (zigzag) attempt encountered a monster.

Equations

• Imo2024Q5.path2OfEdgeNDef hN r = (Imo2024Q5.path2OfEdge0Def hN r).reflect

def Imo2024Q5.path1 {N : ℕ} (hN : 2 ≤ N) (c₁ : Fin (N + 1)) : Imo2024Q5.Path N

The second attempt in a winning strategy, given the column of the monster in the second row, as a Path.

Equations

• Imo2024Q5.path1 hN c₁ = if hc₁ : c₁ = 0 then Imo2024Q5.path1OfEdge0 hN else if ↑c₁ = N then Imo2024Q5.path1OfEdgeN hN else Imo2024Q5.path1OfNotEdge hc₁

def Imo2024Q5.path2 {N : ℕ} (hN : 2 ≤ N) (c₁ : Fin (N + 1)) (r : Fin (N + 2)) : Imo2024Q5.Path N

The third attempt in a winning strategy, given the column of the monster in the second row and the row of the monster (if any) found in the second attempt, as a Path.

Equations

• Imo2024Q5.path2 hN c₁ r = if c₁ = 0 then Imo2024Q5.path2OfEdge0Def hN r else if hc₁N : ↑c₁ = N then Imo2024Q5.path2OfEdgeNDef hN r else Imo2024Q5.path2OfNotEdge hc₁N

def Imo2024Q5.winningStrategy {N : ℕ} (hN : 2 ≤ N) : Imo2024Q5.Strategy N

A strategy that wins in three attempts.

Equations

• Imo2024Q5.winningStrategy hN = fun (x : Fin 0 → Option (Imo2024Q5.Cell N)) => Imo2024Q5.path0 hN
• Imo2024Q5.winningStrategy hN = fun (r : Fin 1 → Option (Imo2024Q5.Cell N)) => Imo2024Q5.path1 hN ((r 0).getD 0).2
• Imo2024Q5.winningStrategy hN = fun (r : Fin (n + 2) → Option (Imo2024Q5.Cell N)) => Imo2024Q5.path2 hN ((r 0).getD 0).2 ((r 1).getD 0).1

theorem Imo2024Q5.path0_firstMonster_eq_apply_row1 {N : ℕ} (hN : 2 ≤ N) (m : Imo2024Q5.MonsterData N) : (Imo2024Q5.path0 hN).firstMonster m = some (1, m (Imo2024Q5.row1 hN))

theorem Imo2024Q5.winningStrategy_play_one {N : ℕ} (hN : 2 ≤ N) (m : Imo2024Q5.MonsterData N) : (Imo2024Q5.winningStrategy hN).play m 3 ⟨1, ⋯⟩ = (Imo2024Q5.path1 hN (m (Imo2024Q5.row1 hN))).firstMonster m

theorem Imo2024Q5.winningStrategy_play_two {N : ℕ} (hN : 2 ≤ N) (m : Imo2024Q5.MonsterData N) : (Imo2024Q5.winningStrategy hN).play m 3 ⟨2, ⋯⟩ = (Imo2024Q5.path2 hN (m (Imo2024Q5.row1 hN)) (((Imo2024Q5.path1 hN (m (Imo2024Q5.row1 hN))).firstMonster m).getD 0).1).firstMonster m

theorem Imo2024Q5.path1_firstMonster_of_not_edge {N : ℕ} (hN : 2 ≤ N) {m : Imo2024Q5.MonsterData N} (hc₁0 : m (Imo2024Q5.row1 hN) ≠ 0) (hc₁N : ↑(m (Imo2024Q5.row1 hN)) ≠ N) : (Imo2024Q5.path1 hN (m (Imo2024Q5.row1 hN))).firstMonster m = none ∨ (Imo2024Q5.path1 hN (m (Imo2024Q5.row1 hN))).firstMonster m = some (⟨2, ⋯⟩, ⟨↑(m (Imo2024Q5.row1 hN)) - 1, ⋯⟩)

theorem Imo2024Q5.path2_firstMonster_of_not_edge {N : ℕ} (hN : 2 ≤ N) {m : Imo2024Q5.MonsterData N} (hc₁0 : m (Imo2024Q5.row1 hN) ≠ 0) (hc₁N : ↑(m (Imo2024Q5.row1 hN)) ≠ N) (r : Fin (N + 2)) : (Imo2024Q5.path2 hN (m (Imo2024Q5.row1 hN)) r).firstMonster m = none ∨ (Imo2024Q5.path2 hN (m (Imo2024Q5.row1 hN)) r).firstMonster m = some (⟨2, ⋯⟩, ⟨↑(m (Imo2024Q5.row1 hN)) + 1, ⋯⟩)

theorem Imo2024Q5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_not_edge {N : ℕ} (hN : 2 ≤ N) {m : Imo2024Q5.MonsterData N} (hc₁0 : m (Imo2024Q5.row1 hN) ≠ 0) (hc₁N : ↑(m (Imo2024Q5.row1 hN)) ≠ N) : (Imo2024Q5.winningStrategy hN).play m 3 ⟨1, ⋯⟩ = none ∨ (Imo2024Q5.winningStrategy hN).play m 3 ⟨2, ⋯⟩ = none

theorem Imo2024Q5.path2OfEdge0_firstMonster_eq_none_of_path1OfEdge0_firstMonster_eq_some {N : ℕ} (hN : 2 ≤ N) {x : Imo2024Q5.Cell N} (hx2 : 2 ≤ ↑x.1) (hxN : ↑x.1 ≤ N) {m : Imo2024Q5.MonsterData N} (hc₁0 : m (Imo2024Q5.row1 hN) = 0) (hx : (Imo2024Q5.path1OfEdge0 hN).firstMonster m = some x) : (Imo2024Q5.path2OfEdge0 hN hx2 hxN).firstMonster m = none

theorem Imo2024Q5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_zero {N : ℕ} (hN : 2 ≤ N) {m : Imo2024Q5.MonsterData N} (hc₁0 : m (Imo2024Q5.row1 hN) = 0) : (Imo2024Q5.winningStrategy hN).play m 3 ⟨1, ⋯⟩ = none ∨ (Imo2024Q5.winningStrategy hN).play m 3 ⟨2, ⋯⟩ = none

theorem Imo2024Q5.winningStrategy_play_one_of_edge_N {N : ℕ} (hN : 2 ≤ N) {m : Imo2024Q5.MonsterData N} (hc₁N : ↑(m (Imo2024Q5.row1 hN)) = N) : (Imo2024Q5.winningStrategy hN).play m 3 ⟨1, ⋯⟩ = Option.map Imo2024Q5.Cell.reflect ((Imo2024Q5.winningStrategy hN).play m.reflect 3 ⟨1, ⋯⟩)

theorem Imo2024Q5.winningStrategy_play_two_of_edge_N {N : ℕ} (hN : 2 ≤ N) {m : Imo2024Q5.MonsterData N} (hc₁N : ↑(m (Imo2024Q5.row1 hN)) = N) : (Imo2024Q5.winningStrategy hN).play m 3 ⟨2, ⋯⟩ = Option.map Imo2024Q5.Cell.reflect ((Imo2024Q5.winningStrategy hN).play m.reflect 3 ⟨2, ⋯⟩)

theorem Imo2024Q5.winningStrategy_play_one_eq_none_or_play_two_eq_none_of_edge_N {N : ℕ} (hN : 2 ≤ N) {m : Imo2024Q5.MonsterData N} (hc₁N : ↑(m (Imo2024Q5.row1 hN)) = N) : (Imo2024Q5.winningStrategy hN).play m 3 ⟨1, ⋯⟩ = none ∨ (Imo2024Q5.winningStrategy hN).play m 3 ⟨2, ⋯⟩ = none

theorem Imo2024Q5.winningStrategy_play_one_eq_none_or_play_two_eq_none {N : ℕ} (hN : 2 ≤ N) (m : Imo2024Q5.MonsterData N) : (Imo2024Q5.winningStrategy hN).play m 3 ⟨1, ⋯⟩ = none ∨ (Imo2024Q5.winningStrategy hN).play m 3 ⟨2, ⋯⟩ = none

theorem Imo2024Q5.winningStrategy_forcesWinIn_three {N : ℕ} (hN : 2 ≤ N) : (Imo2024Q5.winningStrategy hN).ForcesWinIn 3

def Imo2024Q5.answer : ℕ

This is to be determined by the solver of the original problem (and much of the difficulty for contestants is in finding this answer rather than spending time attempting to prove a conjectured answer around log₂ 2023).

Equations

• Imo2024Q5.answer = 3

theorem Imo2024Q5.result : IsLeast {k : ℕ | ∃ (s : Imo2024Q5.Strategy 2022), s.ForcesWinIn k} Imo2024Q5.answer

The final result, combining upper and lower bounds.