`Compfiles/Usa2011P2.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

11 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2011, Problem 2

An integer is assigned to each vertex of a regular pentagon so that the sum of the five integers is 2011. A turn of a solitaire game consists of subtracting an integer m (not necessarily positive) from each of the integers at two neighboring vertices and adding 2m to the opposite vertex, which is not adjacent to either of the first two vertices. (The amount m and the vertices chosen can vary from turn to turn.) The game is won at a certain vertex if, after some number of turns, that vertex has the number 2011 and the other four vertices have the number 0. Prove that for any choice of the initial integers, there is exactly one vertex at which the game can be won.

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Usa2011P2.Config A configuration of the game: an integer at each vertex of the pentagon line 38 source
Source documentation
A configuration of the game: an integer at each vertex of the pentagon. The vertices are indexed by ZMod 5, so that the neighbors of vertex i are i - 1 and i + 1.

no axioms what this means
Proof uses: ZMod, OfNat.ofNat, Nat, Int
1 instances, coercions and auxiliary constants left out.
```
abbrev Config := ZMod 5 → ℤ
```
def Usa2011P2.Reachable Reachability of configurations line 48 source
Source documentation
Reachability of configurations. A turn at the edge i, i + 1 with amount m subtracts m from the values at the vertices i and i + 1 and adds 2 * m to the value at the opposite vertex i + 3 (the unique vertex adjacent to neither of them). The effects of successive turns add up, so a sequence of turns is described by integers x j, the sum of the amounts of the turns whose opposite vertex is j. Such a turn has edge j + 2, j + 3, hence vertex i gains 2 * x i in total and loses x (i + 2) + x (i + 3). Conversely any choice of x is realized by doing one turn per edge.

standard axioms: Quot.sound, propext what this means
Statement uses: Usa2011P2.Config
Proof uses: Exists, ZMod, OfNat.ofNat, Nat, Int, Eq, HSub.hSub, HAdd.hAdd, HMul.hMul
20 instances, coercions and auxiliary constants left out.
```
def Reachable (a b : Config) : Prop :=
…
```
Mentions: Usa2011P2.Config
def Usa2011P2.WinAt The game is won at vertex v from the configuration a if the configuration with value 2011 at v and 0 at the other four vertices is reachable from a line 54 source
Source documentation
The game is won at vertex v from the configuration a if the configuration with value 2011 at v and 0 at the other four vertices is reachable from a.

standard axioms: Quot.sound, propext what this means
Statement uses: Usa2011P2.Config, ZMod, OfNat.ofNat, Nat
Proof uses: Usa2011P2.Reachable, Pi.single, Int
7 instances, coercions and auxiliary constants left out.
```
def WinAt (a : Config) (v : ZMod 5) : Prop :=
…
```
Mentions: Usa2011P2.Config
def Usa2011P2.invariant The invariant of the game: the weighted sum of the values, where the value at vertex i has weight i line 59 source
Source documentation
The invariant of the game: the weighted sum of the values, where the value at vertex i has weight i. A turn changes it by a multiple of 5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2011P2.Config, ZMod, OfNat.ofNat, Nat
Proof uses: Finset.sum, Finset.univ, HMul.hMul
15 instances, coercions and auxiliary constants left out.
```
def invariant (a : Config) : ZMod 5 := ∑ i, i * (a i : ZMod 5)
…
```
Mentions: Usa2011P2.Config
lemma Usa2011P2.zmod5_sum line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, ZMod, OfNat.ofNat, Nat, Eq, Finset.sum, Finset.univ, HAdd.hAdd
Proof uses: Fin.sum_univ_five
22 instances, coercions and auxiliary constants left out.
lemma Usa2011P2.zmod5_cases line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Or, Eq
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2011P2.key_identity The key identity behind the invariance of invariant: the weight of a turn at edge i, i + 1 is i + (i + 1) = 2 * (i + 3) - 5 line 76 source
Source documentation
The key identity behind the invariance of invariant: the weight of a turn at edge i, i + 1 is i + (i + 1) = 2 * (i + 3) - 5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Finset.sum, Finset.univ, HMul.hMul, HSub.hSub, HAdd.hAdd
Proof uses: Fintype.sum_equiv, Equiv.addRight, id, Equiv, Eq.mpr, congrArg, add_sub_cancel_right, Eq.refl, Trans.trans, Eq.symm, Finset.sum_sub_distrib, Finset.sum_congr, rfl, Finset, Membership.mem, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 47 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma key_identity (X : ZMod 5 → ZMod 5) :
    (∑ i, i * (2 * X i - X (i + 2) - X (i + 3))) = 0 := by
…
```
lemma Usa2011P2.invariant_eq_of_reachable The invariant is preserved by any sequence of turns line 102 source
Source documentation
The invariant is preserved by any sequence of turns.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2011P2.Config, Usa2011P2.Reachable, Eq, ZMod, OfNat.ofNat, Nat, Usa2011P2.invariant
Proof uses: Int, HSub.hSub, HAdd.hAdd, HMul.hMul, Finset.sum, Finset.univ, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_add_distrib, Finset.sum_congr, rfl, Finset, Membership.mem, congrFun', Eq.trans, Int.cast_sub, Int.cast_add, Int.cast_mul and 41 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma invariant_eq_of_reachable {a b : Config} (h : Reachable a b) :
    invariant b = invariant a := by
…
```
Mentions: Usa2011P2.Config, h, Usa2011P2.Reachable, Usa2011P2.invariant
lemma Usa2011P2.invariant_single The invariant of the configuration won at vertex v; since 2011 ≡ 1 (mod 5), it equals v line 120 source
Source documentation
The invariant of the configuration won at vertex v; since 2011 ≡ 1 (mod 5), it equals v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Usa2011P2.invariant, Pi.single, Int
Proof uses: id, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, congrArg, Finset.sum_eq_single, Membership.mem, Finset, Ne, Pi.single_eq_of_ne, Int.cast_zero, MulZeroClass.mul_zero, Eq.refl, Not, absurd, Finset.mem_univ, Pi.single_eq_same, of_decide_eq_true, Bool and 3 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma invariant_single (v : ZMod 5) : invariant (Pi.single v 2011) = v := by
…
```
Mentions: Usa2011P2.invariant
lemma Usa2011P2.win_at_zero The core existence lemma: a configuration with sum 2011 and vanishing invariant can be won at vertex 0 line 134 source
Source documentation
The core existence lemma: a configuration with sum 2011 and vanishing invariant can be won at vertex 0. With k given by a 1 + 2 * a 2 + 3 * a 3 + 4 * a 4 = 5 * k, the explicit solution is x 0 = 0, x 1 = -k - a 1, x 2 = -2 * k + a 3 + a 4, x 3 = -3 * k + a 2 + a 3 + 2 * a 4, x 4 = -4 * k + a 2 + 2 * a 3 + 2 * a 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2011P2.Config, Eq, Int, Finset.sum, ZMod, OfNat.ofNat, Nat, Finset.univ, Usa2011P2.invariant, Usa2011P2.WinAt
Proof uses: Dvd.dvd, HAdd.hAdd, HMul.hMul, Eq.mpr, id, congrFun', congrArg, Eq.trans, Int.cast_add, congr, Int.cast_mul, Int.cast_ofNat, Mathlib.Tactic.LinearCombination.eq_of_eq, Eq.mp, Usa2011P2.zmod5_sum, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, HSub.hSub, Mathlib.Tactic.Ring.Common.sub_congr, HPow.hPow and 49 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma win_at_zero (a : Config) (hsum : ∑ i, a i = 2011) (hinv : invariant a = 0) :
    WinAt a 0 := by
…
```
Mentions: Usa2011P2.Config, Usa2011P2.invariant, Usa2011P2.WinAt
problem Usa2011P2.usa2011_p2 line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2011P2.Config, Eq, Int, Finset.sum, ZMod, OfNat.ofNat, Nat, Finset.univ, ExistsUnique, Usa2011P2.WinAt
Proof uses: Exists.intro, And, Usa2011P2.invariant, And.intro, HAdd.hAdd, Fintype.sum_equiv, Equiv.addRight, rfl, Eq.mp, congrArg, HMul.hMul, HSub.hSub, id, Equiv, Eq.mpr, add_sub_cancel_right, Eq.refl, Finset.mul_sum, Eq.symm, Finset.sum_sub_distrib and 60 more
91 instances, coercions and auxiliary constants left out.

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