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

37 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2003, Problem 6

At the vertices of a regular hexagon are written six nonnegative integers whose sum is 2003^2003. Bert is allowed to make moves of the following form: he may pick a vertex and replace the number written there by the absolute value of the difference between the numbers written at the two neighboring vertices. Prove that Bert can make a sequence of moves, after which the number 0 appears at all six vertices.

Imports (7)

Imported by 1 file

Compfiles.lean

abbrev Usa2003P6.Conf A configuration of six integers at the vertices of a hexagon line 37 source
Source documentation
A configuration of six integers at the vertices of a hexagon.

no axioms what this means
Proof uses: ZMod, OfNat.ofNat, Nat, Int
1 instances, coercions and auxiliary constants left out.
```
abbrev Conf := ZMod 6 → ℤ
```
def Usa2003P6.step One move at vertex j: replace the number at j by the absolute value of the difference of the numbers at the two neighboring vertices line 41 source
Source documentation
One move at vertex j: replace the number at j by the absolute value of the difference of the numbers at the two neighboring vertices.

standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat
Proof uses: Function.update, Int, abs, HSub.hSub, HAdd.hAdd
21 instances, coercions and auxiliary constants left out.
```
def step (f : Conf) (j : ZMod 6) : Conf := Function.update f j |f (j - 1) - f (j + 1)|
```
Mentions: f, Usa2003P6.Conf
def Usa2003P6.Moves Moves f g means that configuration g can be reached from f by a sequence of moves line 45 source
Source documentation
Moves f g means that configuration g can be reached from f by a sequence of moves.

standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf
Proof uses: Exists, List, ZMod, OfNat.ofNat, Nat, Eq, List.foldl, Usa2003P6.step
1 instances, coercions and auxiliary constants left out.
```
def Moves (f g : Conf) : Prop := ∃ l : List (ZMod 6), l.foldl step f = g
```
Mentions: f, Usa2003P6.Conf, Usa2003P6.step
lemma Usa2003P6.Moves.refl line 47 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, Usa2003P6.Moves
Proof uses: Exists.intro, List, ZMod, OfNat.ofNat, Nat, Eq, List.foldl, Usa2003P6.step, List.nil, rfl
1 instances, coercions and auxiliary constants left out.
lemma Usa2003P6.Moves.trans line 49 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, Usa2003P6.Moves
Proof uses: List, ZMod, OfNat.ofNat, Nat, Eq, List.foldl, Usa2003P6.step, Exists.intro, HAppend.hAppend, Eq.mpr, id, congrArg, List.foldl_append, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Usa2003P6.cmax The maximum entry of a configuration line 55 source
Source documentation
The maximum entry of a configuration.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, Int
Proof uses: Finset.max', Finset.image, ZMod, OfNat.ofNat, Nat, Finset.univ
6 instances, coercions and auxiliary constants left out.
```
noncomputable def cmax (f : Conf) : ℤ :=
…
```
Mentions: f, Usa2003P6.Conf
lemma Usa2003P6.le_cmax line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, LE.le, Int, Usa2003P6.cmax
Proof uses: Finset.le_max', Finset.image, Finset.univ, Finset.mem_image_of_mem, Finset.mem_univ
7 instances, coercions and auxiliary constants left out.
lemma Usa2003P6.cmax_le line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, Int, ZMod, OfNat.ofNat, Nat, LE.le, Usa2003P6.cmax
Proof uses: Finset.max'_le, Finset.image, Finset.univ, Membership.mem, Finset, And, Eq, Exists, Iff.mp, Finset.mem_image
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.cmax_attained line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, Exists, ZMod, OfNat.ofNat, Nat, Eq, Int, Usa2003P6.cmax
Proof uses: Membership.mem, Finset, Finset.image, Finset.univ, Finset.max', Finset.Nonempty.image, Finset.univ_nonempty, Finset.max'_mem, And, Iff.mp, Finset.mem_image, Exists.intro
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.odd_iff_cast line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Iff, Odd, Eq, ZMod, OfNat.ofNat, Nat
Proof uses: Iff.symm, ZMod.intCast_eq_one_iff_odd
22 instances, coercions and auxiliary constants left out.
lemma Usa2003P6.even_iff_cast line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Iff, Even, Eq, ZMod, OfNat.ofNat, Nat
Proof uses: Iff.symm, ZMod.intCast_eq_zero_iff_even
27 instances, coercions and auxiliary constants left out.
lemma Usa2003P6.odd_sum_iff line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, Iff, Odd, Int, Finset.sum, ZMod, OfNat.ofNat, Nat, Finset.univ, Eq
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Int.cast_sum, Usa2003P6.odd_iff_cast
45 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.one_le_of_odd line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, Odd
Proof uses: Eq, HAdd.hAdd, HMul.hMul, Eq.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.two_le_of_even_pos line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LT.lt, OfNat.ofNat, Even, LE.le
Proof uses: Eq, HAdd.hAdd, Eq.symm
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa2003P6.step2 The move on parity vectors: in ZMod 2 the absolute difference becomes a sum line 93 source
Source documentation
The move on parity vectors: in ZMod 2 the absolute difference becomes a sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat
Proof uses: Function.update, HAdd.hAdd, HSub.hSub
22 instances, coercions and auxiliary constants left out.
```
def step2 (v : ZMod 6 → ZMod 2) (j : ZMod 6) : ZMod 6 → ZMod 2 :=
…
```
lemma Usa2003P6.par_step line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, Eq, Usa2003P6.step, Usa2003P6.step2
Proof uses: funext, dite, Eq.mpr, abs, Int, HSub.hSub, HAdd.hAdd, id, congr, congrArg, Function.update_self, ZMod.intCast_abs_mod_two, Int.cast_sub, Neg.neg, sub_eq_add_neg, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl and 6 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.par_foldl line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, List, ZMod, OfNat.ofNat, Nat, Eq, List.foldl, Usa2003P6.step, Usa2003P6.step2
Proof uses: List.rec, Eq.refl, List.nil, id, List.cons, Eq.mpr, congrArg, Eq.symm, Usa2003P6.par_step
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.step_nonneg line 118 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, LE.le, Int, Usa2003P6.step
Proof uses: dite, Eq, Eq.mpr, Function.update, abs, HSub.hSub, HAdd.hAdd, id, congrArg, Usa2003P6.step.eq_1, Function.update_self, abs_nonneg, Not, Function.update_of_ne
31 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.foldl_nonneg line 127 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, LE.le, Int, List, List.foldl, Usa2003P6.step
Proof uses: List.rec, id, List.cons, Usa2003P6.step_nonneg
6 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.abs_sub_le_of line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, abs, HSub.hSub
Proof uses: Iff.mpr, And, Neg.neg, abs_le, And.intro
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.cmax_step_le line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, LE.le, Int, Usa2003P6.cmax, Usa2003P6.step
Proof uses: Usa2003P6.cmax_le, dite, Eq, Eq.mpr, Function.update, abs, HSub.hSub, HAdd.hAdd, id, congrArg, Usa2003P6.step.eq_1, Function.update_self, le_trans, Max.max, Usa2003P6.abs_sub_le_of, le_max_left, le_max_right, max_le, Usa2003P6.le_cmax, Not and 1 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.cmax_foldl_le line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, LE.le, Int, List, Usa2003P6.cmax, List.foldl, Usa2003P6.step
Proof uses: List.rec, le_refl, List.nil, id, List.cons, le_trans, Usa2003P6.step_nonneg, Usa2003P6.cmax_step_le
7 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Usa2003P6.cands The candidate move sequences used to reach a configuration with exactly one odd entry line 163 source
Source documentation
The candidate move sequences used to reach a configuration with exactly one odd entry. Which one applies depends on the parity pattern of the starting configuration.

standard axioms: Quot.sound, propext what this means
Statement uses: List, ZMod, OfNat.ofNat, Nat
Proof uses: List.cons, List.nil
19 instances, coercions and auxiliary constants left out.
```
def cands : List (List (ZMod 6)) :=
…
```
lemma Usa2003P6.phase1_decide Machine-checked parity verification: from every parity vector with odd sum, one of the candidate sequences leads to a parity vector with exactly one odd entry line 170 source
Source documentation
Machine-checked parity verification: from every parity vector with odd sum, one of the candidate sequences leads to a parity vector with exactly one odd entry.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Finset.sum, Finset.univ, Exists, List, And, Membership.mem, Usa2003P6.cands, List.foldl, Usa2003P6.step2, ite
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
45 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma phase1_decide : ∀ v : ZMod 6 → ZMod 2, (∑ i, v i) = 1 →
    ∃ l ∈ cands, ∃ p, ∀ i, (l.foldl step2 v) i = (if i = p then 1 else 0) := by
…
```
Mentions: Usa2003P6.cands, Usa2003P6.step2
lemma Usa2003P6.phase1 line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, LE.le, Int, Odd, Finset.sum, Finset.univ, Exists, List, And, Eq, List.foldl, Usa2003P6.step, Usa2003P6.cmax, Ne
Proof uses: Membership.mem, Usa2003P6.cands, Usa2003P6.step2, ite, Usa2003P6.phase1_decide, Eq.mp, congrArg, propext, Usa2003P6.odd_sum_iff, Exists.intro, And.intro, rfl, Usa2003P6.foldl_nonneg, Usa2003P6.cmax_foldl_le, congr_fun, Usa2003P6.par_foldl, Eq.mpr, id, ite_eq_left, ite_eq_right
51 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.step_comp_add line 196 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, Eq, Usa2003P6.step, Function.comp, Int, HAdd.hAdd
Proof uses: funext, id, dite, Function.update, abs, HSub.hSub, Eq.mpr, congrArg, Function.update_self, Lattice, AddGroup, Eq.rec, Eq.refl, HSub, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul and 27 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.foldl_comp_add line 212 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, List, Eq, List.foldl, Usa2003P6.step, Function.comp, Int, HAdd.hAdd, List.map
Proof uses: List.rec, Eq.refl, List.nil, Eq.mpr, List.cons, id, congrArg, congrFun', List.map_cons, Usa2003P6.step_comp_add
14 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.moves_comp_add line 221 source
standard axioms: Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, Usa2003P6.Moves, Function.comp, Int, HAdd.hAdd
Proof uses: List, Eq, List.foldl, Usa2003P6.step, Exists.intro, List.map, HSub.hSub, Eq.mpr, id, congrArg, Usa2003P6.foldl_comp_add, List.map_map, funext, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 25 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.abs_sub_le_mk1 line 234 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, HSub.hSub, abs
Proof uses: Iff.mpr, And, Neg.neg, abs_le, And.intro
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.abs_sub_le_mk2 line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, HSub.hSub, abs
Proof uses: Iff.mpr, And, Neg.neg, abs_le, And.intro
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.phase2 line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, LE.le, Int, Eq, Ne, Exists, And, Usa2003P6.Moves, Or, Odd, Finset.sum, Finset.univ, LT.lt, Usa2003P6.cmax
Proof uses: Usa2003P6.one_le_of_odd, Iff.mpr, Usa2003P6.odd_iff_cast, le_trans, Usa2003P6.le_cmax, Usa2003P6.cmax_attained, ite, funext, dite, Eq.mpr, id, congrArg, ite_eq_left, rfl, Eq.symm, Not, ite_eq_right, HSub.hSub, of_decide_eq_true, Bool and 88 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 266 steps (first 200 of 266)
Open to load the checked before-and-after goal states.
lemma Usa2003P6.winnable_aux line 465 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2003P6.Conf, ZMod, OfNat.ofNat, Nat, LE.le, Int, Odd, Finset.sum, Finset.univ, Usa2003P6.Moves
Proof uses: Eq, Int.toNat, Usa2003P6.cmax, Nat.strongRecOn, LT.lt, List, Exists, And, List.foldl, Usa2003P6.step, Ne, Usa2003P6.phase1, Function.comp, HAdd.hAdd, rfl, id, Eq.mpr, congrArg, zero_add, Iff.mpr and 46 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
def Usa2003P6.stepN One move at vertex j, phrased on natural numbers line 529 source
Source documentation
One move at vertex j, phrased on natural numbers.

standard axioms: Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat
Proof uses: Function.update, Nat.dist, HSub.hSub, HAdd.hAdd
18 instances, coercions and auxiliary constants left out.
```
def stepN (f : ZMod 6 → ℕ) (j : ZMod 6) : ZMod 6 → ℕ :=
…
```
Mentions: f
lemma Usa2003P6.dist_cast line 532 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Nat.dist, abs, HSub.hSub
Proof uses: id, LE.le, Or, HAdd.hAdd, le_total, Eq.mpr, OfNat.ofNat, congrArg, Nat.sub_eq_zero_of_le, zero_add, Nat.cast_sub, Neg.neg, abs_of_nonpos, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring and 26 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.stepN_cast line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Int, Usa2003P6.stepN, Usa2003P6.step
Proof uses: funext, dite, Eq.mpr, Function.update, Nat.dist, HSub.hSub, HAdd.hAdd, id, congrArg, Usa2003P6.stepN.eq_1, Function.update_self, abs, Usa2003P6.Conf, Usa2003P6.step.eq_1, Usa2003P6.dist_cast, Not, Function.update_of_ne, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2003P6.foldl_bridge line 550 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, List, Eq, Int, List.foldl, Usa2003P6.stepN, Usa2003P6.Conf, Usa2003P6.step
Proof uses: List.rec, Eq.refl, List.nil, id, List.cons, Eq.mpr, congrArg, Eq.symm, Usa2003P6.stepN_cast
6 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
problem Usa2003P6.usa2003_p6 line 561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Finset.sum, Finset.univ, HPow.hPow, Exists, List, List.foldl, Function.update, Nat.dist, HSub.hSub, HAdd.hAdd
Proof uses: LE.le, Int, Int.natCast_nonneg, Odd, Eq.mpr, id, congrArg, Eq.symm, Nat.cast_sum, Nat.cast_pow, Odd.pow, Exists.intro, HMul.hMul, rfl, Usa2003P6.Conf, Usa2003P6.step, Usa2003P6.Moves, Usa2003P6.winnable_aux, Usa2003P6.stepN, Usa2003P6.foldl_bridge and 6 more
81 instances, coercions and auxiliary constants left out.

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