Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2025P6

module

public import Mathlib.Tactic
public import Mathlib.Algebra.BigOperators.Fin
public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Combinatorics.Hall.Basic
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Real.Basic
public import Mathlib.Data.ZMod.Basic
public import Mathlib.Tactic.Abel
public import Mathlib.Tactic.Linarith.Lemmas
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2025, Problem 6

Let `m` and `n` be positive integers with `m ≥ n`. There are `m` cupcakes of different
flavors arranged around a circle and `n` people who like cupcakes. Each person assigns
a nonnegative real number score to each cupcake, depending on how much they like the
cupcake. Suppose that for each person `P`, it is possible to partition the circle of
`m` cupcakes into `n` groups of consecutive cupcakes so that the sum of `P`'s scores
of the cupcakes in each group is at least 1. Prove that it is possible to distribute
the `m` cupcakes to the `n` people so that each person `P` receives cupcakes of total
score at least 1 with respect to `P`.
-/

namespace Usa2025P6

/-!
## Circular partitions

The circle of `m` cupcakes is modeled by `ZMod m`; arcs are intervals of consecutive
cupcakes and a `CirclePartition` is a partition of the circle into such arcs.
-/

/-- An arc of length `l` starting at `c` on the circle `ZMod m`. -/
def arcSet {m : ℕ} (c : ZMod m) (l : ℕ) : Finset (ZMod m) :=
  (Finset.range l).image (fun t : ℕ => c + (t : ZMod m))


/-- A partition of the circle `ZMod m` into `k` consecutive nonempty arcs,
described by a basepoint and the list of arc lengths. -/
structure CirclePartition (m k : ℕ) where
  base : ZMod m
  len : Fin k → ℕ
  len_pos : ∀ i, 1 ≤ len i
  len_sum : ∑ i, len i = m


namespace CirclePartition

variable {m k : ℕ} (P : CirclePartition m k)

/-- The offset of arc `i`: total length of the preceding arcs. -/
def off (i : Fin k) : ℕ := ∑ j ∈ Finset.univ.filter (· < i), P.len j

/-- The starting point of arc `i`. -/
def start (i : Fin k) : ZMod m := P.base + (P.off i : ZMod m)

/-- The `i`-th arc as a finset. -/
def arcOf (i : Fin k) : Finset (ZMod m) := arcSet (P.start i) (P.len i)


end CirclePartition

/-- The USAMO 2025 Problem 6: distributing cupcakes to people so that everybody
gets total score at least one in their own ranking. -/
theorem usa2025_p6 {m n : ℕ} [NeZero m] (hm : 0 < m) (hn : 0 < n) (hmn : n ≤ m)
    (like : Fin n → ZMod m → ℝ) (hnn : ∀ p c, 0 ≤ like p c)
    (hpart : ∀ p, ∃ P : CirclePartition m n, ∀ i, 1 ≤ ∑ x ∈ P.arcOf i, like p x) :
    ∃ a : ZMod m → Fin n, ∀ p, 1 ≤ ∑ c ∈ Finset.univ.filter (a · = p), like p c := sorry

end Usa2025P6

File author(s): Kimi K3

This problem has a complete formalized solution.