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

18 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2015, Problem 4

Steve is piling m ≥ 1 indistinguishable stones on the squares of an n × n grid. Each square can have an arbitrarily high pile of stones. After he finished piling his stones in some manner, he can then perform stone moves, defined as follows. Consider any four grid squares, which are corners of a rectangle, i.e. in positions (i, k), (i, l), (j, k), (j, l) for some 1 ≤ i, j, k, l ≤ n, such that i < j and k < l. A stone move consists of either removing one stone from each of (i, k) and (j, l) and moving them to (i, l) and (j, k) respectively, or removing one stone from each of (i, l) and (j, k) and moving them to (i, k) and (j, l) respectively.

Two ways of piling the stones are equivalent if they can be obtained from one another by a sequence of stone moves. How many different non-equivalent ways can Steve pile the stones on the grid?

Imports (4)

Imported by 1 file

Compfiles.lean

determine Usa2015P4.solution line 37 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, Nat.choose, HSub.hSub, HAdd.hAdd, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
abbrev Usa2015P4.Piling A way of piling stones on the n × n grid is a multiset of (row, column) pairs, one pair per stone line 43 source
Source documentation
A way of piling stones on the n × n grid is a multiset of (row, column) pairs, one pair per stone.

no axioms what this means
Statement uses: Nat
Proof uses: Multiset, Prod, Fin
```
abbrev Piling (n : ℕ) := Multiset (Fin n × Fin n)
```
def Usa2015P4.StoneMove A single stone move: two stones lying in distinct rows and distinct columns swap their columns line 49 source
Source documentation
A single stone move: two stones lying in distinct rows and distinct columns swap their columns. (The two kinds of moves described in the problem statement — picking either pair of diagonally opposite corners of a rectangle — are both of this form.)

standard axioms: Quot.sound what this means
Statement uses: Nat, Usa2015P4.Piling
Proof uses: Exists, Fin, And, Ne, Eq, Multiset.cons, Prod, Prod.mk
```
def StoneMove {n : ℕ} (S T : Piling n) : Prop :=
…
```
Mentions: S, Usa2015P4.Piling
inductive Usa2015P4.EquivPilings Two pilings are equivalent if they are related by a sequence of stone moves line 56 source
Source documentation
Two pilings are equivalent if they are related by a sequence of stone moves.

standard axioms: Quot.sound what this means
Statement uses: Nat, Usa2015P4.Piling
```
inductive EquivPilings {n : ℕ} : Piling n → Piling n → Prop where
…
```
Mentions: Usa2015P4.Piling
theorem Usa2015P4.StoneMove.fst The multiset of rows is invariant under a single stone move line 63 source
Source documentation
The multiset of rows is invariant under a single stone move.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2015P4.Piling, Usa2015P4.StoneMove, Eq, Multiset, Fin, Multiset.map, Prod, Prod.fst
Proof uses: Exists, And, Ne, Multiset.cons, Prod.mk, of_eq_true, Eq.trans, True, congr, congrArg, Multiset.map_cons, eq_self, Eq.symm
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem StoneMove.fst {n : ℕ} {S T : Piling n} (h : StoneMove S T) :
    S.map Prod.fst = T.map Prod.fst := by
…
```
Mentions: S, Usa2015P4.Piling, h, Usa2015P4.StoneMove
theorem Usa2015P4.StoneMove.snd The multiset of columns is invariant under a single stone move line 69 source
Source documentation
The multiset of columns is invariant under a single stone move.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2015P4.Piling, Usa2015P4.StoneMove, Eq, Multiset, Fin, Multiset.map, Prod, Prod.snd
Proof uses: Exists, And, Ne, Multiset.cons, Prod.mk, Eq.mpr, id, congrArg, Multiset.map_cons, Multiset.cons_swap, Eq.symm
3 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem StoneMove.snd {n : ℕ} {S T : Piling n} (h : StoneMove S T) :
    S.map Prod.snd = T.map Prod.snd := by
…
```
Mentions: S, Usa2015P4.Piling, h, Usa2015P4.StoneMove
theorem Usa2015P4.StoneMove.cons A stone move can be performed in the presence of an extra fixed stone line 76 source
Source documentation
A stone move can be performed in the presence of an extra fixed stone.

standard axioms: Quot.sound what this means
Statement uses: Nat, Usa2015P4.Piling, Usa2015P4.StoneMove, Prod, Fin, Multiset.cons
Proof uses: Exists, And, Ne, Eq, Prod.mk, Exists.intro, And.intro, Eq.mpr, id, congrArg, Multiset, Multiset.cons_swap, Eq.refl, Eq.symm
3 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem StoneMove.cons {n : ℕ} {S T : Piling n} (h : StoneMove S T) (p : Fin n × Fin n) :
    StoneMove (p ::ₘ S) (p ::ₘ T) := by
…
```
Mentions: S, Usa2015P4.Piling, h, Usa2015P4.StoneMove
theorem Usa2015P4.EquivPilings.fst The multiset of rows is invariant under equivalence of pilings line 84 source
Source documentation
The multiset of rows is invariant under equivalence of pilings.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2015P4.Piling, Usa2015P4.EquivPilings, Eq, Multiset, Fin, Multiset.map, Prod, Prod.fst
Proof uses: Usa2015P4.EquivPilings.rec, Eq.refl, Usa2015P4.StoneMove, Usa2015P4.StoneMove.fst, Eq.symm, Eq.trans

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem EquivPilings.fst {n : ℕ} {S T : Piling n} (h : EquivPilings S T) :
    S.map Prod.fst = T.map Prod.fst := by
…
```
Mentions: S, Usa2015P4.Piling, h, Usa2015P4.EquivPilings
theorem Usa2015P4.EquivPilings.snd The multiset of columns is invariant under equivalence of pilings line 93 source
Source documentation
The multiset of columns is invariant under equivalence of pilings.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2015P4.Piling, Usa2015P4.EquivPilings, Eq, Multiset, Fin, Multiset.map, Prod, Prod.snd
Proof uses: Usa2015P4.EquivPilings.rec, Eq.refl, Usa2015P4.StoneMove, Usa2015P4.StoneMove.snd, Eq.symm, Eq.trans

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem EquivPilings.snd {n : ℕ} {S T : Piling n} (h : EquivPilings S T) :
    S.map Prod.snd = T.map Prod.snd := by
…
```
Mentions: S, Usa2015P4.Piling, h, Usa2015P4.EquivPilings
theorem Usa2015P4.EquivPilings.cons Equivalent pilings remain equivalent after adding an extra fixed stone line 102 source
Source documentation
Equivalent pilings remain equivalent after adding an extra fixed stone.

standard axioms: Quot.sound what this means
Statement uses: Nat, Usa2015P4.Piling, Usa2015P4.EquivPilings, Prod, Fin, Multiset.cons
Proof uses: Usa2015P4.EquivPilings.rec, Usa2015P4.EquivPilings.refl, Usa2015P4.StoneMove, Usa2015P4.EquivPilings.move, Usa2015P4.StoneMove.cons, Usa2015P4.EquivPilings.symm, Usa2015P4.EquivPilings.trans

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem EquivPilings.cons {n : ℕ} {S T : Piling n} (h : EquivPilings S T)
    (p : Fin n × Fin n) : EquivPilings (p ::ₘ S) (p ::ₘ T) := by
…
```
Mentions: S, Usa2015P4.Piling, h, Usa2015P4.EquivPilings
theorem Usa2015P4.equivPilings_of_signature The hard direction: two pilings with the same signature (the same multiset of rows and the same multiset of columns) are equivalent line 115 source
Source documentation
The hard direction: two pilings with the same signature (the same multiset of rows and the same multiset of columns) are equivalent. Proved by strong induction on the number of stones: pick a stone s of the first piling, find a stone t of the second piling in the same row, and use one or two stone moves to put t's column right, then apply the induction hypothesis to the remaining stones.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2015P4.Piling, Eq, Multiset.card, Prod, Fin, Multiset, Multiset.map, Prod.fst, Prod.snd, Usa2015P4.EquivPilings
Proof uses: Nat.strong_induction_on, LT.lt, Multiset.induction_on, OfNat.ofNat, Iff.mp, Multiset.card_eq_zero, Eq.mpr, id, congrArg, Eq.symm, Multiset.card_map, Eq.refl, Usa2015P4.EquivPilings.refl, Multiset.cons, HAdd.hAdd, Multiset.card_cons, Membership.mem, Multiset.mem_map_of_mem, Multiset.mem_cons_self, And and 34 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 148 steps
Open to load the checked before-and-after goal states.
```
theorem equivPilings_of_signature {n : ℕ} :
    ∀ k : ℕ, ∀ S T : Piling n,
      S.card = k → S.map Prod.fst = T.map Prod.fst → S.map Prod.snd = T.map Prod.snd →
      EquivPilings S T := by
…
```
Mentions: S, Usa2015P4.Piling, Usa2015P4.EquivPilings
def Usa2015P4.pilingOf Every signature is realized by at least one piling: sort the rows and the columns and pair them up line 278 source
Source documentation
Every signature is realized by at least one piling: sort the rows and the columns and pair them up.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Multiset, Fin, Usa2015P4.Piling
Proof uses: Prod, List.zip, Multiset.sort, LE.le
6 instances, coercions and auxiliary constants left out.
```
def pilingOf {n : ℕ} (X Y : Multiset (Fin n)) : Piling n :=
…
```
Mentions: Usa2015P4.Piling
theorem Usa2015P4.pilingOf_fst line 281 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Multiset, Fin, Eq, Multiset.card, Multiset.map, Prod, Prod.fst, Usa2015P4.pilingOf
Proof uses: LE.le, List.length, Multiset.sort, Eq.mpr, id, congrArg, Multiset.length_sort, le_refl, List.zip, Usa2015P4.Piling, Usa2015P4.pilingOf.eq_1, List.map, Multiset.map_coe, List, List.map_fst_zip, Multiset.sort_eq, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2015P4.pilingOf_snd line 287 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Multiset, Fin, Eq, Multiset.card, Multiset.map, Prod, Prod.snd, Usa2015P4.pilingOf
Proof uses: LE.le, List.length, Multiset.sort, Eq.mpr, id, congrArg, Multiset.length_sort, le_refl, List.zip, Usa2015P4.Piling, Usa2015P4.pilingOf.eq_1, List.map, Multiset.map_coe, List, List.map_snd_zip, Multiset.sort_eq, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2015P4.pilingOf_card line 293 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Multiset, Fin, Eq, Multiset.card, Prod, Usa2015P4.pilingOf
Proof uses: Eq.mpr, List.zip, Multiset.sort, LE.le, id, congrArg, Usa2015P4.Piling, Usa2015P4.pilingOf.eq_1, List.length, Multiset.coe_card, Min.min, List.length_zip, Multiset.length_sort, min_self, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance Usa2015P4.pilingSetoid The equivalence relation on pilings of m stones, as a Setoid line 299 source
Source documentation
The equivalence relation on pilings of m stones, as a Setoid.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Setoid, Subtype, Usa2015P4.Piling, Eq, Multiset.card, Prod, Fin
Proof uses: Setoid.mk, Usa2015P4.EquivPilings
2 instances, coercions and auxiliary constants left out.
```
instance pilingSetoid (m n : ℕ) : Setoid {S : Piling n // S.card = m} where
…
```
Mentions: S, Usa2015P4.Piling
def Usa2015P4.quotientEquivSignatures The non-equivalent pilings of m stones are in bijection with the pairs (X, Y) of multisets of rows and columns of size m line 309 source
Source documentation
The non-equivalent pilings of m stones are in bijection with the pairs (X, Y) of multisets of rows and columns of size m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Quotient, Subtype, Usa2015P4.Piling, Eq, Multiset.card, Prod, Fin, Sym
Proof uses: Equiv.mk, Quotient.lift, Prod.mk, Subtype.mk, Multiset, Multiset.map, Prod.fst, Prod.snd, Usa2015P4.quotientEquivSignatures.match_1, Quotient.mk, Usa2015P4.pilingOf
9 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
def quotientEquivSignatures (m n : ℕ) :
    Quotient (pilingSetoid m n) ≃ Sym (Fin n) m × Sym (Fin n) m where
…
```
Mentions: Usa2015P4.pilingSetoid
problem Usa2015P4.usa2015_p4 line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Nat.card, Quotient, Subtype, Usa2015P4.Piling, Multiset.card, Prod, Fin, Usa2015P4.solution
Proof uses: Eq.mpr, Sym, id, congrArg, Nat.card_congr, Usa2015P4.quotientEquivSignatures, HMul.hMul, Nat.card_prod, Fintype.card, Nat.card_eq_fintype_card, Nat.choose, HSub.hSub, HAdd.hAdd, Sym.card_sym_eq_choose, Fintype.card_fin, Eq.symm, Nat.choose_symm, HPow.hPow, Nat.pow_two
21 instances, coercions and auxiliary constants left out.

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