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

13 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1985, Problem 3

For any polynomial $P(x) = a_0 + a_1x + \dots + a_kx^k$ with integer coefficients, the number of odd coefficients is denoted by $o(P)$. For $i = 0, 1, 2, \dots$ let $Q_i(x) = (1 + x)^i$. Prove that if $i_1, i_2, \dots, i_n$ are integers satisfying $0 \le i_1 < i_2 < \dots < i_n$, then $$o(Q_{i_1} + Q_{i_2} + \dots + Q_{i_n}) \ge o(Q_{i_1}).$$

Imports (6)

Imported by 1 file

Compfiles.lean

def Imo1985P3.oddCount The number of odd coefficients of a polynomial with integer coefficients line 37 source
Source documentation
The number of odd coefficients of a polynomial with integer coefficients.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Nat
Proof uses: Finset.card, Finset.filter, Odd, Finsupp, Polynomial.coeff, Polynomial.support
7 instances, coercions and auxiliary constants left out.
```
noncomputable def oddCount (P : ℤ[X]) : ℕ :=
…
```
Mentions: P
def Imo1985P3.o o P is the number of nonzero coefficients of a polynomial P over ZMod 2 line 61 source
Source documentation
o P is the number of nonzero coefficients of a polynomial P over ZMod 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, ZMod, OfNat.ofNat, Nat
Proof uses: Finset.card, Polynomial.support
12 instances, coercions and auxiliary constants left out.
```
noncomputable def o (P : (ZMod 2)[X]) : ℕ := P.support.card
```
Mentions: P
lemma Imo1985P3.support_X_pow_mul The support of X ^ m * p is the support of p shifted by m line 64 source
Source documentation
The support of X ^ m * p is the support of p shifted by m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, ZMod, OfNat.ofNat, Eq, Finset, Polynomial.support, HMul.hMul, HPow.hPow, Polynomial.X, Finset.image, HAdd.hAdd
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Not, ite, LE.le, Finsupp, Polynomial.coeff, HSub.hSub, Exists, And, id, congr, congrArg, Eq.trans, Ne, congrFun', Polynomial.coeff_X_pow_mul', funext and 11 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma support_X_pow_mul (m : ℕ) (p : (ZMod 2)[X]) :
    (X ^ m * p).support = p.support.image (· + m) := by
…
```
lemma Imo1985P3.o_add_X_pow_mul If p has degree less than m, the supports of p and X ^ m * q are disjoint, hence o (p + X ^ m * q) = o p + o q line 85 source
Source documentation
If p has degree less than m, the supports of p and X ^ m * q are disjoint, hence o (p + X ^ m * q) = o p + o q.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, ZMod, OfNat.ofNat, LT.lt, Polynomial.natDegree, Eq, Imo1985P3.o, HAdd.hAdd, HMul.hMul, HPow.hPow, Polynomial.X
Proof uses: Finset, Polynomial.support, Union.union, Finset.Subset.antisymm, Polynomial.support_add, Membership.mem, Eq.mpr, Ne, Finsupp, Polynomial.coeff, id, congrArg, propext, Polynomial.mem_support_iff, Or, Iff.mp, Finset.mem_union, lt_of_le_of_lt, Polynomial.le_natDegree_of_mem_supp, Polynomial.coeff_add and 25 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma o_add_X_pow_mul {m : ℕ} {p q : (ZMod 2)[X]} (hp : p.natDegree < m) :
    o (p + X ^ m * q) = o p + o q := by
…
```
Mentions: Imo1985P3.o
lemma Imo1985P3.o_add_le Subadditivity of o line 114 source
Source documentation
Subadditivity of o.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, ZMod, OfNat.ofNat, Nat, LE.le, Imo1985P3.o, HAdd.hAdd
Proof uses: le_trans, Finset.card, Union.union, Finset, Polynomial.support, Finset.card_le_card, Polynomial.support_add, Finset.card_union_le
22 instances, coercions and auxiliary constants left out.
```
lemma o_add_le (p q : (ZMod 2)[X]) : o (p + q) ≤ o p + o q :=
…
```
Mentions: Imo1985P3.o
lemma Imo1985P3.o_le_o_add_add A convenient rearrangement of subadditivity line 118 source
Source documentation
A convenient rearrangement of subadditivity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, ZMod, OfNat.ofNat, Nat, LE.le, Imo1985P3.o, HAdd.hAdd
Proof uses: Eq, Neg.neg, congrArg, Finset, Polynomial.support, Finset.card, Polynomial.support_neg, Trans.trans, Eq.mpr, id, add_neg_cancel_right, Eq.refl, Imo1985P3.o_add_le
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma o_le_o_add_add (p q : (ZMod 2)[X]) : o p ≤ o (p + q) + o q := by
…
```
Mentions: Imo1985P3.o
lemma Imo1985P3.natDegree_one_add_X_pow The degree of (1 + X) ^ i over ZMod 2 line 125 source
Source documentation
The degree of (1 + X) ^ i over ZMod 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Polynomial.natDegree, ZMod, OfNat.ofNat, HPow.hPow, Polynomial, HAdd.hAdd, Polynomial.X
Proof uses: RingHom, Polynomial.C, Eq.mpr, id, congrArg, Polynomial.C_1, add_comm, HMul.hMul, Polynomial.Monic.natDegree_pow, Polynomial.monic_X_add_C, Polynomial.natDegree_X_add_C, mul_one, Eq.refl
51 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma natDegree_one_add_X_pow (i : ℕ) : ((1 + X : (ZMod 2)[X]) ^ i).natDegree = i := by
…
```
lemma Imo1985P3.one_add_X_pow_two_pow The freshman's dream in characteristic $2$: (1 + X) ^ (2 ^ k) = 1 + X ^ (2 ^ k) line 130 source
Source documentation
The freshman's dream in characteristic $2$: (1 + X) ^ (2 ^ k) = 1 + X ^ (2 ^ k).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Polynomial, ZMod, OfNat.ofNat, HPow.hPow, HAdd.hAdd, Polynomial.X
Proof uses: Eq.mpr, id, congrArg, add_pow_expChar_pow, one_pow, Eq.refl
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma one_add_X_pow_two_pow (k : ℕ) :
    (1 + X : (ZMod 2)[X]) ^ 2 ^ k = 1 + X ^ 2 ^ k := by
…
```
lemma Imo1985P3.oddCount_eq_o The number of odd coefficients of P : ℤ[X] equals o of its image in (ZMod 2)[X] line 136 source
Source documentation
The number of odd coefficients of P : ℤ[X] equals o of its image in (ZMod 2)[X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Eq, Nat, Imo1985P3.oddCount, Imo1985P3.o, Polynomial.map, ZMod, OfNat.ofNat, Int.castRingHom
Proof uses: id, Finset.card, Finset.filter, Odd, Finsupp, Polynomial.coeff, Polynomial.support, Finset, Eq.rec, Eq.refl, Finset.ext, Eq.mpr, Iff, Membership.mem, And, Ne, congr, congrArg, Eq.trans, congrFun' and 15 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma oddCount_eq_o (P : ℤ[X]) :
    oddCount P = o (P.map (Int.castRingHom (ZMod 2))) := by
…
```
Mentions: P, Imo1985P3.oddCount, Imo1985P3.o
lemma Imo1985P3.map_one_add_X_pow The image of a single power of 1 + X in (ZMod 2)[X] line 158 source
Source documentation
The image of a single power of 1 + X in (ZMod 2)[X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Polynomial, ZMod, OfNat.ofNat, Polynomial.map, Int, Int.castRingHom, HPow.hPow, HAdd.hAdd, Polynomial.X
Proof uses: Eq.mpr, id, congrArg, Polynomial.map_pow, Polynomial.map_add, Polynomial.map_one, Polynomial.map_X, Eq.refl
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma map_one_add_X_pow (i : ℕ) :
    ((1 + X : ℤ[X]) ^ i).map (Int.castRingHom (ZMod 2)) = (1 + X : (ZMod 2)[X]) ^ i := by
…
```
lemma Imo1985P3.map_sum_one_add_X_pow The image of a sum of powers of 1 + X in (ZMod 2)[X] line 163 source
Source documentation
The image of a sum of powers of 1 + X in (ZMod 2)[X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Eq, Polynomial, ZMod, OfNat.ofNat, Polynomial.map, Int, Int.castRingHom, Finset.sum, HPow.hPow, HAdd.hAdd, Polynomial.X
Proof uses: Eq.mpr, id, congrArg, Polynomial.map_sum, Finset.sum_congr, rfl, Membership.mem, Imo1985P3.map_one_add_X_pow
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma map_sum_one_add_X_pow (S : Finset ℕ) :
    (∑ i ∈ S, (1 + X : ℤ[X]) ^ i).map (Int.castRingHom (ZMod 2)) =
      ∑ i ∈ S, (1 + X : (ZMod 2)[X]) ^ i := by
…
```
Mentions: S
lemma Imo1985P3.key The main inequality over ZMod 2, proved by strong induction on the largest index N line 171 source
Source documentation
The main inequality over ZMod 2, proved by strong induction on the largest index N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Finset.Nonempty, Eq, Finset.max', LE.le, Imo1985P3.o, HPow.hPow, Polynomial, ZMod, OfNat.ofNat, HAdd.hAdd, Polynomial.X, Finset.min', Finset.sum
Proof uses: Nat.strong_induction_on, LT.lt, dite, Singleton.singleton, Iff.mpr, And, Membership.mem, Finset.eq_singleton_iff_nonempty_unique_mem, And.intro, le_trans, Exists.intro, Finset.le_max', le_of_eq, Eq.mpr, id, congrArg, Finset.singleton_nonempty, Finset.min'_singleton, Finset.sum_singleton, le_refl and 53 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 108 steps
Open to load the checked before-and-after goal states.
```
lemma key : ∀ N : ℕ, ∀ (S : Finset ℕ) (hS : S.Nonempty), S.max' hS = N →
    o ((1 + X : (ZMod 2)[X]) ^ S.min' hS) ≤
      o (∑ i ∈ S, (1 + X : (ZMod 2)[X]) ^ i) :=
…
```
Mentions: S, Imo1985P3.o
problem Imo1985P3.imo1985_p3 line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, LE.le, Imo1985P3.oddCount, HPow.hPow, Polynomial, Int, HAdd.hAdd, OfNat.ofNat, Polynomial.X, Finset.min', Finset.sum
Proof uses: Eq.mpr, Imo1985P3.o, Polynomial.map, ZMod, Int.castRingHom, id, Eq, congrArg, Imo1985P3.oddCount_eq_o, Imo1985P3.map_one_add_X_pow, Imo1985P3.map_sum_one_add_X_pow, Imo1985P3.key, Finset.max', rfl
35 instances, coercions and auxiliary constants left out.

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