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

9 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2025, Problem 2

Let n > k ≥ 1 be integers. Let P(x) ∈ ℝ[x] be a polynomial of degree n with no repeated roots and P(0) ≠ 0. Suppose that for any real numbers a₀, a₁, ..., aₖ such that the polynomial aₖxᵏ + ··· + a₁x + a₀ divides P(x), the product a₀a₁···aₖ is zero. Prove that P(x) has a nonreal root.

Imports (6)

Imported by 1 file

Compfiles.lean

lemma Usa2025P2.coeff_iterate_derivative_factor The coefficients of an iterated formal derivative are the shifted coefficients of the original polynomial, up to a natural-number factor line 37 source
Source documentation
The coefficients of an iterated formal derivative are the shifted coefficients of the original polynomial, up to a natural-number factor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Real, Nat, Exists, Eq, Finsupp, Polynomial.coeff, Nat.iterate, LinearMap, RingHom.id, Polynomial.derivative, HMul.hMul, HAdd.hAdd
Proof uses: Nat.recAux, Exists.intro, OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, congr, add_zero, Nat.cast_one, mul_one, eq_self, Eq.mpr, id, Nat.succ, Function.iterate_succ_apply', Polynomial.coeff_derivative, Nat.cast_mul, Nat.cast_add, Mathlib.Tactic.Ring.of_eq and 23 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma coeff_iterate_derivative_factor (F : ℝ[X]) (j m : ℕ) :
    ∃ N : ℕ, (derivative^[j] F).coeff m = F.coeff (m + j) * N := by
…
```
lemma Usa2025P2.natDegree_iterate_derivative_eq The degree of an iterated formal derivative, as long as it is nonzero line 50 source
Source documentation
The degree of an iterated formal derivative, as long as it is nonzero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Real, Nat, LE.le, Polynomial.natDegree, Eq, Nat.iterate, LinearMap, RingHom.id, Polynomial.derivative, HSub.hSub
Proof uses: Nat.recAux, OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, tsub_zero, eq_self, HAdd.hAdd, Eq.mpr, id, Nat.succ, Function.iterate_succ_apply', Polynomial.natDegree_derivative
60 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma natDegree_iterate_derivative_eq (F : ℝ[X]) (j : ℕ) (hj : j ≤ F.natDegree) :
    (derivative^[j] F).natDegree = F.natDegree - j := by
…
```
lemma Usa2025P2.good_derivative Rolle's theorem: if a real polynomial has all of its roots real and distinct, then so does its derivative line 61 source
Source documentation
Rolle's theorem: if a real polynomial has all of its roots real and distinct, then so does its derivative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Real, And, Multiset.Nodup, Polynomial.roots, Eq, Nat, Multiset.card, Polynomial.natDegree, LinearMap, RingHom.id, Polynomial.derivative
Proof uses: dite, LE.le, OfNat.ofNat, Iff.mp, Nat.le_zero, LE.le.trans, HSub.hSub, Polynomial.natDegree_derivative_le, Nat.sub_le_sub_right, LE.le.trans_eq, Polynomial.card_roots', Eq.mpr, Multiset, id, congrArg, Multiset.card_eq_zero, And.intro, Multiset.nodup_zero, Multiset.card_zero, Eq.symm and 121 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 96 steps
Open to load the checked before-and-after goal states.
```
lemma good_derivative {F : ℝ[X]}
    (h : F.roots.Nodup ∧ Multiset.card F.roots = F.natDegree) :
    F.derivative.roots.Nodup ∧ Multiset.card F.derivative.roots = F.derivative.natDegree := by
…
```
Mentions: h
lemma Usa2025P2.good_iterate Iterated derivatives of a polynomial with distinct real roots still have distinct real roots line 145 source
Source documentation
Iterated derivatives of a polynomial with distinct real roots still have distinct real roots.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Real, Nat, And, Multiset.Nodup, Polynomial.roots, Eq, Multiset.card, Polynomial.natDegree, Nat.iterate, LinearMap, RingHom.id, Polynomial.derivative
Proof uses: Nat.recAux, Eq.mpr, HAdd.hAdd, OfNat.ofNat, id, congrArg, Nat.succ, Function.iterate_succ_apply', Usa2025P2.good_derivative
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma good_iterate (F : ℝ[X]) (j : ℕ)
    (h : F.roots.Nodup ∧ Multiset.card F.roots = F.natDegree) :
    (derivative^[j] F).roots.Nodup ∧
      Multiset.card (derivative^[j] F).roots = (derivative^[j] F).natDegree := by
…
```
Mentions: h
lemma Usa2025P2.dvd_X_pow_two_iterate_derivative If the coefficients of x^(t-1) and x^t of R both vanish, then X^2 divides the (t-1)-st derivative of R line 155 source
Source documentation
If the coefficients of x^(t-1) and x^t of R both vanish, then X^2 divides the (t-1)-st derivative of R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Real, Nat, LE.le, OfNat.ofNat, Eq, Finsupp, Polynomial.coeff, HSub.hSub, Dvd.dvd, HPow.hPow, Polynomial.X, Nat.iterate, LinearMap, RingHom.id, Polynomial.derivative
Proof uses: Eq.mpr, LT.lt, id, congrArg, propext, Polynomial.X_pow_dvd_iff, HMul.hMul, HAdd.hAdd, Exists, Usa2025P2.coeff_iterate_derivative_factor, dite, MulZeroClass.zero_mul, Eq.refl, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat and 2 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_X_pow_two_iterate_derivative (R : ℝ[X]) {t : ℕ} (ht : 1 ≤ t)
    (h0 : R.coeff (t - 1) = 0) (h1 : R.coeff t = 0) :
    (X : ℝ[X]) ^ 2 ∣ derivative^[t - 1] R := by
…
```
lemma Usa2025P2.not_nodup_roots_of_X_pow_two_dvd A nonzero polynomial divisible by X^2 has 0 as a multiple root, so its root multiset is duplicate-free nowhere line 167 source
Source documentation
A nonzero polynomial divisible by X^2 has 0 as a multiple root, so its root multiset is duplicate-free nowhere.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Real, Ne, OfNat.ofNat, Dvd.dvd, HPow.hPow, Nat, Polynomial.X, Not, Multiset.Nodup, Polynomial.roots
Proof uses: LE.le, Polynomial.rootMultiplicity, Eq.mpr, HSub.hSub, RingHom, Polynomial.C, id, Eq, congrArg, propext, Polynomial.le_rootMultiplicity_iff, congrFun', Eq.trans, map_zero, sub_zero, Multiset.count, Eq.mp, Multiset.nodup_iff_count_le_one, Polynomial.count_roots
58 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma not_nodup_roots_of_X_pow_two_dvd {F : ℝ[X]} (hF : F ≠ 0)
    (h : (X : ℝ[X]) ^ 2 ∣ F) : ¬ F.roots.Nodup := by
…
```
Mentions: h
lemma Usa2025P2.core_pigeonhole The combinatorial heart of the problem line 184 source
Source documentation
The combinatorial heart of the problem. Let s be a set of k + 1 real numbers (with k ≥ 1). Then it is impossible that for every i ∈ s, the polynomial ∏_{r ∈ s \ {i}} (X - r) has a zero coefficient among the positions 1, ..., k - 1. Indeed, two such polynomials would share the position t of a zero coefficient (pigeonhole), forcing the common sub-product ∏_{r ∈ s \ {i₁, i₂}} (X - r) to have two consecutive zero coefficients, contradicting Rolle's theorem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Real, Eq, Finset.card, HAdd.hAdd, Membership.mem, Exists, And, Finset.Icc, HSub.hSub, Finsupp, Polynomial.coeff, Finset.prod, Polynomial, Finset.erase, Polynomial.X, RingHom and 2 more
Proof uses: Subtype, Subtype.property, dite, Subtype.mk, Not, rfl, LT.lt, Eq.mpr, id, congrArg, Nat.card_Icc, Ne, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Set, dite_eq_left, And.left, Eq.symm, And.right, Eq.mp, Finset.card_erase_of_mem and 112 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 89 steps
Open to load the checked before-and-after goal states.
```
lemma core_pigeonhole {k : ℕ} (hk : 1 ≤ k) {s : Finset ℝ} (hscard : s.card = k + 1)
    (H : ∀ i ∈ s, ∃ t ∈ Finset.Icc 1 (k - 1),
      (∏ r ∈ s.erase i, (X - C r)).coeff t = 0) :
    False := by
…
```
lemma Usa2025P2.roots_real_aux If every complex root of a squarefree real polynomial P is real, then the real roots of P are distinct and there are deg P many of them (i.e. P splits over ℝ) line 275 source
Source documentation
If every complex root of a squarefree real polynomial P is real, then the real roots of P are distinct and there are deg P many of them (i.e. P splits over ℝ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Real, Ne, OfNat.ofNat, Squarefree, Complex, Eq, AlgHom, Polynomial.aeval, Complex.im, And, Multiset.Nodup, Polynomial.roots, Nat, Multiset.card, Polynomial.natDegree
Proof uses: Polynomial.Separable, Iff.mpr, PerfectField.separable_iff_squarefree, Polynomial.nodup_roots, And.intro, Polynomial.map, Algebra.algebraMap, rfl, Function.Injective, RingHom, RingHom.injective, Polynomial.map_ne_zero, Polynomial.Separable.map, Membership.mem, Multiset, Eq.mpr, Polynomial.eval₂, id, congrArg, Polynomial.aeval_def and 36 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma roots_real_aux {P : ℝ[X]} (hP : P ≠ 0) (hsq : Squarefree P)
    (h : ∀ z : ℂ, aeval z P = 0 → z.im = 0) :
    P.roots.Nodup ∧ Multiset.card P.roots = P.natDegree := by
…
```
Mentions: P, h
problem Usa2025P2.usa2025_p2 line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, OfNat.ofNat, Polynomial, Real, Eq, Polynomial.natDegree, Squarefree, Ne, Polynomial.eval, Fin, HAdd.hAdd, Dvd.dvd, Finset.sum, Finset.univ, HMul.hMul, RingHom, Polynomial.C, HPow.hPow and 8 more
Proof uses: False, Eq.symm, Classical.byContradiction, Not, Multiset.Nodup, Polynomial.roots, Multiset.card, Usa2025P2.roots_real_aux, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Finset, Multiset.toFinset, rfl, Finset.card, Eq.mpr and 71 more
173 instances, coercions and auxiliary constants left out.

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