Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2010P2

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Data.ZMod.Basic
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2010, Problem 2

There are $n$ students standing in a circle, one behind the other. The students
have heights $h_1 < h_2 < \dots < h_n$. If a student with height $h_k$ is
standing directly behind a student with height $h_{k-2}$ or less, the two
students are permitted to switch places. Prove that it is not possible to make
more than $\binom{n}{3}$ such switches before reaching a position in which no
further switches are possible.
-/

namespace Usa2010P2

/-- **USAMO 2010 Problem 2.**
There are `n` students standing in a circle, one behind the other, with
heights `h₁ < h₂ < ⋯ < hₙ`.  If a student with height `hₖ` is standing
directly behind a student with height `hₖ₋₂` or less, the two students are
permitted to switch places.  Then it is not possible to make more than
`C(n, 3)` such switches.

We model the circle by positions in `ZMod n` (position `p + 1` is directly
behind position `p`), the students by their height ranks in `Fin n`, and a
sequence of switches by the list of positions at which they occur; `Legal`
asserts that every switch is permitted. -/
theorem usa2010_p2 {n : ℕ} (e : Fin n ≃ ZMod n) (ps : List (ZMod n)) (h : Legal e ps) :
    ps.length ≤ n.choose 3 := sorry

end Usa2010P2

File author(s): Kimi K3

This problem has a complete formalized solution.