\pdfoutput=1 \documentclass[11pt]{amsart} \usepackage{amssymb,amsmath,booktabs,array} \usepackage[margin=1in]{geometry} \usepackage{tikz} \usetikzlibrary{shapes.misc,patterns} \usepackage[export]{adjustbox} \usepackage{graphicx} \usepackage{hyperref} \hypersetup{pdftitle={Smale's mean value constant (1981) exceeds 1.1559}, pdfauthor={Dave Goel}, hidelinks} \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\D}{\mathbb D} \newcommand{\cS}{\mathcal S} \title{Smale's mean value constant (1981) exceeds 1.1559} \author{Dave Goel}\date{October 28, 2026. Revised: November 9, 2026} \thanks{The Lean~4 proof and the programs and data of Section~\ref{sec:pair} are at \url{https://github.com/david44hello/papers_supporting_materials/tree/smale-mean-value-constant-v2.90/smale-mean-value-constant}.} \begin{document} \begin{abstract} We prove that Smale's mean value constant exceeds $1.1559837$, improving the bound $1.1018$ of Jatar and Ng. Smale proved in 1981 that for every complex polynomial $P$ of degree at least $2$ and every point $z$ with $P'(z)\neq0$, some critical point $\zeta$ of $P$ satisfies $|P(z)-P(\zeta)|\le K\,|z-\zeta|\,|P'(z)|$ with $K=4$, and he conjectured that $K=1$ suffices. The best constant $K^*$ is called Smale's mean value constant. Smale's conjecture is false: a proof that $K^*>1$ appeared in 2026. Jatar and Ng showed that every pair $(W,B)$ of a normalized univalent map $W$ of the unit disk and a finite Blaschke product $B$ with $B(0)>0$, such that $(WB)'$ has no zero in the disk, gives $K^*\ge1/B(0)$. We construct such a pair explicitly, with $B$ of degree two, from a polynomial of degree $18$ with Gaussian rational coefficients, and we verify the required properties by a computation in exact arithmetic. Since the best constant $K(d)$ for degree $d$ is nondecreasing in $d$ (Crane), $K(d)$ also exceeds $1.1559837$ for all large $d$. All theorems, lemmas and corollaries of this paper, and the results of Jatar and Ng that it uses, are also proved in the Lean~4 proof assistant and checked with the Lean comparator. \end{abstract} \subjclass[2020]{Primary 30C10; Secondary 30C15, 30C45, 30J10} \keywords{Smale's mean value conjecture, univalent functions, Blaschke products} \maketitle {\footnotesize\leftskip=3pc\rightskip=3pc\noindent\textbf{AI Disclosure.} This work was done overwhelmingly by AI models and supervised by the author. The models were Anthropic's Claude and OpenAI's ChatGPT. The author takes full responsibility for the paper.\par} \section{Introduction}\label{sec:intro} We prove that Smale's mean value constant $K^*$, defined below, exceeds $1.1559837$. The best lower bound proved before was $1.1018$, due to Jatar and Ng~\cite{JatarNg2026b}. \subsection*{Smale's mean value problem} For $d\ge2$ let $\mathcal P_d$ be the set of complex polynomials $p$ of degree $d$ with $p(0)=0$ and $p'(0)=1$. Every critical point $\beta$ of such a $p$ is nonzero, as $p'(0)=1$, and we put \[ m(p)=\min_{p'(\beta)=0}\frac{|p(\beta)|}{|\beta|},\qquad K(d)=\sup_{p\in\mathcal P_d}m(p),\qquad K^*=\sup_{d\ge2}K(d). \] If $P$ is a polynomial of degree $d$ and $P'(z)\neq0$, then $p(u)=(P(z+u)-P(z))/P'(z)$ lies in $\mathcal P_d$, and its critical points are the points $\beta=\zeta-z$ with $\zeta$ a critical point of $P$. So $K(d)$ is the best constant $K$ in the inequality \begin{equation}\label{eq:smale} \Bigl|\frac{P(z)-P(\zeta)}{z-\zeta}\Bigr|\le K\,|P'(z)|\qquad\text{for some critical point $\zeta$ of $P$}, \end{equation} over all polynomials $P$ of degree $d$ and all $z$ with $P'(z)\neq0$, and $K^*$ is the best constant over all degrees: \emph{Smale's mean value constant}. In words, \eqref{eq:smale} says that the mean rate of change of $P$ between $z$ and some critical point $\zeta$ is at most $K$ times its rate of change at $z$; hence the name. Smale proved~\eqref{eq:smale} with $K=4$~\cite{Smale1981}, so $K^*\le4$. The polynomial $p(z)=z-z^d/d$ gives $K(d)\ge{(d-1)/d}$ (its critical points $\beta$ are the $(d-1)$-st roots of unity, and $p(\beta)/\beta=1-\beta^{d-1}/d=(d-1)/d$ at each). Smale conjectured that $K^*=1$, and even that $K(d)={(d-1)/d}$ for every $d$; this is \emph{Smale's mean value conjecture}. The mean value problem is the first of the additional problems in Smale's list of problems for the next century~\cite{Smale2000}. The equality $K(d)={(d-1)/d}$ holds for $d\le4$ (Tischler~\cite{Tischler1989}; see also~\cite[Sect.~7.2]{RahmanSchmeisser2002}), and Crane announced a computer-assisted proof for $d=5$~\cite[Sect.~1]{Crane2007}. Every later improvement of the constant $4$ is a bound for $K(d)$ that depends on $d$. For example, Beardon, Minda and Ng proved $K(d)\le4^{(d-2)/(d-1)}$ using an estimate for the hyperbolic metric~\cite{BeardonMindaNg2002}; Conte, Fujikawa and Lakic proved $K(d)\le4(d-1)/(d+1)$ using Bieberbach's bound for the second coefficient of univalent functions~\cite{ConteFujikawaLakic2007}; Fujikawa and Sugawa combined the two methods~\cite{FujikawaSugawa2006}; and Crane proved $K(d)<4-2.263/\sqrt d$ for $d\ge8$~\cite{Crane2007}. All these bounds tend to $4$ as $d\to\infty$, so $4$ is still the best known upper bound for $K^*$. Crane also showed that $K(d)$ is nondecreasing in $d$~\cite{Crane2006}. Smale's conjecture is false: a proof that $K^*>1$ was made public in September 2026~\cite{LeanMVP2026}; it shows that some $p$ has $m(p)>1$, but does not make the degree of $p$ explicit. Jatar and Ng~\cite{JatarNg2026b} then recast the problem in terms of pairs of a univalent map of the unit disk and a finite Blaschke product (Section~\ref{sec:pairs}) and proved \[ K^*\ge\sqrt{8081/6656}=1.1018586\ldots; \] this bound comes from an explicit pair. (In~\cite{JatarNg2026b}, $m(p)$, $K(d)$ and $K^*$ are written $S(P)$, $\mathcal M_d$ and $\mathcal M$.) Adamczewski and Colbrook~\cite{AdamczewskiColbrook2026} explain the mechanism behind the proof in~\cite{LeanMVP2026} and give an explicit polynomial $p$ of degree $29\,984$ with $m(p)>1.0000004$, verified by interval arithmetic; it gives $K(d)>1$ for every $d\ge29\,984$. \subsection*{Main result} The table compares the best earlier bounds with ours. \begin{center} \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.48\textwidth}@{\hspace{0.04\textwidth}}>{\raggedright\arraybackslash}p{0.45\textwidth}@{}} \toprule \textbf{Best result before this paper} & \textbf{New result}\\ \midrule $K^*>1.1018$~\cite[Thm.~1.3]{JatarNg2026b}; $K^*>1.1030$, stated without proof in~\cite[Rem.~6.7]{JatarNg2026b} & $K^*>1.1559837$ (Theorem~\ref{thm:main})\\[3pt] $K(d)>1.1018$ for all large $d$~\cite[Thm.~1.3]{JatarNg2026b} & $K(d)>1.1559837$ for all large $d$ (Corollary~\ref{cor:Kd})\\ \bottomrule \end{tabular} \end{center} \begin{theorem}\label{thm:intro} Smale's mean value constant satisfies $K^*\ge\sqrt\Lambda$, where $\Lambda$ is the rational number \[ \Lambda=\frac{2679525219362263370274816001747955444675871769085742015997} {2005184811347697816912979513414954793585480256604979855360} \] and $\sqrt\Lambda=1.15598372919\ldots$; in particular $K^*>1.1559837$, and $K(d)>1.1559837$ for all sufficiently large $d$. \end{theorem} \begin{figure}[ht] \centering \begin{tikzpicture}[x=3.6cm,y=1cm,font=\small] \foreach \yy/\bound/\name in {1.05/0.1018586/known before this work: $K^*>1.1018$, 0/0.1559837/this work: $K^*>1.1559$} { \fill[black!55] (0,\yy) rectangle (\bound,\yy+0.42); \fill[pattern=north east lines,pattern color=black!45] (\bound,\yy) rectangle (3,\yy+0.42); \draw (0,\yy) rectangle (3,\yy+0.42); \node[above right,inner sep=1pt] at (0,\yy+0.44) {\name}; \node[fill=white,inner sep=1.5pt] at (1.55,\yy+0.21) {$K^*$ lies somewhere here}; \node[left,inner sep=3pt] at (0,\yy+0.21) {$1$}; \node[right,inner sep=3pt] at (3,\yy+0.21) {$4$}; } \end{tikzpicture} \caption{What is known about $K^*$, to scale. Each bar runs from $1$, the value Smale conjectured, to $4$, his upper bound of 1981. The dark part is excluded by the best lower bound; the hatched part is left open.}\label{fig:known} \end{figure} The bound comes from a single explicit admissible pair $(W,B)$ in the sense of Jatar and Ng (Definition~\ref{def:admissible}), with $B$ of degree two. We build it from a polynomial $Q$ of degree $18$, whose derivative has a zero of order $5$ at $z=1$, by a construction of Jatar and Ng~\cite[Lemma~6.2]{JatarNg2026b} that we extend from one zero of $B$ to several (Lemma~\ref{lem:kzero}). The coefficients of $Q$ and the zeros of $Q$ used in the construction are Gaussian rationals. That the pair has the required properties reduces, by Dieudonn\'e's univalence criterion and the Schur--Cohn test, to four finite checks (Lemma~\ref{lem:certify}); the main check says that a certain polynomial of degree $578$ in one real variable has no zero in $[-1,1]$. All four checks are made in exact arithmetic, on the exact data printed in Section~\ref{sec:pair}. An expanded version of this paper, with further results, is posted on Zenodo~\cite{GoelLong}. \section{Admissible pairs}\label{sec:pairs} Let $\D=\{|w|<1\}$ be the unit disk and $\cS$ the class of univalent (holomorphic and injective) maps $W$ of $\D$ with $W(0)=0$ and $W'(0)=1$. For $a\in\D$ let $B_a(w)=(w-a)/(1-\bar aw)$. A \emph{finite Blaschke product of degree $k\ge0$} is a function $B=\lambda B_{a_1}\cdots B_{a_k}$ with $|\lambda|=1$ and $a_1,\dots,a_k\in\D$. \begin{definition}[{\cite[Def.~1.1]{JatarNg2026b}}]\label{def:admissible} An \emph{admissible pair} is a pair $(W,B)$ of a map $W\in\cS$ and a finite Blaschke product $B$ with $B(0)>0$ such that the derivative $(WB)'$ has no zero in $\D$. We write $\sigma_k$ for the supremum of $1/B(0)$ over the admissible pairs with $\deg B\le k$. \end{definition} \begin{theorem}[Jatar and Ng]\label{thm:JN} For every admissible pair $(W,B)$ and every $A<1/B(0)$ there is a polynomial $p\in\mathcal P_d$, for some $d\ge2$, with $m(p)>A$~\cite[Prop.~4.2]{JatarNg2026b}. Hence $K^*\ge1/B(0)$ for every admissible pair. \end{theorem} The condition in Definition~\ref{def:admissible} concerns the open disk only: if $WB$ extends holomorphically across the unit circle, $(WB)'$ may vanish there. The pair of Section~\ref{sec:pair} has such a zero, of order $5$. It is still admissible, and~\cite[Prop.~4.2]{JatarNg2026b} is stated for every admissible pair. Its proof first reduces to pairs with no zero of $(WB)'$ on the closed disk~\cite[Lemma~2.1]{JatarNg2026b}, as follows. Let $B$ be nonconstant, and let $t<1$ satisfy $t>B(0)$ and $t>|B(z)|$ at every critical point $z$ of $B$ in $\D$. Then the set $\Omega_t=\{z\in\D:|B(z)|0$. Then $\psi_t$ extends conformally across the circle, and $(W^{(t)},B^{(t)})=\bigl(W\circ\psi_t/\psi_t'(0),\,B\circ\psi_t/t\bigr)$ is an admissible pair. Moreover $(W^{(t)}B^{(t)})'=(WB)'(\psi_t)\,\psi_t'/(t\psi_t'(0))$ has no zero even on the closed disk, and $1/B^{(t)}(0)=t/B(0)$ tends to $1/B(0)$ as $t\to1$. \begin{remark}[From polynomials to pairs]\label{rem:converse} The link between pairs and polynomials is easiest to see by going from polynomials to pairs~\cite[Prop.~3.1]{JatarNg2026b}. Let $p\in\mathcal P_d$ with $m(p)>1$, let $10$, and put $W=\psi/\kappa$ and $B=(q\circ\psi)/R$. Then $W\in\cS$ and $B(0)=1/R$. Moreover $B$ is a finite Blaschke product: since $|q|R$ and so lies outside $\Omega$. So $(W,B)$ is admissible with $1/B(0)=R$; letting $R\to m(p)$ gives $m(p)\le\sup_k\sigma_k$. This also holds when $m(p)\le1$, since the admissible pair $W(w)=w$, $B=1$ gives $\sigma_k\ge1$ for every $k$. Hence $K^*\le\sup_k\sigma_k$. Theorem~\ref{thm:JN} goes the other way, so $K^*=\sup_k\sigma_k$~\cite[Thm.~1.2]{JatarNg2026b}. From a given pair, Jatar and Ng build polynomials $p$ with $m(p)$ close to $1/B(0)$, using Runge's theorem and Hilbert's lemniscate theorem. \end{remark} \section{A construction of admissible pairs}\label{sec:construction} For $a,b\in\D$ with $a\neq b$ put \[ J(a,b)=1+\frac{(1-|a|^2)(1-|b|^2)}{|a-b|^2}. \] Since $|1-\bar ab|^2-|a-b|^2=(1-|a|^2)(1-|b|^2)$, we have $1/|B_a(b)|^2=J(a,b)$. For $b\in\D$ let $\varphi(w)=(w+b)/(1+\bar bw)$; it maps $\D$ onto $\D$, with $\varphi(0)=b$ and $\varphi'(0)=1-|b|^2$. The idea of the next lemma is to start from a polynomial $Q$ without critical points in $\D$ and to divide out the Blaschke factors $B_{a_j}$ of some of its zeros $a_1,\dots,a_k$ in $\D$. If the quotient $H$ is univalent, then $Q=H\prod_jB_{a_j}$ is a univalent function times a Blaschke product, and the derivative of this product is $Q'$, which has no zero in $\D$ by the choice of $Q$; composition with the automorphism $\varphi$ moves a further zero $b$ of $Q$ to $0$. The bound $1/B(0)=\prod_j1/|B_{a_j}(b)|$ is large when the $a_j$ are close to $b$ in the pseudo-hyperbolic distance $|B_{a_j}(b)|$; what limits it is that $Q$ must keep its critical points out of $\D$ while $H$ stays univalent. For $k=1$ the lemma is~\cite[Lemma~6.2]{JatarNg2026b}. \begin{lemma}\label{lem:kzero} Let $k\ge1$ and let $Q$ be a polynomial such that $Q'$ has no zero in $\D$ and $Q$ has $k+1$ distinct zeros $b,a_1,\dots,a_k$ in $\D$. Suppose that the polynomial \[ H(z)=Q(z)\prod_{j=1}^k\frac{1-\bar a_jz}{z-a_j} \] is univalent in $\D$. Put $N=(1-|b|^2)H'(b)$, $\eta=\prod_{j=1}^kB_{a_j}(b)$, \[ W=\frac{H\circ\varphi}{N},\qquad B=\frac{|\eta|}{\eta}\prod_{j=1}^kB_{a_j}\circ\varphi . \] Then $(W,B)$ is an admissible pair, $\deg B=k$, and \[ \frac1{B(0)^2}=\prod_{j=1}^kJ(a_j,b). \] \end{lemma} \begin{proof} Since the $a_j$ are distinct zeros of $Q$, $H$ is a polynomial. As $Q(b)=0$ and $b\neq a_j$ for every $j$, $H(b)=0$. As $H$ is univalent, $H'(b)\neq0$, so $N\neq0$. Since $\varphi$ is a conformal self-map of $\D$, $W$ is univalent in $\D$, with $W(0)=H(b)/N=0$ and $W'(0)=H'(b)\varphi'(0)/N=1$; so $W\in\cS$. Each $B_{a_j}\circ\varphi$ is a conformal automorphism of $\D$, hence of the form $\lambda B_\gamma$ with $|\lambda|=1$ and $\gamma\in\D$; so $B$ is a finite Blaschke product of degree $k$. Moreover $\eta\neq0$, since $b\neq a_j$, and $B(0)=(|\eta|/\eta)\,\eta=|\eta|>0$. Since $H\prod_jB_{a_j}=Q$, we have $WB=(|\eta|/(\eta N))\,Q\circ\varphi$, so \[ (WB)'=\frac{|\eta|}{\eta N}\,Q'(\varphi)\,\varphi', \] which has no zero in $\D$, because $\varphi(\D)=\D$, $Q'$ has no zero in $\D$ and $\varphi'$ has no zero at all. Finally $1/B(0)^2=1/|\eta|^2=\prod_j1/|B_{a_j}(b)|^2=\prod_jJ(a_j,b)$. \end{proof} \section{Reduction to finite checks}\label{sec:certificate} Lemma~\ref{lem:kzero} needs two facts that are not finite checks as they stand: that $H$ is univalent in $\D$, and that $Q'$ has no zero in $\D$. This section reduces both to finitely many exact computations. \subsection*{Univalence} Let $H(z)=\sum_{\ell=0}^nh_\ell z^\ell$ be a polynomial. The \emph{Dieudonn\'e polynomials} of $H$ are \[ P_c(w)=\sum_{\ell=1}^nh_\ell\,U_{\ell-1}(c)\,w^{\ell-1}\qquad(c\in[-1,1]), \] where $U_{\ell-1}$ is the Chebyshev polynomial of the second kind, $U_{\ell-1}(\cos\theta)=\sin\ell\theta/\sin\theta$. For $c=\cos\theta$ they satisfy $H(ze^{i\theta})-H(ze^{-i\theta})=2i\sin\theta\,zP_c(z)$; moreover $P_1=H'$, since $U_{\ell-1}(1)=\ell$, and $P_c(0)=h_1$. Since $U_{\ell-1}(-c)=(-1)^{\ell-1}U_{\ell-1}(c)$, also $P_{-c}(w)=P_c(-w)$; in particular $P_{-1}(w)=H'(-w)$. So if $-1|e_n|$, then $f$ and $Tf$ have the same zeros on the circle, and if $f$ has none there, the same number of zeros in $\D$. Consequently, if $f_0=f$, $f_j=Tf_{j-1}$ (with $f_{j-1}$ at formal degree $n-j+1$), and the constant terms $\delta_j$ of $f_j$ $(1\le j\le n)$ are all positive, then $f$ has no zero in $\overline\D$. \end{lemma} \begin{proof} On the circle $|f^*|=|f|$. If $f(w)=0$ there, then $f^*(w)=0$ and $Tf(w)=0$; if $Tf(w)=0$ there, then $|e_0|\,|f(w)|=|e_n|\,|f(w)|$, so $f(w)=0$. If $f$ has no zero on the circle, then $|e_nf^*|<|\bar e_0f|$ there, and Rouch\'e's theorem gives the same number of zeros in $\D$ for $\bar e_0f$ and $Tf$. For the last claim, let $1\le j\le n$. The constant term $\delta_j$ of $f_j=Tf_{j-1}$ is $|u_0|^2-|u_{n-j+1}|^2$, where $u_0$ and $u_{n-j+1}$ are the constant and the top coefficient of $f_{j-1}$, of formal degree $n-j+1$. So $\delta_j>0$ is the hypothesis of the first claim for $f_{j-1}$. Now $f_n=\delta_n$ is a nonzero constant, so it has no zeros; going back from $j=n$ to $j=1$, each $f_{j-1}$ has no zero on the circle and none in $\D$. \end{proof} \subsection*{The four checks} \begin{lemma}\label{lem:certify} Let $k\ge1$, let $Q$ be a polynomial of degree $n\ge2$, let $b,a_1,\dots,a_k\in\mathbb C$, and let $H(z)=Q(z)\prod_{j=1}^k(1-\bar a_jz)/(z-a_j)$. Suppose: \begin{enumerate} \item[(D)] $|b|,|a_1|,\dots,|a_k|<1$, the points $b,a_1,\dots,a_k$ are pairwise distinct, and $Q(b)=Q(a_1)=\dots=Q(a_k)=0$. \end{enumerate} By (D), $H$ is a polynomial of degree at most $n$; let $P_c$ be its Dieudonn\'e polynomials. Suppose further: \begin{enumerate} \item[(C)] $Q'=ZV$, where $V$ is a polynomial without zeros in $\overline\D$ and $Z$ is a nonzero constant times $\prod_\nu(z-\zeta_\nu)^{\mu_\nu}$ (possibly an empty product), with all $|\zeta_\nu|=1$ and all $\mu_\nu$ positive integers; \item[(R)] $\operatorname{Res}_w(P_c,P_c^*)\neq0$ for every $c\in[-1,1]$, where $P_c^*(w)=\sum_{\ell=1}^n\bar h_\ell\,U_{\ell-1}(c)\,w^{n-\ell}$ (for real $c$ this is $(P_c)^*$, with $P_c$ taken at formal degree $n-1$), and $\operatorname{Res}_w(P_c,P_c^*)$ is the determinant of the $(2n-2)\times(2n-2)$ Sylvester matrix of $P_c$ and $P_c^*$, both taken at formal degree $n-1$; \item[(S)] $H'$ has no zero in $\overline\D$. \end{enumerate} Then the pair $(W,B)$ of Lemma~\ref{lem:kzero} is admissible, $\deg B=k$, and $1/B(0)^2=\prod_{j=1}^kJ(a_j,b)$. Hence $K^*\ge\prod_{j=1}^kJ(a_j,b)^{1/2}$. \end{lemma} \begin{proof} Each $P_c$ has formal degree $n-1$. Let $c\in[-1,1]$ and suppose that $P_c(w_0)=0$ for some $w_0$ with $|w_0|=1$. Since $1/\bar w_0=w_0$, we get $P_c^*(w_0)=w_0^{n-1}\overline{P_c(w_0)}=0$, so $w_0$ is a common zero of $P_c$ and $P_c^*$, and the resultant vanishes at $c$ (a common zero makes the Sylvester matrix singular, at any formal degrees). This contradicts (R). So no $P_c$ with $c\in[-1,1]$ has a zero on the circle, and by (S) and Lemma~\ref{lem:dieudonne}, $H$ is univalent in $\D$. By (C), $Q'$ has no zero in $\D$. So Lemma~\ref{lem:kzero} applies, and Theorem~\ref{thm:JN} gives $K^*\ge1/B(0)$. \end{proof} The labels (D), (C), (R), (S) stand for the data, the critical points of $Q$, the resultant, and the Schur--Cohn test for $H'$. Since the $h_\ell$ are fixed and each $U_{\ell-1}$ is a polynomial, the formulas for $P_c$ and $P_c^*$ make sense for every $c$, and $\operatorname{Res}_w(P_c,P_c^*)$ is a polynomial in $c$, so (R) is a statement about one polynomial in one real variable. In (C) and (S) the absence of zeros in $\overline\D$ is checked with Lemma~\ref{lem:SC}, applied to $V$ and to $H'$. Lemma~\ref{lem:SC} can only show that a polynomial has no zero in the closed disk, while the $Q'$ of Section~\ref{sec:pair} has a zero on the circle, at $z=1$; this is why (C) splits off the factor $Z$. \section{Proof of Theorem~\ref{thm:intro}}\label{sec:pair} The polynomial $Q$ of our pair has degree $18$, and we describe it through its critical points. Fifteen of its seventeen critical points are prescribed: $z=1$, with multiplicity $5$, and ten Gaussian rationals $\rho_j$; the other two, the zeros of a quadratic $G$, are then fixed by requiring that $Q$ vanish at $a_1$ and $a_2$ as well as at $b$. The numbers $b$, $a_1$, $a_2$, $\rho_1,\dots,\rho_{10}$ below are Gaussian rationals whose denominators are powers of $2$; $G$, $Q$ and $H$ are determined by them exactly. These thirteen numbers were found by a numerical search that made $1/B(0)$ large (see Remark~\ref{rem:margins}), with the degree $18$ and the critical point of order $5$ at $z=1$ held fixed, and were then rounded; the proof uses only the printed numbers. Let \[ b=-\tfrac{3238273}{16777216}+\tfrac{6869081}{8388608}\,i,\qquad a_1=-\tfrac{4425427}{16777216}-\tfrac{256269}{2097152}\,i,\qquad a_2=\tfrac{2126359}{8388608}-\tfrac{6838355}{8388608}\,i, \] and let $\rho_1,\dots,\rho_{10}$ be the Gaussian rationals \begin{align*} \rho_1 &= \tfrac{524767}{524288}+\tfrac{3303}{1048576}\,i, & \rho_2 &= \tfrac{262319}{262144}+\tfrac{3785}{1048576}\,i, & \rho_3 &= \tfrac{510667}{1048576}+\tfrac{596603}{524288}\,i,\\ \rho_4 &= \tfrac{140827}{1048576}+\tfrac{1177373}{1048576}\,i, & \rho_5 &= -\tfrac{20639}{32768}+\tfrac{439225}{524288}\,i, & \rho_6 &= -\tfrac{105435}{131072}-\tfrac{652651}{1048576}\,i,\\ \rho_7 &= -\tfrac{291711}{524288}-\tfrac{113639}{131072}\,i, & \rho_8 &= -\tfrac{96673}{524288}-\tfrac{1084035}{1048576}\,i, & \rho_9 &= \tfrac{524719}{524288}-\tfrac{3195}{262144}\,i,\\ \rho_{10} &= \tfrac{262337}{262144}-\tfrac{4087}{1048576}\,i . \end{align*} Put $L(t)=(t-1)^5\prod_{j=1}^{10}(t-\rho_j)$. There is a unique pair $(g_0,g_1)$ of Gaussian rationals such that the quadratic $G(t)=t^2+g_1t+g_0$ satisfies \[ \int_b^{a_1}G(t)L(t)\,dt=\int_b^{a_2}G(t)L(t)\,dt=0. \] This is a linear system in $g_0,g_1$ with nonzero determinant; the real and imaginary parts of $g_0$ and $g_1$ have denominators of $451$ to $458$ digits. Define \[ Q(z)=18\int_b^zG(t)L(t)\,dt,\qquad\text{so that}\qquad Q'(z)=18\,(z-1)^5\,G(z)\prod_{j=1}^{10}(z-\rho_j). \] Since $GL$ is monic of degree $17$, $Q$ is a monic polynomial of degree $18$; $Q(b)=0$ by definition, and the two conditions on $G$ say exactly that $Q(a_1)=Q(a_2)=0$. We put $V(z)=18\,G(z)\prod_j(z-\rho_j)$, of degree $12$, and $H(z)=Q(z)(1-\bar a_1z)(1-\bar a_2z)/((z-a_1)(z-a_2))$, a polynomial of degree $18$. Numerically the zeros of $G$ are \mbox{$1.00000688\ldots-0.00152261\ldots\,i$} and \mbox{$-0.41009053\ldots+1.04265219\ldots\,i$}. The exact coefficients of $Q$, $Q'$, $V$ and $H$ are in the repository named on the first page. Figure~\ref{fig:pair} shows the configuration: ten of the seventeen critical points of $Q$, counted with multiplicity, lie within $0.0123$ of $z=1$ (the zero of order $5$, the first zero of $G$, and $\rho_1$, $\rho_2$, $\rho_9$, $\rho_{10}$), and the other seven have moduli between $1.017$ and $1.238$. The two factors of $\Lambda=J(a_1,b)\,J(a_2,b)$ are $J(a_1,b)=1.30038\ldots$ and $J(a_2,b)=1.02761\ldots$. \begin{figure}[t] \centering \begin{tikzpicture}[scale=1.45,baseline=(current bounding box.center), zeroQ/.style={circle,fill,inner sep=1.3pt}, crit/.style={cross out,draw,thick,inner sep=1.6pt}] \draw[gray!40,thin] (-1.25,0)--(1.25,0) (0,-1.2)--(0,1.25); \draw[thick] (0,0) circle (1); \node[zeroQ,label={[label distance=-1pt]below:$b$}] at (-0.1930,0.8189) {}; \node[zeroQ,label={[label distance=-1pt]below:$a_1$}] at (-0.2638,-0.1222) {}; \node[zeroQ,label={[label distance=-1pt]above:$a_2$}] at (0.2535,-0.8152) {}; \foreach \pt in {(0.4870,1.1379),(0.1343,1.1228),(-0.6299,0.8378),(-0.8044,-0.6224), (-0.5564,-0.8670),(-0.1844,-1.0338),(-0.4101,1.0427)} \node[crit] at \pt {}; \node[crit,very thick,inner sep=3.2pt] at (1,0) {}; \node[below right] at (1.04,-0.02) {$1$}; \end{tikzpicture} \hspace{0.05\textwidth} \includegraphics[width=0.32\textwidth,valign=c]{figures/fig_image.pdf} \caption{Left: the data of this section. The dots are the zeros $b$, $a_1$, $a_2$ of $Q$ in $\D$, and the crosses are the $17$ critical points of $Q$, counted with multiplicity; none lies in $\D$. The large cross at $z=1$ stands for the ten of them within $0.0123$ of $1$, named in the text; the small crosses are the other seven. Right: the image $H(\D)=N\,W(\D)$, computed numerically and shown without its scale. The dot is $H(b)=0$, next to the tip of a narrow inlet whose two sides almost touch (Remark~\ref{rem:margins}).}\label{fig:pair} \end{figure} \begin{theorem}\label{thm:main} For these data, (D), (C) with $Z=(z-1)^5$, (R) and (S) of Lemma~\ref{lem:certify} hold, with $k=2$ and $n=18$. Hence the pair $(W,B)$ of Lemma~\ref{lem:kzero} is admissible, $\deg B=2$, and $1/B(0)^2=J(a_1,b)\,J(a_2,b)=\Lambda$, the rational number of Theorem~\ref{thm:intro}; so $K^*\ge\sqrt\Lambda>1.1559837$. \end{theorem} \begin{proof} Each of the four facts reduces to finitely many exact computations over $\mathbb Q(i)$, which we carry out by computer, from the numbers printed above, as follows. We first solve the linear system for $g_0,g_1$ and expand $Q$, $Q'$ and $H$ into exact lists of coefficients; all the checks are made on these lists. The programs and their output are in the repository named on the first page; the whole computation takes about eight minutes on one processor core. \begin{enumerate} \item[(D)] We compute $|b|^2$, $|a_1|^2$, $|a_2|^2$ exactly, compare them with $1$, and check that the three points are distinct and that $Q$ vanishes at each of them. We also check that the coefficient list of $Q'$ is that of the derivative of $Q$, and that $H(z)(z-a_1)(z-a_2)=Q(z)(1-\bar a_1z)(1-\bar a_2z)$. \item[(C)] We divide $Q'$ by $(z-1)^5$ exactly, with remainder $0$, and apply Lemma~\ref{lem:SC} to the quotient $V$: the $12$ numbers $\delta_j$ are positive. \item[(R)] After multiplying $H$ by a positive integer, so that its coefficients are Gaussian integers (this multiplies the resultant by a positive constant), we compute $F(c)=\operatorname{Res}_w(P_c,P_c^*)$ as an exact polynomial in $c$. The resultant is the determinant of a $34\times34$ Sylvester matrix whose entries are polynomials in $c$ of degree at most $17$, so $F$ has degree at most $578$, and its values at $579$ points determine it. We compute the determinant at the $581$ integer points $c=0,1,\dots,580$, where the entries are Gaussian integers since each $U_{\ell-1}$ has integer coefficients. We work modulo the $1128$ largest primes $r\equiv1\pmod4$ below $2^{62}$, mapping $i$ to each of the two square roots of $-1$ modulo $r$ (the two images give the real and imaginary parts modulo $r$), and recover the values exactly by the Chinese remainder theorem: Hadamard's inequality bounds the real and imaginary parts at every point by $2^E$ with $E=69921$, and the product of the primes exceeds $2^{E+2}$. The imaginary parts of all $581$ values are $0$; since $F$ has degree at most $578$, $F$ has real coefficients. We interpolate $F$ from its values at $579$ of the points, check the result at the other two, and find that $F$ has degree $578$. Finally $F(\pm1)\neq0$, and $F$ has no zero in $(-1,1)$: we split $[-1,1]$ by repeated bisection, checking that $F$ does not vanish at any midpoint, until on each piece $[c_0,c_1]$ the coefficients of $(1+x)^{578}F\bigl((c_0+c_1x)/(1+x)\bigr)$ have no sign change; since $x\mapsto(c_0+c_1x)/(1+x)$ maps $(0,\infty)$ onto $(c_0,c_1)$, Descartes' rule of signs shows that $F$ has no zero in $(c_0,c_1)$. For our $F$ this takes $47$ applications of Descartes' rule, $24$ of them on final subintervals. \item[(S)] We apply Lemma~\ref{lem:SC} to $H'$, of degree $17$: the $17$ numbers $\delta_j$ are positive. \end{enumerate} We also check that $J(a_1,b)\,J(a_2,b)$ equals the rational number $\Lambda$ of Theorem~\ref{thm:intro}. In exact arithmetic, $\Lambda-1.1559837^2=6.75\ldots\cdot10^{-8}>0$, so $\sqrt\Lambda>1.1559837$. Lemma~\ref{lem:certify} gives the rest. \end{proof} \begin{remark}[The margins]\label{rem:margins} The zeros of $V$, $H'$ and the $P_c$ lie outside $\overline\D$. We call the distance from the unit circle to the nearest zero of such a polynomial its \emph{margin}. Some margins are very small, which is why every step is done in exact arithmetic. They are small because the data were chosen to make $1/B(0)$ large, and, as explained before Lemma~\ref{lem:kzero}, what limits $1/B(0)$ is that these zeros must stay out of $\D$. The zero of $V$ nearest to the circle, a zero of $G$, has modulus $1.00000804\ldots$. The zero of $H'$ nearest to the circle has modulus $1.00001141\ldots$; since $P_{\pm1}(w)=H'(\pm w)$, this gives the margin at $c=\pm1$. Numerically the zeros of the $P_c$ come closest to the circle near $c=\pm0.9231$, within about $7.03\cdot10^{-6}$; see Figure~\ref{fig:margin}. A small margin has a geometric meaning. For $-11$; so when $|w|$ is close to $1$, two points of the boundary curve of $H(\D)$ nearly coincide. Numerically, at the dips of Figure~\ref{fig:margin} this happens along the narrow inlet of Figure~\ref{fig:pair}, whose two sides almost touch. \end{remark} \begin{figure}[ht] \centering \includegraphics[width=0.86\textwidth]{figures/fig_margin.pdf} \caption{The margin of $P_c$, that is, the distance from the unit circle to the nearest zero of $P_c$ (Remark~\ref{rem:margins}), computed numerically for $0\le c\le1$ and drawn on a logarithmic scale. Since $P_{-c}(w)=P_c(-w)$, the curve for $-1\le c\le0$ is the mirror image of this one. Check (R) proves that the curve never reaches $0$. Its deep dips are the places where zeros of $P_c$ are pushed against the circle.}\label{fig:margin} \end{figure} The degree statement of Theorem~\ref{thm:intro} rests on the monotonicity of $K(d)$, which is due to Crane~\cite{Crane2006} (see also~\cite[proof of Cor.~4.6]{JatarNg2026b}); we include the short proof. \begin{lemma}[Crane]\label{lem:mono} $K(d+1)\ge K(d)$ for every $d\ge2$. \end{lemma} \begin{proof} Let $p\in\mathcal P_d$, and for $\varepsilon\neq0$ put $p_\varepsilon(z)=p(z)+\varepsilon z^{d+1}$, which lies in $\mathcal P_{d+1}$. As $\varepsilon\to0$, $d-1$ of the $d$ critical points of $p_\varepsilon$, counted with multiplicity, tend to those of $p$, and the remaining one, $\beta_\varepsilon$, tends to $\infty$. The first claim follows from Hurwitz's theorem, as $p_\varepsilon'\to p'$ locally uniformly; the second because the product of the $d$ critical points of $p_\varepsilon$ has modulus $1/((d+1)|\varepsilon|)\to\infty$, as $p_\varepsilon'(0)=1$, while the other $d-1$ stay bounded. Since $p_\varepsilon'(\beta_\varepsilon)=0$ gives $\varepsilon\beta_\varepsilon^d=-p'(\beta_\varepsilon)/(d+1)$, we have \[ \frac{p_\varepsilon(\beta_\varepsilon)}{\beta_\varepsilon}=\frac{p(\beta_\varepsilon)}{\beta_\varepsilon} -\frac{p'(\beta_\varepsilon)}{d+1}, \] and if $\alpha$ is the leading coefficient of $p$, the right side is $\alpha\beta_\varepsilon^{d-1}/(d+1)+O(\beta_\varepsilon^{d-2})$, which tends to $\infty$ in modulus, since $d\ge2$. As the critical points of $p$ are nonzero, it follows that $m(p_\varepsilon)\to m(p)$. Hence $K(d+1)\ge m(p)$ for every $p\in\mathcal P_d$, and $K(d+1)\ge K(d)$. \end{proof} \begin{corollary}\label{cor:Kd} $K(d)>1.1559837$ for all sufficiently large $d$. \end{corollary} \begin{proof} Let $A=1.1559837$. By Theorem~\ref{thm:main}, $AA$ for some $d_0$. By Lemma~\ref{lem:mono}, $K(d)>A$ for every $d\ge d_0$. \end{proof} The proof gives no explicit value of $d_0$, since Theorem~\ref{thm:JN} does not bound the degree of the polynomial it gives. Theorem~\ref{thm:main} and Corollary~\ref{cor:Kd} prove Theorem~\ref{thm:intro}. \section*{Acknowledgments} The author is immensely grateful to Edward Crane for mentorship, and for feedback and suggestions that greatly improved this work and its exposition. {\raggedright \begin{thebibliography}{99} \bibitem{LeanMVP2026} T.~Adamczewski, Smale's mean value conjecture ($K = 1$): disproof, GitHub repository, \url{https://github.com/tadamcz/mean-value-problem}, 2026. \bibitem{AdamczewskiColbrook2026} T.~Adamczewski and M.~J.~Colbrook, From boundary geometry to counterexamples in Smale's mean value problem, arXiv:2610.36158v1, 2026. \bibitem{BeardonMindaNg2002} A.~F.~Beardon, D.~Minda and T.~W.~Ng, Smale's mean value conjecture and the hyperbolic metric, \emph{Math. Ann.} \textbf{322} (2002), 623--632. \bibitem{ConteFujikawaLakic2007} A.~Conte, E.~Fujikawa and N.~Lakic, Smale's mean value conjecture and the coefficients of univalent functions, \emph{Proc. Amer. Math. Soc.} \textbf{135} (2007), no.~10, 3295--3300. \bibitem{Crane2006} E.~Crane, Extremal polynomials in Smale's mean value conjecture, \emph{Comput. Methods Funct. Theory} \textbf{6} (2006), no.~1, 145--163. \bibitem{Crane2007} E.~Crane, A bound for Smale's mean value conjecture for complex polynomials, \emph{Bull. Lond. Math. Soc.} \textbf{39} (2007), no.~5, 781--791. \bibitem{Dieudonne1931} J.~Dieudonn\'e, Recherches sur quelques probl\`emes relatifs aux polyn\^omes et aux fonctions born\'ees d'une variable complexe, \emph{Ann. Sci. \'Ecole Norm. Sup. (3)} \textbf{48} (1931), 247--358. \bibitem{FujikawaSugawa2006} E.~Fujikawa and T.~Sugawa, Geometric function theory and Smale's mean value conjecture, \emph{Proc. Japan Acad. Ser. A Math. Sci.} \textbf{82} (2006), no.~7, 97--100. \bibitem{GoelLong} D.~Goel, Smale's mean value constant (1981) exceeds 1.1559, and other miscellanea, Zenodo, 2026, \url{https://doi.org/10.5281/zenodo.23597020}. \bibitem{JatarNg2026b} A.~Jatar and T.~W.~Ng, Smale's mean value constant and admissible univalent Blaschke pairs, arXiv:2610.21472v2, 2026. \bibitem{Marden} M.~Marden, \emph{Geometry of Polynomials}, 2nd ed., Math. Surveys 3, Amer. Math. Soc., Providence, RI, 1966. \bibitem{RahmanSchmeisser2002} Q.~I.~Rahman and G.~Schmeisser, \emph{Analytic Theory of Polynomials}, London Math. Soc. Monographs (N.S.) 26, Oxford Univ. Press, 2002. \bibitem{Smale1981} S.~Smale, The fundamental theorem of algebra and complexity theory, \emph{Bull. Amer. Math. Soc. (N.S.)} \textbf{4} (1981), 1--36. \bibitem{Smale2000} S.~Smale, Mathematical problems for the next century, in \emph{Mathematics: Frontiers and Perspectives} (V.~Arnold, M.~Atiyah, P.~Lax and B.~Mazur, eds.), Amer. Math. Soc., Providence, RI, 2000, 271--294. \bibitem{Tischler1989} D.~Tischler, Critical points and values of complex polynomials, \emph{J. Complexity} \textbf{5} (1989), no.~4, 438--456. \end{thebibliography} } \end{document}