From $\log 2$ to $\pi /2$: the sharp asymptotic inradius of polynomial lemniscates

Abstract

Let $R_n$ be the infimum of the inradii of $\{z:|p(z)|<1\}$ over monic degree-$n$ polynomials whose zeros lie in the closed unit disk. We prove $n{R}_n\to \pi /2$, matching the asymptotic obstruction supplied by $z^n-1$. We first establish the exact universal radius $2^{1/n}-1$ for disks centered at zeros, which recovers the $(\log 2)/n$ bound. Small inradius then forces radial concentration of the zeros and decay of their low reciprocal moments. These estimates give an entire limit with a modulus reflection identity; a second rescaling produces an exponential tangent and strict sublevel disks of every radius below $\pi /2$. The proof is accompanied by a Lean~4 formalization and a step-by-step source index.

17 pages, 3 figures