Smale's mean value constant (1981) equals 4

For a complex polynomial p of degree d ≥ 2 with p(0) = 0 and p′(0) ≠ 0, let S(p) be the minimum of |p(c)/(c p′(0))| over the critical points c of p, and let K(d) be the supremum of S(p) over all such p of degree d. In 1981 Smale proved that K(d) ≤ 4 for every d, and asked whether 4 can be replaced by 1. We prove that Smale's mean value constant supd K(d) equals 4 and that K(d) → 4 as d → ∞, combining a reduction due to Jatar and Ng with an explicit construction. In particular, 4 cannot be replaced by any smaller constant. Each K(d) is known to be below 4, so the supremum is not attained. The main result has also been formalized in the Lean 4 proof assistant.