从 $\log 2$ 到 $\pi/2$：多项式叶形线的尖锐渐近内半径
From $\log 2$ to $π/2$: the sharp asymptotic inradius of polynomial lemniscates
- gxu.edu.cn（广西大学）
机构由 AI 辅助整理，请以论文原文为准。
中文总结 AI 辅助
本文证明首一多项式叶形线内半径下确界满足 $nR_n\to\pi/2$，通过精确半径 $2^{1/n}-1$ 及零点集中估计实现，并附 Lean 4 形式化验证。
中文摘要 AI 辅助
设 $R_n$ 为所有零点位于闭单位圆盘内的首一 $n$ 次多项式所对应的集合 $\{z:|p(z)|<1\}$ 的内半径的下确界。我们证明 $nR_n\to\pi/2$，与 $z^n-1$ 所提供的渐近障碍相匹配。我们首先建立以零点为圆心的圆盘的精确通用半径 $2^{1/n}-1$，这恢复了 $(\log 2)/n$ 的界。小的内半径随后迫使零点产生径向集中，并使其低阶倒数矩衰减。这些估计给出一个具有模反射恒等式的整体极限；第二次重标度产生指数切线以及半径严格小于 $\pi/2$ 的每个半径的严格子水平圆盘。该证明附有 Lean 4 形式化验证和逐步源码索引。
英文摘要
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 $nR_n\toπ/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 $(\log2)/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 $π/2$. The proof is accompanied by a Lean~4 formalization and a step-by-step source index.
