Rubinstein's boundary theorem, at the zero a = 1

If p has degree n ≥ 2, all zeroes in the closed unit disk, and p(1) = 0, then p' has a zero strictly inside D(1,1) unless p = c(Xⁿ - 1).

The polar identity is useless here: at a = 1 the reflected point 1/a coincides with a, 1 - a² = 0, and the identity degenerates. One elementary identity replaces it, obtained from p''(1)/p'(1). Writing p = c(X-1)Q and p' = ncR, evaluation at 1 gives

Q(1) = n R(1) and 2 Q'(1) = n R'(1)

— the factor 2 coming from p''(1) = 2Q'(1) — whence the boundary reciprocal identity

∑ⱼ qⱼ = 2 ∑ⱼ 1/(1 - zⱼ), qⱼ = 1/(1 - wⱼ).

Both sides are then sandwiched. On the left Re qⱼ ≤ ‖qⱼ‖ ≤ 1, so the real part is at most n-1; on the right Re 1/(1-z) ≥ 1/2 for ‖z‖ ≤ 1, because Re 1/(1-z) - 1/2 = (1-‖z‖²)/(2‖1-z‖²), so the real part is at least n-1. Equality forces Re qⱼ = 1 for every j, hence qⱼ = 1, hence every critical point is 0, hence p' = n c Xⁿ⁻¹ and p = c(Xⁿ - 1).

The repeated-root case is handled before any division: if 1 is a multiple zero then p'(1) = 0 and ζ = 1 is a strict witness, so under the contradiction hypothesis p'(1) ≠ 0 and every zⱼ ≠ 1.

No polar integral, origin identity, defect lemma, numerical certificate or Gauss–Lucas theorem is used. Only the two factorizations of Sendov.Counterexample.Factor are shared with the interior argument.

Main statements

• Sendov.rubinstein_one: the strict-or-extremal alternative;
• Sendov.sendov_boundary_one: the closed-disk form, ‖ζ - 1‖ ≤ 1;
• Sendov.boundary_reciprocal: (BR), in division-free form.

Evaluating ∏ⱼ (X - zⱼ) and its derivative at a point

The versions in Sendov.Counterexample.Identities are specialized to the origin; the boundary argument needs them at 1.

theorem Sendov.eval_prod_at (u : ℂ) (s : Multiset ℂ) : Polynomial.eval u (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) s).prod = (Multiset.map (fun (w : ℂ) => u - w) s).prod

theorem Sendov.eval_deriv_prod_at (u : ℂ) (s : Multiset ℂ) : Polynomial.eval u (Polynomial.derivative (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) s).prod) = sumEraseProd (Multiset.map (fun (w : ℂ) => u - w) s)

Scalar facts

theorem Sendov.half_le_re_inv_one_sub {z : ℂ} (hz : ‖z‖ ≤ 1) (hz1 : z ≠ 1) : 1 / 2 ≤ (1 - z)⁻¹.re

The disk inequality. Re 1/(1-z) ≥ 1/2 for ‖z‖ ≤ 1, z ≠ 1; after clearing the positive denominator this is exactly 1 - ‖z‖² ≥ 0.

theorem Sendov.eq_one_of_re_eq_one_of_norm_le_one {v : ℂ} (hre : v.re = 1) (hv : ‖v‖ ≤ 1) : v = 1

A point of the closed unit disk with real part 1 is 1.

theorem Sendov.eq_zero_of_sum_eq_zero {s : Multiset ℝ} (hs : ∀ x ∈ s, 0 ≤ x) (h : s.sum = 0) (x : ℝ) : x ∈ s → x = 0

A multiset of nonnegative reals summing to zero is all zeroes.

theorem Sendov.sum_le_card_mul (c : ℝ) (s : Multiset ℝ) : (∀ x ∈ s, x ≤ c) → s.sum ≤ ↑s.card * c

theorem Sendov.card_mul_le_sum (c : ℝ) (s : Multiset ℝ) : (∀ x ∈ s, c ≤ x) → ↑s.card * c ≤ s.sum

theorem Sendov.sum_map_one_sub_re (s : Multiset ℂ) : (Multiset.map (fun (v : ℂ) => 1 - v.re) s).sum = ↑s.card - (Multiset.map (fun (v : ℂ) => v.re) s).sum

The boundary reciprocal identity

theorem Sendov.boundary_reciprocal {n : ℕ} {Zs Qi : Multiset ℂ} (hn0 : ↑n ≠ 0) (hZ : ∀ u ∈ Zs, u ≠ 0) (hQ : ∀ u ∈ Qi, u ≠ 0) (hI : Zs.prod = ↑n * Qi.prod) (hII : 2 * sumEraseProd Zs = ↑n * sumEraseProd Qi) : (Multiset.map (fun (u : ℂ) => u⁻¹) Qi).sum = 2 * (Multiset.map (fun (u : ℂ) => u⁻¹) Zs).sum

(BR), in division-free form. From ∏ Zs = n ∏ Qi and 2 ∑ₑ Zs = n ∑ₑ Qi — the two readings of p'(1) and p''(1) — one gets ∑ⱼ 1/Qiⱼ = 2 ∑ⱼ 1/Zsⱼ. Applied with Zsⱼ = 1 - zⱼ and Qiⱼ = 1/qⱼ this is ∑ⱼ qⱼ = 2 ∑ⱼ 1/(1-zⱼ).

The sandwich

theorem Sendov.all_q_eq_one {N : ℕ} {qs zs : Multiset ℂ} (hqcard : qs.card = N) (hzcard : zs.card = N) (hq1 : ∀ v ∈ qs, ‖v‖ ≤ 1) (hz1 : ∀ w ∈ zs, ‖w‖ ≤ 1) (hzne : ∀ w ∈ zs, w ≠ 1) (hBR : qs.sum = 2 * (Multiset.map (fun (w : ℂ) => (1 - w)⁻¹) zs).sum) (v : ℂ) : v ∈ qs → v = 1

Both sides of (BR) are pinned: the left has real part at most N, the right at least N, so every qⱼ has real part 1 and hence, lying in the closed unit disk, equals 1.

Rubinstein's theorem at a = 1

theorem Sendov.rubinstein_one {n : ℕ} (hn : 2 ≤ n) {p : Polynomial ℂ} (hdeg : p.natDegree = n) (hroots : ∀ w ∈ p.roots, ‖w‖ ≤ 1) (hp1 : Polynomial.eval 1 p = 0) : (∃ (ζ : ℂ), Polynomial.eval ζ (Polynomial.derivative p) = 0 ∧ ‖ζ - 1‖ < 1) ∨ p = Polynomial.C p.leadingCoeff * (Polynomial.X ^ n - 1)

Rubinstein's boundary theorem at a = 1, with its equality case.

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

The closed-disk form. In the extremal case p = c(Xⁿ - 1) the only critical point is 0, at distance exactly 1 from the zero 1.