Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2013P3

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Group.Nat.Range
public import Mathlib.Data.Fintype.BigOperators
public import Mathlib.Order.Lattice.Nat
public import Mathlib.Tactic.IntervalCases

public section


/-!
# USA Mathematical Olympiad 2013, Problem 3

Let n be a positive integer. There are n(n+1)/2 tokens, each with a black
side and a white side, arranged into an equilateral triangle, with the
biggest row containing n tokens. Initially, each token has the white side
up. An operation is to choose a line parallel to the sides of the triangle,
and flip all the tokens on that line. A configuration is called admissible
if it can be obtained from the initial configuration by performing a finite
number of operations. For each admissible configuration C, let f(C) denote
the smallest number of operations required to obtain C from the initial
configuration. Find the maximum value of f(C), where C varies over all
admissible configurations.
-/

namespace Usa2013P3

/-! ### Basic definitions -/

/-- The tokens are indexed by pairs `(a, b)` of natural numbers with
`a + b < n`. One should think of barycentric coordinates `(a, b, c)` with
`a + b + c = n - 1`, so that `c = n - 1 - a - b` is determined. -/
def Token (n : ℕ) := { p : ℕ × ℕ // p.1 + p.2 < n }

lemma lt_left {n a b : ℕ} (h : a + b < n) : a < n := by lia
lemma lt_right {n a b : ℕ} (h : a + b < n) : b < n := by lia
lemma lt_third {n a b : ℕ} (h : a + b < n) : n - 1 - a - b < n := by lia

/-- A choice of lines to flip: for each of the three directions and each
`i < n`, whether the `i`-th line in that direction is flipped. The three
lines through the token `(a, b, c)` are the `a`-th, `b`-th and `c`-th lines
of the three directions respectively. -/
@[ext]
structure Moves (n : ℕ) where
  x : Fin n → Bool
  y : Fin n → Bool
  z : Fin n → Bool

/-- The configuration reached from the initial (all-white) configuration by
performing the moves `v`: token `(a, b)` ends up black iff an odd number of
the three lines through it were flipped. -/
def applyMoves {n : ℕ} (v : Moves n) (t : Token n) : Bool :=
  v.x ⟨t.1.1, lt_left t.2⟩ ^^
  v.y ⟨t.1.2, lt_right t.2⟩ ^^
  v.z ⟨n - 1 - t.1.1 - t.1.2, lt_third t.2⟩

/-- A configuration is admissible if it can be obtained from the initial
configuration by a finite number of operations. Since the operations commute
and are involutions, every sequence of operations is described by a `Moves`. -/
def Admissible {n : ℕ} (C : Token n → Bool) : Prop := ∃ v : Moves n, applyMoves v = C

/-- The number of operations in a `Moves`: the total number of flipped lines. -/
def weight {n : ℕ} (v : Moves n) : ℕ :=
  (Finset.univ.filter fun i => v.x i = true).card +
  (Finset.univ.filter fun i => v.y i = true).card +
  (Finset.univ.filter fun i => v.z i = true).card

/-- `f C` is the smallest number of operations required to obtain `C`. -/
noncomputable def f {n : ℕ} (C : Token n → Bool) : ℕ :=
  sInf {m : ℕ | ∃ v : Moves n, applyMoves v = C ∧ weight v = m}

/- determine -/ abbrev answer (n : ℕ) : ℕ := sorry

theorem usa2013_p3 (n : ℕ) (hn : 0 < n) :
    IsGreatest {m : ℕ | ∃ C : Token n → Bool, Admissible C ∧ f C = m} (answer n) := sorry

end Usa2013P3

File author(s): Kimi K3

This problem has a complete formalized solution.