`Compfiles/Usa2012P2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

6 declarations, 0 contain sorry, 0 declared as axioms

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).

Imports (4)

Imported by 1 file

Compfiles.lean

def Usa2012P2.arcDist The arc distance between two of the 432 points: the number of unit arcs in the shorter of the two arcs joining them line 49 source
Source documentation
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.

standard axioms: Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat
Proof uses: Min.min, ZMod.val, HSub.hSub
10 instances, coercions and auxiliary constants left out.
```
def arcDist (x y : ZMod 432) : ℕ := min (x - y).val (y - x).val
…
```
lemma Usa2012P2.arcDist_add Arc distance is invariant under rotations line 59 source
Source documentation
Arc distance is invariant under rotations.

standard axioms: Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Usa2012P2.arcDist, HAdd.hAdd
Proof uses: id, Eq.mpr, Min.min, ZMod.val, HSub.hSub, congrArg, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma arcDist_add (x y t : ZMod 432) : arcDist (x + t) (y + t) = arcDist x y := by
…
```
Mentions: Usa2012P2.arcDist
lemma Usa2012P2.mem_filter_color line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Fin, Iff, Membership.mem, Finset, Finset.filter, Eq, Finset.univ
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, And, true_and, iff_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P2.disjoint_color Different color classes are disjoint line 68 source
Source documentation
Different color classes are disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Fin, Ne, Disjoint, Finset, Finset.filter, Eq, Finset.univ
Proof uses: Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, Eq.trans, Eq.symm, Eq.mp, Usa2012P2.mem_filter_color
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma disjoint_color {color : ZMod 432 → Fin 4} {i j : Fin 4} (hij : i ≠ j) :
    Disjoint (Finset.univ.filter fun x => color x = i)
      (Finset.univ.filter fun x => color x = j) := by
…
```
lemma Usa2012P2.exists_rotation Pigeonhole over rotations line 82 source
Source documentation
Pigeonhole over rotations. Suppose that no rotation in avoid moves a point of S onto a point of C, and that (432 - #avoid) * k < #S * #C. Each of the #S * #C pairs (x, c) ∈ S × C determines a unique rotation sending x to c, and this rotation lies outside avoid; averaging over the 432 - #avoid allowed rotations, some rotation moves more than k points of S onto C.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, ZMod, OfNat.ofNat, Nat, Membership.mem, Not, HAdd.hAdd, LT.lt, HMul.hMul, HSub.hSub, Finset.card, Exists, And, LE.le
Proof uses: Finset.filter, Eq, Finset.sum, SDiff.sdiff, Finset.univ, Finset.ext, Eq.mpr, Iff, id, congr, congrArg, Eq.trans, congrFun', True, true_and, Iff.intro, And.right, And.intro, Finset.card_bij, Eq.mp and 24 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma exists_rotation {S C avoid : Finset (ZMod 432)} {k : ℕ}
    (havoid : ∀ x ∈ S, ∀ t ∈ avoid, x + t ∉ C)
    (hcard : (432 - avoid.card) * k < S.card * C.card) :
    ∃ t, t ∉ avoid ∧ ∃ T, T ⊆ S ∧ k < T.card ∧ ∀ x ∈ T, x + t ∈ C := by
…
```
Mentions: S
problem Usa2012P2.usa2012_p2 line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Fin, Eq, Finset.card, Finset.filter, Finset.univ, Exists, Finset, And, Membership.mem, HAdd.hAdd, Usa2012P2.arcDist
Proof uses: Not, Singleton.singleton, LE.le, LT.lt, Usa2012P2.exists_rotation, Eq.mpr, id, congrArg, add_zero, Iff.mp, Disjoint, Finset.disjoint_left, Usa2012P2.disjoint_color, Ne, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm and 28 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 72 steps
Open to load the checked before-and-after goal states.