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

20 declarations, 0 contain sorry, 0 declared as axioms

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

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Usa2024P4.Necklace A circular necklace with m * n beads, each red (true) or blue (false) line 32 source
Source documentation
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).

no axioms what this means
Statement uses: Nat
Proof uses: ZMod, HMul.hMul, Bool
2 instances, coercions and auxiliary constants left out.
```
abbrev Necklace (m n : ℕ) := ZMod (m * n) → Bool
```
def Usa2024P4.blockCount The number of red beads in the block of n consecutive beads starting at position s + i * n (positions are taken modulo m * n) line 36 source
Source documentation
The number of red beads in the block of n consecutive beads starting at position s + i * n (positions are taken modulo m * n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P4.Necklace, ZMod, HMul.hMul
Proof uses: Finset.sum, Finset.range, ite, Eq, Bool, HAdd.hAdd, Bool.true, OfNat.ofNat
19 instances, coercions and auxiliary constants left out.
```
def blockCount {m n : ℕ} (c : Necklace m n) (s : ZMod (m * n)) (i : ℕ) : ℕ :=
…
```
Mentions: Usa2024P4.Necklace
def Usa2024P4.AllCutsDistinct Documented declaration: AllCutsDistinct line 43 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P4.Necklace
Proof uses: ZMod, HMul.hMul, Function.Injective, Fin, Usa2024P4.blockCount
3 instances, coercions and auxiliary constants left out.
```
def AllCutsDistinct {m n : ℕ} (c : Necklace m n) : Prop :=
…
```
Mentions: Usa2024P4.Necklace
lemma Usa2024P4.blockCount_le Each block contains n beads, so its red bead count is at most n line 49 source
Source documentation
Each block contains n beads, so its red bead count is at most n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P4.Necklace, ZMod, HMul.hMul, LE.le, Usa2024P4.blockCount
Proof uses: id, Trans.trans, Eq, Finset.sum, Finset.range, ite, Bool, HAdd.hAdd, Bool.true, OfNat.ofNat, Finset.sum_le_sum, Membership.mem, Finset, Decidable, Not, Eq.mpr, congrFun', congrArg, ite_eq_right, of_eq_true and 9 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma blockCount_le {m n : ℕ} (c : Necklace m n) (s : ZMod (m * n)) (i : ℕ) :
    blockCount c s i ≤ n := by
…
```
Mentions: Usa2024P4.Necklace, Usa2024P4.blockCount
lemma Usa2024P4.le_of_allCutsDistinct Necessity: the m distinct block counts all lie in {0, 1, ..., n}, which has only n + 1 elements line 61 source
Source documentation
Necessity: the m distinct block counts all lie in {0, 1, ..., n}, which has only n + 1 elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P4.Necklace, Usa2024P4.AllCutsDistinct, LE.le, HAdd.hAdd, OfNat.ofNat
Proof uses: Function.Injective, Fin, Usa2024P4.blockCount, ZMod, HMul.hMul, Finset, Finset.image, Finset.univ, Finset.range, Membership.mem, And, Eq, Exists, Eq.mp, congrArg, propext, Finset.mem_image, Eq.mpr, LT.lt, id and 10 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma le_of_allCutsDistinct {m n : ℕ} {c : Necklace m n} (hc : AllCutsDistinct c) :
    m ≤ n + 1 := by
…
```
Mentions: Usa2024P4.Necklace, Usa2024P4.AllCutsDistinct
def Usa2024P4.rowRed Documented declaration: rowRed line 79 source
Source documentation
The red indicator of the unfolded construction: writing p = q * n + j with j < n (so q is the row and j the column of bead p), the bead is red iff n + 1 - m ≤ j < n - q.

no axioms what this means
Statement uses: Nat
Proof uses: ite, And, LE.le, HSub.hSub, HAdd.hAdd, OfNat.ofNat, HMod.hMod, LT.lt, HDiv.hDiv
14 instances, coercions and auxiliary constants left out.
```
def rowRed (m n : ℕ) (p : ℕ) : ℕ :=
…
```
lemma Usa2024P4.rowRed_eq Evaluating rowRed on the bead t * n + a in row t, column a line 83 source
Source documentation
Evaluating rowRed on the bead t * n + a in row t, column a.

standard axioms: propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Usa2024P4.rowRed, HAdd.hAdd, HMul.hMul, ite, And, LE.le, HSub.hSub
Proof uses: id, HMod.hMod, Nat.mul_add_mod_of_lt, HDiv.hDiv, Eq.mpr, congrArg, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 11 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma rowRed_eq {m n : ℕ} (hn : 0 < n) (t a : ℕ) (ha : a < n) :
    rowRed m n (t * n + a) = if n + 1 - m ≤ a ∧ a + t < n then 1 else 0 := by
…
```
Mentions: Usa2024P4.rowRed
lemma Usa2024P4.rowRed_self Evaluating rowRed on a bead in row 0 line 93 source
Source documentation
Evaluating rowRed on a bead in row 0.

standard axioms: propext what this means
Statement uses: Nat, LT.lt, Eq, Usa2024P4.rowRed, ite, LE.le, HSub.hSub, HAdd.hAdd, OfNat.ofNat
Proof uses: id, Eq.mpr, And, HMod.hMod, HDiv.hDiv, congrArg, Nat.mod_eq_of_lt, Nat.div_eq_of_lt, of_eq_true, Eq.trans, True, congrFun', ite_congr, eq_true, and_true, Eq.refl, Not, eq_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma rowRed_self {m n j : ℕ} (hj : j < n) :
    rowRed m n j = if n + 1 - m ≤ j then 1 else 0 := by
…
```
Mentions: Usa2024P4.rowRed
def Usa2024P4.constr The necklace constructed for the m ≤ n + 1 direction: writing p = q * n + j with j < n, bead p is red iff n + 1 - m ≤ j < n - q line 101 source
Source documentation
The necklace constructed for the m ≤ n + 1 direction: writing p = q * n + j with j < n, bead p is red iff n + 1 - m ≤ j < n - q.

no axioms what this means
Statement uses: Nat, Usa2024P4.Necklace
Proof uses: ZMod, HMul.hMul, Decidable.decide, And, LE.le, HSub.hSub, HAdd.hAdd, OfNat.ofNat, HMod.hMod, ZMod.val, LT.lt, HDiv.hDiv
16 instances, coercions and auxiliary constants left out.
```
def constr (m n : ℕ) : Necklace m n :=
…
```
Mentions: Usa2024P4.Necklace
lemma Usa2024P4.blockCount_constr_eq Documented declaration: blockCount_constr_eq line 107 source
Source documentation
Bridging lemma: the block count of the constructed necklace can be computed with natural number arithmetic; the modulo m * n on the indices keeps track of the wrap-around of the circle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2024P4.blockCount, Usa2024P4.constr, ZMod, HMul.hMul, Finset.sum, Finset.range, Usa2024P4.rowRed, HMod.hMod, HAdd.hAdd
Proof uses: id, Finset.sum_congr, ite, Bool, Bool.true, OfNat.ofNat, rfl, Finset, Membership.mem, Eq.mpr, congrArg, congr, Eq.trans, Nat.cast_add, congrFun', Nat.cast_mul, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr and 31 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma blockCount_constr_eq {m n : ℕ} (s' t : ℕ) :
    blockCount (constr m n) ((s' : ℕ) : ZMod (m * n)) t =
      ∑ j ∈ Finset.range n, rowRed m n ((s' + t * n + j) % (m * n)) := by
…
```
Mentions: Usa2024P4.blockCount, Usa2024P4.constr, Usa2024P4.rowRed
lemma Usa2024P4.sum_rowRed Documented declaration: sum_rowRed line 120 source
Source documentation
The key counting lemma: for a cut starting at s' < n, the number of red beads in block t (interpreted without wrap-around) is m - 1 - t if s' + t < n and m - 2 - t otherwise.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, Eq, Finset.sum, Finset.range, Usa2024P4.rowRed, HMul.hMul, ite, HSub.hSub
Proof uses: Finset.sum_range_add, Eq.mpr, id, congrArg, Eq.mp, Nat.sub_add_cancel, Nat.le_of_lt, Max.max, And, Finset.sum_congr, rfl, Finset, Membership.mem, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl and 35 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma sum_rowRed {m n : ℕ} (hn : 0 < n) (hmn : m ≤ n + 1) {s' t : ℕ}
    (hs : s' < n) :
    (∑ j ∈ Finset.range n, rowRed m n (s' + t * n + j)) =
      if s' + t < n then m - 1 - t else m - 2 - t := by
…
```
Mentions: Usa2024P4.rowRed
lemma Usa2024P4.sum_rowRed_last Documented declaration: sum_rowRed_last line 172 source
Source documentation
The last block (which wraps around the end of the necklace) contains exactly s' - (n + 1 - m) red beads: its first n - s' beads lie in row m - 1 (which is entirely blue) and its last s' beads lie in row 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, Eq, Finset.sum, Finset.range, Usa2024P4.rowRed, HMod.hMod, HMul.hMul, HSub.hSub
Proof uses: Exists, Exists.intro, Eq.mpr, id, congrArg, Nat.add_sub_cancel, Nat.succ, Nat.succ_mul, Eq.refl, Eq.symm, Finset.sum_range_add, Eq.mp, Nat.sub_add_cancel, Nat.le_of_lt, Finset.sum_eq_zero, Membership.mem, Finset, propext, Finset.mem_range, add_lt_add_left and 42 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma sum_rowRed_last {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (hmn : m ≤ n + 1) {s' : ℕ}
    (hs : s' < n) :
    (∑ j ∈ Finset.range n, rowRed m n ((s' + (m - 1) * n + j) % (m * n))) =
      s' - (n + 1 - m) := by
…
```
Mentions: Usa2024P4.rowRed
lemma Usa2024P4.blockCount_constr The complete formula for the block counts of the constructed necklace when the cut starts at s' < n line 223 source
Source documentation
The complete formula for the block counts of the constructed necklace when the cut starts at s' < n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, Eq, Usa2024P4.blockCount, Usa2024P4.constr, ZMod, HMul.hMul, ite, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.range, Usa2024P4.rowRed, HMod.hMod, id, congrArg, Usa2024P4.blockCount_constr_eq, dite, ite_eq_left, rfl, Usa2024P4.sum_rowRed_last, Eq.symm, Not, ite_eq_right, Membership.mem, Finset, mul_le_mul_of_nonneg_right, Nat.zero_le, Trans.trans and 8 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma blockCount_constr {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (hmn : m ≤ n + 1) {s' t : ℕ}
    (hs : s' < n) (ht : t < m) :
    blockCount (constr m n) ((s' : ℕ) : ZMod (m * n)) t =
      if t = m - 1 then s' - (n + 1 - m)
      else if s' + t < n then m - 1 - t else m - 2 - t := by
…
```
Mentions: Usa2024P4.blockCount, Usa2024P4.constr
lemma Usa2024P4.blockCount_add_period The block count is periodic in the block index with period m line 252 source
Source documentation
The block count is periodic in the block index with period m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P4.Necklace, ZMod, HMul.hMul, Eq, Usa2024P4.blockCount, HAdd.hAdd
Proof uses: id, Finset.sum_congr, Finset.range, ite, Bool, Bool.true, OfNat.ofNat, rfl, Finset, Membership.mem, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.mpr, congrArg, Eq.symm, Eq.refl and 16 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma blockCount_add_period {m n : ℕ} (c : Necklace m n) (s : ZMod (m * n)) (i : ℕ) :
    blockCount c s (i + m) = blockCount c s i := by
…
```
Mentions: Usa2024P4.Necklace, Usa2024P4.blockCount
lemma Usa2024P4.blockCount_add_mul Iterated version of blockCount_add_period line 263 source
Source documentation
Iterated version of blockCount_add_period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P4.Necklace, ZMod, HMul.hMul, Eq, Usa2024P4.blockCount, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, MulZeroClass.mul_zero, add_zero, eq_self, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm, Eq.refl and 17 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma blockCount_add_mul {m n : ℕ} (c : Necklace m n) (s : ZMod (m * n)) (i q : ℕ) :
    blockCount c s (i + m * q) = blockCount c s i := by
…
```
Mentions: Usa2024P4.Necklace, Usa2024P4.blockCount
lemma Usa2024P4.blockCount_mod The block count only depends on the block index modulo m line 272 source
Source documentation
The block count only depends on the block index modulo m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2024P4.Necklace, ZMod, HMul.hMul, Eq, Usa2024P4.blockCount, HMod.hMod
Proof uses: Eq.mpr, HAdd.hAdd, HDiv.hDiv, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Nat.mod_add_div, Usa2024P4.blockCount_add_mul
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma blockCount_mod {m n : ℕ} (c : Necklace m n) (s : ZMod (m * n)) (x : ℕ) :
    blockCount c s x = blockCount c s (x % m) := by
…
```
Mentions: Usa2024P4.Necklace, Usa2024P4.blockCount
lemma Usa2024P4.blockCount_shift Shifting the starting position of the cut by n beads shifts the blocks by one line 279 source
Source documentation
Shifting the starting position of the cut by n beads shifts the blocks by one. This reduces a general cut s to a cut starting at s.val % n < n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero, HMul.hMul, Usa2024P4.Necklace, ZMod, Eq, Usa2024P4.blockCount, HMod.hMod, ZMod.val, HAdd.hAdd, HDiv.hDiv
Proof uses: id, Finset.sum_congr, Finset.range, ite, Bool, Bool.true, OfNat.ofNat, rfl, Finset, Membership.mem, Eq.mpr, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, ZMod.natCast_zmod_val, Nat.cast_add, NatCast, Nat.mod_add_div and 18 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma blockCount_shift {m n : ℕ} [NeZero (m * n)] (c : Necklace m n)
    (s : ZMod (m * n)) (i : ℕ) :
    blockCount c s i =
      blockCount c ((s.val % n : ℕ) : ZMod (m * n)) (s.val / n + i) := by
…
```
Mentions: Usa2024P4.Necklace, Usa2024P4.blockCount
lemma Usa2024P4.allCutsDistinct_constr The constructed necklace satisfies the property of the problem line 296 source
Source documentation
The constructed necklace satisfies the property of the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, Usa2024P4.AllCutsDistinct, Usa2024P4.constr
Proof uses: NeZero, HMul.hMul, NeZero.mk, LT.lt.ne', Nat.mul_pos, ZMod, Fin, Eq, Usa2024P4.blockCount, HMod.hMod, ZMod.val, Nat.mod_lt, HDiv.hDiv, dite, HSub.hSub, Decidable.byContradiction, Not, Eq.mp, ite, congrArg and 16 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma allCutsDistinct_constr {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (hmn : m ≤ n + 1) :
    AllCutsDistinct (constr m n) := by
…
```
Mentions: Usa2024P4.AllCutsDistinct, Usa2024P4.constr
determine Usa2024P4.solution The answer: the required necklaces exist exactly for the pairs (m, n) with m ≤ n + 1 line 325 source
Source documentation
The answer: the required necklaces exist exactly for the pairs (m, n) with m ≤ n + 1.

no axioms what this means
Statement uses: Nat
Proof uses: LE.le, HAdd.hAdd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
determine solution : ℕ → ℕ → Prop := fun m n ↦ m ≤ n + 1
```
problem Usa2024P4.usa2024_p4 line 327 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Exists, Usa2024P4.Necklace, Usa2024P4.AllCutsDistinct, Usa2024P4.solution
Proof uses: Iff.intro, Usa2024P4.le_of_allCutsDistinct, Exists.intro, Usa2024P4.constr, Usa2024P4.allCutsDistinct_constr
5 instances, coercions and auxiliary constants left out.

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