← All papers
First page of Smale's mean value constant and admissible univalent Blaschke pairs

Smale's mean value constant and admissible univalent Blaschke pairs

Aneesh Jatar, Tuen Wai Ng

math.CV Oct 15, 2026 · v1
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.
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$.

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.

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.

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.