module
public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.ZMod.Basic
public import Mathlib.Tactic.Ring
public section
/-!
# USA Mathematical Olympiad 2024, Problem 4
Let m and n be positive integers. A circular necklace contains mn beads, each
either red or blue. It turned out that no matter how the necklace was cut into
m blocks of n consecutive beads, each block had a distinct number of red beads.
Determine, with proof, all possible values of the ordered pair (m, n).
-/
namespace Usa2024P4
/-- A circular necklace with `m * n` beads, each red (`true`) or blue (`false`).
The beads are indexed by their position on the circle, i.e. by `ZMod (m * n)`. -/
abbrev Necklace (m n : ℕ) := ZMod (m * n) → Bool
/-- The number of red beads in the block of `n` consecutive beads starting at
position `s + i * n` (positions are taken modulo `m * n`). -/
def blockCount {m n : ℕ} (c : Necklace m n) (s : ZMod (m * n)) (i : ℕ) : ℕ :=
∑ j ∈ Finset.range n, if c (s + ((i * n + j : ℕ) : ZMod (m * n))) then 1 else 0
/-- The property from the problem statement: no matter how the necklace is cut
into `m` blocks of `n` consecutive beads (the cut is determined by the starting
position `s` of the first block), the numbers of red beads in the `m` blocks
are pairwise distinct. -/
def AllCutsDistinct {m n : ℕ} (c : Necklace m n) : Prop :=
∀ s : ZMod (m * n), Function.Injective (fun i : Fin m ↦ blockCount c s i.val)
/-- The answer: the required necklaces exist exactly for the pairs `(m, n)`
with `m ≤ n + 1`. -/
/- determine -/ abbrev solution : ℕ → ℕ → Prop := sorry
theorem usa2024_p4 (m n : ℕ) (hm : 0 < m) (hn : 0 < n) :
(∃ c : Necklace m n, AllCutsDistinct c) ↔ solution m n := sorry
end Usa2024P4
This problem has a complete formalized solution.