Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2011P2

module

public import Mathlib.Algebra.BigOperators.Fin
public import Mathlib.Data.ZMod.Basic
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2011, Problem 2

An integer is assigned to each vertex of a regular pentagon so that the sum of
the five integers is 2011. A turn of a solitaire game consists of subtracting
an integer m (not necessarily positive) from each of the integers at two
neighboring vertices and adding 2m to the opposite vertex, which is not
adjacent to either of the first two vertices. (The amount m and the vertices
chosen can vary from turn to turn.) The game is won at a certain vertex if,
after some number of turns, that vertex has the number 2011 and the other four
vertices have the number 0. Prove that for any choice of the initial integers,
there is exactly one vertex at which the game can be won.
-/

namespace Usa2011P2

/-- A configuration of the game: an integer at each vertex of the pentagon.
The vertices are indexed by `ZMod 5`, so that the neighbors of vertex `i` are
`i - 1` and `i + 1`. -/
abbrev Config := ZMod 5 → ℤ

/-- Reachability of configurations. A turn at the edge `i, i + 1` with amount
`m` subtracts `m` from the values at the vertices `i` and `i + 1` and adds
`2 * m` to the value at the opposite vertex `i + 3` (the unique vertex adjacent
to neither of them). The effects of successive turns add up, so a sequence of
turns is described by integers `x j`, the sum of the amounts of the turns whose
opposite vertex is `j`. Such a turn has edge `j + 2, j + 3`, hence vertex `i`
gains `2 * x i` in total and loses `x (i + 2) + x (i + 3)`. Conversely any
choice of `x` is realized by doing one turn per edge. -/
def Reachable (a b : Config) : Prop :=
  ∃ x : ZMod 5 → ℤ, ∀ i, b i = a i + 2 * x i - x (i + 2) - x (i + 3)

/-- The game is won at vertex `v` from the configuration `a` if the
configuration with value 2011 at `v` and 0 at the other four vertices is
reachable from `a`. -/
def WinAt (a : Config) (v : ZMod 5) : Prop :=
  Reachable a (Pi.single v 2011)

/-- The invariant of the game: the weighted sum of the values, where the value
at vertex `i` has weight `i`. A turn changes it by a multiple of 5. -/
def invariant (a : Config) : ZMod 5 := ∑ i, i * (a i : ZMod 5)

theorem usa2011_p2 (a : Config) (hsum : ∑ i, a i = 2011) :
    ∃! v, WinAt a v := sorry

end Usa2011P2

File author(s): Kimi K3

This problem has a complete formalized solution.