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

8 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2016, Problem 2

Prove that for any positive integer k,

(k²)! · ∏_{j=0}^{k-1} j!/(j + k)!

is an integer.

Imports (5)

Imported by 1 file

Compfiles.lean

lemma Usa2016P2.period_mul If F is periodic with period q, then it is also periodic with period a * q line 37 source
Source documentation
If F is periodic with period q, then it is also periodic with period a * q.

standard axioms: propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, MulZeroClass.zero_mul, 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 16 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma period_mul {q : ℕ} {F : ℕ → ℕ} (hF : ∀ j, F (j + q) = F j) (a j : ℕ) :
    F (j + a * q) = F j := by
…
```
lemma Usa2016P2.sum_range_period_mul The sum of a q-periodic function over range (a * q) splits into a copies of the full-period sum line 47 source
Source documentation
The sum of a q-periodic function over range (a * q) splits into a copies of the full-period sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Finset.sum, Finset.range, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congr, congrArg, congrFun', EmptyCollection.emptyCollection, Finset, MulZeroClass.zero_mul, eq_self, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 23 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_period_mul {q : ℕ} {F : ℕ → ℕ} (hF : ∀ j, F (j + q) = F j) (a : ℕ) :
    ∑ j ∈ Finset.range (a * q), F j = a * ∑ i ∈ Finset.range q, F i := by
…
```
lemma Usa2016P2.sum_range_period The sum of a q-periodic function over range (a * q + b) splits into full periods plus a remainder sum line 67 source
Source documentation
The sum of a q-periodic function over range (a * q + b) splits into full periods plus a remainder sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Finset.sum, Finset.range, HMul.hMul
Proof uses: Finset.sum_range_add, Eq.mpr, id, congrArg, Usa2016P2.sum_range_period_mul, Finset.sum_congr, rfl, Finset, Membership.mem, add_comm, Usa2016P2.period_mul, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_period {q : ℕ} {F : ℕ → ℕ} (hF : ∀ j, F (j + q) = F j) (a b : ℕ) :
    ∑ j ∈ Finset.range (a * q + b), F j =
      a * (∑ i ∈ Finset.range q, F i) + ∑ i ∈ Finset.range b, F i := by
…
```
lemma Usa2016P2.sum_range_period_shift The sum of a q-periodic function over one full period is shift invariant line 81 source
Source documentation
The sum of a q-periodic function over one full period is shift invariant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Finset.sum, Finset.range
Proof uses: OfNat.ofNat, Finset.sum_range_succ', Finset.sum_range_succ, Eq.mp, congrFun', congrArg, zero_add, Nat.recAux, of_eq_true, Eq.trans, True, Finset.sum_congr, Eq.refl, Finset, Membership.mem, add_zero, eq_self, Eq.mpr, id, Nat.add_right_comm and 2 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_period_shift {q : ℕ} {F : ℕ → ℕ} (hF : ∀ j, F (j + q) = F j) (b : ℕ) :
    ∑ i ∈ Finset.range q, F (i + b) = ∑ i ∈ Finset.range q, F i := by
…
```
lemma Usa2016P2.sum_range_mod_add_ge For b ≤ q and m ≤ q, the sum of i over range b is at most the sum of (i + m) % q line 107 source
Source documentation
For b ≤ q and m ≤ q, the sum of i over range b is at most the sum of (i + m) % q.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Finset.sum, Finset.range, HMod.hMod, HAdd.hAdd
Proof uses: LT.lt, Eq, Int, HSub.hSub, HMul.hMul, ite, OfNat.ofNat, dite, Eq.mpr, id, congrArg, ite_eq_left, Nat.mod_eq_sub_mod, Nat.mod_eq_of_lt, Nat.cast_sub, Nat.cast_add, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Int.rawCast and 94 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_mod_add_ge {q b m : ℕ} (hb : b ≤ q) (hm : m ≤ q) :
    ∑ i ∈ Finset.range b, i ≤ ∑ i ∈ Finset.range b, (i + m) % q := by
…
```
lemma Usa2016P2.sum_mod_le_sum_add_mod The sum of the remainders of 0, 1, …, k-1 modulo q is at most the sum of the remainders of n, n+1, …, n+k-1 modulo q line 169 source
Source documentation
The sum of the remainders of 0, 1, …, k-1 modulo q is at most the sum of the remainders of n, n+1, …, n+k-1 modulo q.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Finset.sum, Finset.range, HMod.hMod, HAdd.hAdd
Proof uses: Eq, HMul.hMul, HDiv.hDiv, Eq.symm, Nat.div_add_mod', Nat.add_mod_right, Eq.mpr, id, congrArg, Nat.add_right_comm, Eq.refl, Finset.sum_congr, rfl, Finset, Membership.mem, Nat.mod_eq_of_lt, Eq.mp, propext, Finset.mem_range, Usa2016P2.sum_range_period_shift and 10 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma sum_mod_le_sum_add_mod (k n q : ℕ) (hq : 0 < q) :
    ∑ j ∈ Finset.range k, j % q ≤ ∑ j ∈ Finset.range k, (j + n) % q := by
…
```
lemma Usa2016P2.sum_add_div_le For each q > 0, ∑ j ∈ range k, (j + k) / q ≤ k ^ 2 / q + ∑ j ∈ range k, j / q line 215 source
Source documentation
For each q > 0, ∑ j ∈ range k, (j + k) / q ≤ k ^ 2 / q + ∑ j ∈ range k, j / q. This is the per-prime-power comparison in Legendre's formula for the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Finset.sum, Finset.range, HDiv.hDiv, HAdd.hAdd, HPow.hPow
Proof uses: Eq, Int, HMul.hMul, HSub.hSub, HMod.hMod, cast, Eq.symm, Nat.div_add_mod, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat and 91 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma sum_add_div_le (k q : ℕ) (hq : 0 < q) :
    ∑ j ∈ Finset.range k, (j + k) / q ≤ k ^ 2 / q + ∑ j ∈ Finset.range k, j / q := by
…
```
problem Usa2016P2.usa2016_p2 line 281 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, Finset.prod, Finset.range, Nat.factorial, HAdd.hAdd, HMul.hMul, HPow.hPow
Proof uses: Ne, Nat.factorial_ne_zero, Iff.mpr, Membership.mem, Finset, Finset.prod_ne_zero_iff, Eq.mpr, LE.le, Finsupp, Nat.factorization, id, Eq, congrArg, Eq.symm, propext, Nat.factorization_le_iff_dvd, mul_ne_zero, Finsupp.le_def, dite, Nat.Prime and 105 more
140 instances, coercions and auxiliary constants left out.

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