Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2008P3

module

public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.BigOperators.Group.List
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Interval
public import Mathlib.Data.Int.ModEq
public import Mathlib.Data.Int.Star
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Lemmas
public import Mathlib.Tactic.NormNum.Abs
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2008, Problem 3

Let n be a positive integer. Denote by Sₙ the set of points (x, y)
with integer coordinates such that

  |x| + |y + 1/2| < n.

A path is a sequence of distinct points (x₁, y₁), (x₂, y₂), ..., (x_ℓ, y_ℓ)
in Sₙ such that, for i = 2, ..., ℓ, the distance between (xᵢ, yᵢ) and
(xᵢ₋₁, yᵢ₋₁) is 1. Prove that the points in Sₙ cannot be partitioned into
fewer than n paths.
-/

namespace Usa2008P3

/-- The half-width of the row of `S n` at height `y`: the row consists of the
points `(x, y)` with `|x| ≤ rowK n y`. -/
def rowK (n : ℕ) (y : ℤ) : ℤ := if 0 ≤ y then (n : ℤ) - 1 - y else (n : ℤ) + y

/-- The set `Sₙ` of the problem, namely the integer points `(x, y)` with
`|x| + |y + 1/2| < n`.  Multiplying by two, this is `2|x| + |2y + 1| < 2n`,
and we build the set row by row. -/
noncomputable def S (n : ℕ) : Finset (ℤ × ℤ) :=
  (Finset.Icc (-(n : ℤ)) ((n : ℤ) - 1)).biUnion fun y ↦
    (Finset.Icc (-(rowK n y)) (rowK n y)) ×ˢ {y}

/-- Two lattice points are adjacent when their (Manhattan) distance is 1. -/
def Adj (p q : ℤ × ℤ) : Prop := |p.1 - q.1| + |p.2 - q.2| = 1

/-- USAMO 2008, Problem 3: any partition of `Sₙ` into paths uses at least
`n` paths.  We model a partition as a list of lists of points: each list is a
path (its points are distinct, lie in `S n`, and consecutive points are
adjacent), the lists are pairwise disjoint, and together they cover `S n`. -/
theorem usa2008_p3 (n : ℕ) (hn : 0 < n) (paths : List (List (ℤ × ℤ)))
    (hmem : ∀ P ∈ paths, ∀ p ∈ P, p ∈ S n)
    (hnodup : ∀ P ∈ paths, P.Nodup)
    (hchain : ∀ P ∈ paths, P.IsChain Adj)
    (hdisj : paths.Pairwise List.Disjoint)
    (hcover : ∀ p ∈ S n, ∃ P ∈ paths, p ∈ P) :
    n ≤ paths.length := sorry

end Usa2008P3

File author(s): Kimi K3

This problem has a complete formalized solution.