Smale's mean value constant and admissible univalent Blaschke pairs
Aneesh Jatar, Tuen Wai Ng
math.CV
Oct 15, 2026 · v1
TL;DR
Builds on and credits a third-party Lean 4/Mathlib machine-checked disproof of the constant-1 Smale mean value conjecture, produced by GPT-6 Astra.
Abstract
Let $\mathcal{P}$ be the class of polynomials $P$ of degree at least $2$ with $P(0)=0$, $P'(0)=1$, let $S(P)=\min_{P'(c)=0}|P(c)/c|$ and let $\mathcal{M}=\sup_{P\in\mathcal{P}}S(P)$ be Smale's mean value constant. Smale proved that $\mathcal{M}\le4$, observed that $\mathcal{M}\ge 1$, and asked whether $\mathcal{M}=1$. We show that $\mathcal{M}$ coincides with $$ \mathcal{B}=\sup\frac1{B(0)}, $$ the supremum running over pairs $(W,B)$ in which $W$ is a normalised univalent map of the standard unit disk $\mathbb{D}$ and $B$ is a finite Blaschke product with $B(0)>0$ such that $WB$ is locally univalent in $\mathbb{D}$. Smale's question is therefore a problem in univalent function theory. We also introduce the degree-restricted constants $\mathcal{B}_d$ for $B$ with $\mathrm{deg} B \le d$ and show that $$1.1018586788\ldots=\sqrt{\frac{8081}{6656}} \le \mathcal{B}_1 < \sqrt{\frac{7}{5}}=1.1832159566\ldots$$ This implies that $\mathcal{M}>1.1018$ and we also show that there are polynomials of arbitrarily large degree with $S(P)>1.1018$.
Problem
Smale's mean value constant M is the supremum over normalised polynomials of the minimum of |P(c)/c| over critical points c. Smale proved M ≤ 4 and asked whether M = 1. A Lean 4/Mathlib-checked construction by GPT-6 Astra showed M > 1 but gave only a tiny margin.
Approach
Builds on that Lean-verified construction and recasts the problem in univalent function theory. It introduces admissible pairs (W,B): W is a normalised univalent map of the disk and B is a finite Blaschke product with B(0)>0 such that WB is locally univalent. It shows M equals the supremum B of 1/B(0) over such pairs, and constructs explicit degree-one pairs from quartic polynomials using Dieudonné's univalence test.
Results
Proves M = B and gives the degree-one bounds sqrt(8081/6656) ≈ 1.10186 ≤ B_1 < sqrt(7/5), so M > 1.1018, with such polynomials existing in arbitrarily large degree. Also shows B_d < 4 − C/d², that every degree occurs, and that each B_d is attained.