Sendov's conjecture for a real interior zero

This file assembles everything: if p has degree n ≥ 2, all zeroes in the closed unit disk, and a zero at a real a with 0 < a < 1, then p' has a zero within distance 1 of a.

The proof is by contradiction. Suppose not; then every critical point w satisfies ‖w - a‖ ≥ 1, so Sendov.exists_crit_multiset writes p' over points qⱼ of the closed unit disk, and Sendov.exists_root_multiset writes p over the other zeroes zⱼ. Setting x + iy = (∑ⱼ qⱼ)/(n-1), the two channels are:

• polar: the polar identity and p'(a) two ways feed the branch point (⋆).

From (⋆) the argument branches on the degree.

• For n ≥ 5, AM–GM relaxes (⋆) to the raw polar inequality (1Q), the centroid identity and the two origin identities give (origin-exact), and Sendov.polar_origin_incompatible says the two cannot hold together.
• For n ≤ 5, Sendov.low_degree_contradiction shows (⋆) is already contradictory on its own, with no recourse to the origin channel. The two branches overlap at degree five.

The zero a = 0 is excluded above (the polar identity divides by a) but needs none of this machinery: p'(a) two ways already says (∏ⱼ qⱼ)(∏ⱼ (a - zⱼ)) = n, and at a = 0 both factors have norm at most one.

Main statements

• Sendov.sendov_interior: the conjecture for a real zero 0 < a < 1, every degree n ≥ 2;
• Sendov.sendov_center: the conjecture at a = 0;
• Sendov.sendov_interior_real: the two combined, 0 ≤ a < 1.

theorem Sendov.sendov_interior {n : ℕ} (hn : 2 ≤ n) {p : Polynomial ℂ} (hdeg : p.natDegree = n) (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) (hpa : Polynomial.eval (↑a) p = 0) : ∃ (ζ : ℂ), Polynomial.eval ζ (Polynomial.derivative p) = 0 ∧ ‖ζ - ↑a‖ < 1

Sendov's conjecture for a real interior zero. If every zero of p lies in the closed unit disk and p(a) = 0 for a real a with 0 < a < 1, then some zero of p' lies within distance 1 of a.

theorem Sendov.sendov_center {n : ℕ} (hn : 2 ≤ n) {p : Polynomial ℂ} (hdeg : p.natDegree = n) (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) (hp0 : Polynomial.eval 0 p = 0) : ∃ (ζ : ℂ), Polynomial.eval ζ (Polynomial.derivative p) = 0 ∧ ‖ζ‖ < 1

The conjecture at a = 0. p'(a) two ways gives (∏ⱼ qⱼ)(∏ⱼ (a - zⱼ)) = n. At a = 0 the second factor is ∏ⱼ zⱼ up to sign, so both factors have norm at most one and n ≤ 1 — impossible for n ≥ 2. No polar or origin estimate is involved.

theorem Sendov.sendov_interior_real {n : ℕ} (hn : 2 ≤ n) {p : Polynomial ℂ} (hdeg : p.natDegree = n) (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) (hpa : Polynomial.eval (↑a) p = 0) : ∃ (ζ : ℂ), Polynomial.eval ζ (Polynomial.derivative p) = 0 ∧ ‖ζ - ↑a‖ < 1

The conjecture for a real zero in [0,1), every degree n ≥ 2.