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

24 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1988, Problem 5

Let p(x) be the polynomial (1 - x)ᵃ (1 - x²)ᵇ (1 - x³)ᶜ ... (1 - x³²)ᵏ, where a, b, ..., k are integers. When expanded in powers of x, the coefficient of x¹ is -2 and the coefficients of x², x³, ... , x³² are all zero. Find k.

Imports (4)

Imported by 1 file

Compfiles.lean

def Usa1988P5.prodForm The polynomial p(x) = ∏_{i = 1}^{32} (1 - X^i) ^ (a i) line 34 source
Source documentation
The polynomial p(x) = ∏_{i = 1}^{32} (1 - X^i) ^ (a i). The exponent a 32 of the last factor is the k of the problem. (We take the exponents to be natural numbers; the coefficient conditions force every exponent to be positive anyway.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Rat
Proof uses: Finset.prod, Finset.Icc, OfNat.ofNat, HPow.hPow, HSub.hSub, Polynomial.X
19 instances, coercions and auxiliary constants left out.
```
noncomputable def prodForm (a : ℕ → ℕ) : ℚ[X] := ∏ i ∈ Finset.Icc 1 32, (1 - X ^ i) ^ a i
…
```
def Usa1988P5.nextA The effect of one doubling step p(x) ↦ p(x) p(-x) on the exponents: if p = ∏ (1 - X^i) ^ (a i) then p(x) p(-x) = q(x²) where q = ∏ (1 - X^i) ^ (nextA a i) line 41 source
Source documentation
The effect of one doubling step p(x) ↦ p(x) p(-x) on the exponents: if p = ∏ (1 - X^i) ^ (a i) then p(x) p(-x) = q(x²) where q = ∏ (1 - X^i) ^ (nextA a i).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, ite, Odd, OfNat.ofNat, HMul.hMul
7 instances, coercions and auxiliary constants left out.
```
def nextA (a : ℕ → ℕ) (j : ℕ) : ℕ := (if Odd j then a j else 0) + 2 * a (2 * j)
```
def Usa1988P5.Good Good p c m expresses p = 1 + c * X + O(X^(m+1)) line 44 source
Source documentation
Good p c m expresses p = 1 + c * X + O(X^(m+1)).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat
Proof uses: And, Eq, Finsupp, Polynomial.coeff, OfNat.ofNat, LE.le
9 instances, coercions and auxiliary constants left out.
```
def Good (p : ℚ[X]) (c : ℚ) (m : ℕ) : Prop :=
…
```
lemma Usa1988P5.coeff_comp_neg_X line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, Eq, Finsupp, Polynomial.coeff, Polynomial.comp, Neg.neg, Polynomial.X, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: Polynomial.induction_on', Eq.mpr, HAdd.hAdd, id, congrArg, Polynomial.add_comp, Polynomial.coeff_add, mul_add, Eq.refl, LinearMap, RingHom.id, Polynomial.monomial, RingHom, Polynomial.C, Eq.symm, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.mul_comp, Polynomial.C_comp, Polynomial.pow_comp, Polynomial.X_comp and 24 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_comp_X_sq line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, Eq, Finsupp, Polynomial.coeff, Polynomial.comp, HPow.hPow, Polynomial.X, OfNat.ofNat, HMul.hMul
Proof uses: Polynomial.induction_on', Eq.mpr, HAdd.hAdd, id, congrArg, Polynomial.add_comp, Polynomial.coeff_add, Eq.refl, LinearMap, RingHom.id, Polynomial.monomial, RingHom, Polynomial.C, Eq.symm, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.mul_comp, Polynomial.C_comp, Polynomial.pow_comp, Polynomial.X_comp, pow_mul and 7 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_one_sub_pow Binomial expansion of the coefficients of (1 - X^n)^a line 77 source
Source documentation
Binomial expansion of the coefficients of (1 - X^n)^a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HSub.hSub, OfNat.ofNat, Polynomial.X, Finset.sum, Finset.range, HAdd.hAdd, ite, HMul.hMul, Neg.neg, Nat.choose
Proof uses: Eq.mpr, id, congrArg, sub_eq_add_neg, add_comm, add_pow, Polynomial.finsetSum_coeff, Finset.sum_congr, rfl, Finset, Membership.mem, RingHom, Polynomial.C, of_eq_true, Eq.trans, True, neg_mul, one_mul, eq_self, mul_pow and 20 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma coeff_one_sub_pow (n a k : ℕ) :
    ((1 - X ^ n) ^ a : ℚ[X]).coeff k =
      ∑ j ∈ Finset.range (a + 1),
        if j * n = k then (-1 : ℚ) ^ j * (a.choose j : ℚ) else 0 := by
…
```
lemma Usa1988P5.coeff_zero_factor line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HSub.hSub, Polynomial.X
Proof uses: Eq.mpr, Polynomial.eval, id, congrArg, Polynomial.coeff_zero_eq_eval_zero, Polynomial.eval_pow, Polynomial.eval_sub, Polynomial.eval_one, Polynomial.eval_X, zero_pow, of_eq_true, Eq.trans, True, congrFun', sub_zero, one_pow, eq_self
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_one_factor line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HSub.hSub, Polynomial.X
Proof uses: Eq.mpr, Finset.sum, Finset.range, HAdd.hAdd, ite, HMul.hMul, Neg.neg, Nat.choose, id, congrArg, Usa1988P5.coeff_one_sub_pow, Finset.sum_eq_zero, Membership.mem, Finset, dite, False.elim, GT.gt, Or, False, Nat.eq_zero_or_pos and 10 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_two_factor line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HSub.hSub, Polynomial.X
Proof uses: Eq.mpr, Finset.sum, Finset.range, HAdd.hAdd, ite, HMul.hMul, Neg.neg, Nat.choose, id, congrArg, Usa1988P5.coeff_one_sub_pow, Finset.sum_eq_zero, Membership.mem, Finset, dite, False.elim, GT.gt, Or, False, Nat.eq_zero_or_pos and 10 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_zero_one_sub_X line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HSub.hSub, OfNat.ofNat, Polynomial.X
Proof uses: Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, pow_one, eq_self, Usa1988P5.coeff_zero_factor, le_refl
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_one_one_sub_X line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HSub.hSub, OfNat.ofNat, Polynomial.X, Neg.neg
Proof uses: Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, pow_one, eq_self, Finset.sum, Finset.range, HAdd.hAdd, ite, HMul.hMul, Nat.choose, Usa1988P5.coeff_one_sub_pow, GT.gt, Or, Nat.eq_zero_or_pos, congr, Membership.mem and 26 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_two_one_sub_X line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HSub.hSub, OfNat.ofNat, Polynomial.X, Nat.choose
Proof uses: Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, pow_one, eq_self, Finset.sum, Finset.range, HAdd.hAdd, ite, HMul.hMul, Neg.neg, Usa1988P5.coeff_one_sub_pow, dite, LE.le, Finset.sum_eq_single, Membership.mem, Finset and 17 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_two_one_sub_X_sq line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Finsupp, Polynomial.coeff, HPow.hPow, Polynomial, HSub.hSub, OfNat.ofNat, Polynomial.X, Neg.neg
Proof uses: Eq.mpr, Finset.sum, Finset.range, HAdd.hAdd, ite, HMul.hMul, Nat.choose, id, congrArg, Usa1988P5.coeff_one_sub_pow, GT.gt, Or, Nat.eq_zero_or_pos, of_eq_true, Eq.trans, True, congr, Membership.mem, Finset, Singleton.singleton and 25 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_mul_two line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Eq, Finsupp, Nat, Polynomial.coeff, HMul.hMul, OfNat.ofNat, HAdd.hAdd
Proof uses: Eq.mpr, Finset.sum, Prod, Finset.HasAntidiagonal.antidiagonal, Prod.fst, Prod.snd, id, congrArg, Polynomial.coeff_mul, Finset, Insert.insert, Prod.mk, Singleton.singleton, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Finset.sum_insert, Not and 3 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_zero_prod line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Polynomial, Rat, Membership.mem, Eq, Finsupp, Polynomial.coeff, OfNat.ofNat, Finset.prod
Proof uses: Eq.mpr, Polynomial.eval, id, congrArg, Polynomial.coeff_zero_eq_eval_zero, Polynomial.eval_prod, Finset.prod_eq_one, Eq.symm
34 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_one_prod line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Polynomial, Rat, Membership.mem, Eq, Finsupp, Polynomial.coeff, OfNat.ofNat, Finset.prod
Proof uses: Finset.induction, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congrFun', congrArg, ite, Polynomial.coeff_one, ite_eq_right_of_eq_false, eq_self, Not, Insert.insert, Finset.mem_insert_of_mem, Eq.mpr, HMul.hMul, id, Finset.prod_insert, HAdd.hAdd, Polynomial.mul_coeff_one and 6 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.coeff_two_prod line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Polynomial, Rat, Membership.mem, Eq, Finsupp, Polynomial.coeff, OfNat.ofNat, Finset.prod
Proof uses: Finset.induction, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congrFun', congrArg, ite, Polynomial.coeff_one, ite_eq_right_of_eq_false, eq_self, Not, Insert.insert, Finset.mem_insert_of_mem, Eq.mpr, HMul.hMul, id, Finset.prod_insert, HAdd.hAdd, Usa1988P5.coeff_mul_two and 7 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.nextA_support line 233 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Usa1988P5.nextA
Proof uses: HMul.hMul, of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, ite, Odd, congr, ite_congr, Eq.refl, Not, ite_self, MulZeroClass.mul_zero, add_zero, eq_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.nextA_even line 239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, Odd, Eq, Usa1988P5.nextA, HMul.hMul, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, ite, ite_eq_right_of_eq_false, eq_false, zero_add, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1988P5.prod_double The doubling step, at the level of the product representation: (∏ (1 - X^i)^(a i)) · (∏ (1 - X^i)^(a i)).comp (-X) equals (∏ (1 - X^i)^(nextA a i)).comp (X^2) line 246 source
Source documentation
The doubling step, at the level of the product representation: (∏ (1 - X^i)^(a i)) · (∏ (1 - X^i)^(a i)).comp (-X) equals (∏ (1 - X^i)^(nextA a i)).comp (X^2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Polynomial, Rat, HMul.hMul, Usa1988P5.prodForm, Polynomial.comp, Neg.neg, Polynomial.X, Usa1988P5.nextA, HPow.hPow
Proof uses: Finset.prod, Finset.Icc, HSub.hSub, Eq.mpr, id, congrArg, Usa1988P5.prodForm.eq_1, Polynomial.prod_comp, Eq.symm, Finset.prod_mul_distrib, Finset.prod_congr, rfl, Finset, Membership.mem, Polynomial.pow_comp, Polynomial.sub_comp, Polynomial.one_comp, Polynomial.X_comp, mul_pow, Eq.refl and 90 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
lemma prod_double {a : ℕ → ℕ} (ha : ∀ i, 32 < i → a i = 0) :
    prodForm a * (prodForm a).comp (-X) = (prodForm (nextA a)).comp (X ^ 2) := by
…
```
Mentions: Usa1988P5.prodForm, Usa1988P5.nextA
lemma Usa1988P5.good_transport The doubling step preserves the 1 + c * X + O(X^(m+1)) shape, squaring the linear coefficient and halving the range of vanishing line 339 source
Source documentation
The doubling step preserves the 1 + c * X + O(X^(m+1)) shape, squaring the linear coefficient and halving the range of vanishing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Rat, Nat, LE.le, OfNat.ofNat, Usa1988P5.Good, Eq, HMul.hMul, Polynomial.comp, Neg.neg, Polynomial.X, HPow.hPow, HDiv.hDiv
Proof uses: Finsupp, Polynomial.coeff, And, Usa1988P5.coeff_comp_neg_X, And.intro, Usa1988P5.coeff_comp_X_sq, Eq.mpr, id, congrArg, Eq.symm, Eq.mp, MulZeroClass.mul_zero, Polynomial.mul_coeff_zero, of_eq_true, Eq.trans, True, congrFun', pow_zero, mul_one, eq_self and 79 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma good_transport {p q : ℚ[X]} {c : ℚ} {m : ℕ} (hm : 2 ≤ m)
    (hp : Good p c m) (h : p * p.comp (-X) = q.comp (X ^ 2)) :
    Good q (-c ^ 2) (m / 2) := by
…
```
Mentions: Usa1988P5.Good, h
lemma Usa1988P5.extract Reading off the two lowest coefficients of a product ∏ (1 - X^i)^(b i): the exponent of 1 - X is 65536 and the exponent of 1 - X^2 is its binomial coefficient line 378 source
Source documentation
Reading off the two lowest coefficients of a product ∏ (1 - X^i)^(b i): the exponent of 1 - X is 65536 and the exponent of 1 - X^2 is its binomial coefficient.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Finsupp, Polynomial.coeff, Usa1988P5.prodForm, OfNat.ofNat, Neg.neg, And, Nat.choose
Proof uses: Membership.mem, Finset, Finset.Icc, Eq.mpr, LE.le, id, congrArg, propext, Finset.mem_Icc, Polynomial, Finset.prod, Finset.erase, HPow.hPow, HSub.hSub, Polynomial.X, rfl, Usa1988P5.coeff_zero_prod, Usa1988P5.coeff_zero_factor, Eq.mp, Ne and 72 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 84 steps
Open to load the checked before-and-after goal states.
```
lemma extract {b : ℕ → ℕ} (h1 : (prodForm b).coeff 1 = -65536)
    (h2 : (prodForm b).coeff 2 = 0) :
    b 1 = 65536 ∧ b 2 = (65536).choose 2 := by
…
```
Mentions: Usa1988P5.prodForm
determine Usa1988P5.answer line 463 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HSub.hSub, HPow.hPow, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
problem Usa1988P5.usa1988_p5 line 465 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Finsupp, Polynomial.coeff, Usa1988P5.prodForm, OfNat.ofNat, Neg.neg, LE.le, Usa1988P5.answer
Proof uses: ite, Membership.mem, Finset, Finset.Icc, Polynomial, Finset.prod_congr, HPow.hPow, HSub.hSub, Polynomial.X, rfl, Eq.mpr, id, congrArg, ite_eq_left, Eq.refl, LT.lt, Not, And, propext, Finset.mem_Icc and 40 more
69 instances, coercions and auxiliary constants left out.

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