Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2012P2

module

public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.ZMod.Basic
public import Mathlib.Tactic.Abel

public section


/-!
# USA Mathematical Olympiad 2012, Problem 2

A circle is divided into 432 congruent arcs by 432 points. The points are
colored in four colors such that some 108 points are colored Red, some 108
points are colored Green, some 108 points are colored Blue, and the remaining
108 points are colored Yellow. Prove that one can choose three points of each
color in such a way that the four triangles formed by the chosen points of the
same color are congruent.

## Formalization notes

We identify the 432 points with `ZMod 432`; a rotation of the circle is then
addition of a constant. The coloring is a map `color : ZMod 432 → Fin 4`,
where `0, 1, 2, 3` stand for red, green, blue and yellow. We prove the
stronger statement that the four triangles can be chosen to be rotations of
one another: there is a red triangle `U` and rotations `t₁, t₂, t₃` such that
`U + t₁`, `U + t₂`, `U + t₃` are green, blue and yellow triangles. Since the
pairwise arc distances of the vertices are preserved by rotations, the four
triangles are congruent (equal chord lengths, hence SSS).
-/

namespace Usa2012P2

/-- The arc distance between two of the 432 points: the number of unit arcs
in the shorter of the two arcs joining them. The chord through `x` and `y` has
length `2R sin(π·d/432)` with `d = arcDist x y`, which is strictly increasing
in `d ∈ [0, 216]`; hence two inscribed triangles with equal pairwise arc
distances have equal side lengths and are congruent. -/
def arcDist (x y : ZMod 432) : ℕ := min (x - y).val (y - x).val

theorem usa2012_p2 (color : ZMod 432 → Fin 4)
    (hcolor : ∀ i, (Finset.univ.filter fun x => color x = i).card = 108) :
    ∃ (U : Finset (ZMod 432)) (t₁ t₂ t₃ : ZMod 432),
      U.card = 3 ∧
      (∀ x ∈ U, color x = 0) ∧
      (∀ x ∈ U, color (x + t₁) = 1) ∧
      (∀ x ∈ U, color (x + t₂) = 2) ∧
      (∀ x ∈ U, color (x + t₃) = 3) ∧
      (∀ x ∈ U, ∀ y ∈ U, arcDist x y = arcDist (x + t₁) (y + t₁)) ∧
      (∀ x ∈ U, ∀ y ∈ U, arcDist x y = arcDist (x + t₂) (y + t₂)) ∧
      (∀ x ∈ U, ∀ y ∈ U, arcDist x y = arcDist (x + t₃) (y + t₃)) := sorry

end Usa2012P2

File author(s): Kimi K3

This problem has a complete formalized solution.