Beyond Sendov's conjecture: the quadratic Tang--Zhang inequality

Very recently, Lech Mazur proved the celebrated Sendov conjecture, and Terence Tao subsequently distilled the main ideas of the proof in a blog post. In this paper, we establish a quantitative strengthening of Sendov’s conjecture, namely the quadratic Tang–Zhang inequality. Let $p$ be a polynomial of degree $n\ge 2$ whose zeros lie in the closed unit disk, and let ${\zeta }_1,\dots ,{\zeta }_{n-1}$ denote its critical points, counted with multiplicity. We prove that, for every zero $a$ of $p$, $$\sum _{j=1}^{n-1}\frac{1}{\mathrm{\mid }a-{\zeta }_j{\mathrm{\mid }}^2}\ge n-1.$$ Moreover, equality holds if and only if $p(z)=c(z^n-\omega )$ for some $c\in \mathbb{C}\setminus \{0\}$ and $\mathrm{\mid }\omega \mathrm{\mid }=1$. We also provide a Lean 4 formalization of the main results.