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

5 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1989, Problem 3

Let P(z) = zⁿ + c₁zⁿ⁻¹ + ⋯ + cₙ be a polynomial in the complex variable z, with real coefficients cₖ. Suppose that |P(i)| < 1. Prove that there exist real numbers a and b such that P(a + bi) = 0 and (a² + b² + 1)² < 4b² + 1.

Imports (5)

Imported by 1 file

Compfiles.lean

theorem Usa1989P3.star_eval Evaluating a polynomial whose coefficients are all real at the conjugate of z is the same as conjugating its value at z line 35 source
Source documentation
Evaluating a polynomial whose coefficients are all real at the conjugate of z is the same as conjugating its value at z.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Nat, Eq, Real, Complex.im, Finsupp, Polynomial.coeff, OfNat.ofNat, Star.star, Polynomial.eval
Proof uses: RingHom, starRingEnd, Eq.mpr, Finset.sum, Finset.range, HAdd.hAdd, Polynomial.natDegree, HMul.hMul, HPow.hPow, id, congrArg, Polynomial.eval_eq_sum_range, map_sum, NNRat, RingHom.id, Finset.sum_congr, rfl, Finset, Membership.mem, map_mul and 6 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem star_eval {P : ℂ[X]} (hreal : ∀ n : ℕ, (P.coeff n).im = 0) (z : ℂ) :
    star (P.eval z) = P.eval (star z) := by
…
```
Mentions: P
theorem Usa1989P3.normSq_I_sub_mul_normSq_I_add For a complex number r, the product of the squared distances from r to i and to -i equals (r.re² + r.im² + 1)² - 4 r.im² line 47 source
Source documentation
For a complex number r, the product of the squared distances from r to i and to -i equals (r.re² + r.im² + 1)² - 4 r.im².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Eq, Real, HMul.hMul, MonoidWithZeroHom, Complex.normSq, HSub.hSub, Complex.I, HAdd.hAdd, HPow.hPow, Nat, Complex.re, OfNat.ofNat, Complex.im
Proof uses: id, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, congrArg, Eq.symm, Eq.refl and 48 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem normSq_I_sub_mul_normSq_I_add (r : ℂ) :
    Complex.normSq (Complex.I - r) * Complex.normSq (Complex.I + r) =
      (r.re ^ 2 + r.im ^ 2 + 1) ^ 2 - 4 * r.im ^ 2 := by
…
```
theorem Usa1989P3.prod_normSq_sub_roots The squared distances from the roots of a monic polynomial to a point z multiply to the squared norm of the value of the polynomial at z line 56 source
Source documentation
The squared distances from the roots of a monic polynomial to a point z multiply to the squared norm of the value of the polynomial at z.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Polynomial.Splits, Polynomial.Monic, Eq, Real, Multiset.prod, Multiset.map, MonoidWithZeroHom, Complex.normSq, HSub.hSub, Polynomial.roots, Polynomial.eval
Proof uses: Eq.mpr, id, congrArg, Polynomial.Splits.eval_eq_prod_roots_of_monic, map_multiset_prod, Function.comp, Multiset, Multiset.map_map, Eq.refl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem prod_normSq_sub_roots {P : ℂ[X]} (hsplit : P.Splits) (hmonic : P.Monic) (z : ℂ) :
    (P.roots.map fun r ↦ Complex.normSq (z - r)).prod =
      Complex.normSq (P.eval z) := by
…
```
Mentions: P
theorem Usa1989P3.prod_normSq_add_roots The squared distances from the roots of a monic polynomial to a point z, with signs flipped, again multiply to the squared norm of the value of the polynomial at -z line 65 source
Source documentation
The squared distances from the roots of a monic polynomial to a point z, with signs flipped, again multiply to the squared norm of the value of the polynomial at -z.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Polynomial.Splits, Polynomial.Monic, Eq, Real, Multiset.prod, Multiset.map, MonoidWithZeroHom, Complex.normSq, HAdd.hAdd, Polynomial.roots, Polynomial.eval, Neg.neg
Proof uses: HSub.hSub, funext, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.neg_congr, Int.rawCast and 20 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem prod_normSq_add_roots {P : ℂ[X]} (hsplit : P.Splits) (hmonic : P.Monic) (z : ℂ) :
    (P.roots.map fun r ↦ Complex.normSq (z + r)).prod =
      Complex.normSq (P.eval (-z)) := by
…
```
Mentions: P
problem Usa1989P3.usa1989_p3 line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Complex, Polynomial.Monic, Nat, Eq, Real, Complex.im, Finsupp, Polynomial.coeff, OfNat.ofNat, LT.lt, Norm.norm, Polynomial.eval, Complex.I, Exists, And, HAdd.hAdd, HMul.hMul, HPow.hPow
Proof uses: Polynomial.Splits, IsAlgClosed.splits, Ne, Polynomial.Monic.ne_zero, MonoidWithZeroHom, Complex.normSq, Eq.mpr, id, congrArg, Complex.normSq_eq_norm_sq, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance and 107 more
164 instances, coercions and auxiliary constants left out.

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