A counterexample to the complex polynomial Koebe radius conjecture

技术摘要：复系数多项式柯贝半径猜想的反例

问题陈述
本文旨在解决对于归一化为 $f(z) = z + \sum_{j=2}^N a_j z^j$ 的单变函数（全纯且单射）多项式类 $\mathcal{F}$ 的柯贝半径 $\rho(\mathcal{F})$ 的确定问题。柯贝半径定义为所有满足 $f \in \mathcal{F}$ 的函数 $f$ 的像 $f(D)$ 中包含圆盘 $D_r$ 的最大半径 $r$ 的上确界。

2018年，Dmitrishin、Smorodin 和 Stokolos 猜想，对于实系数多项式类 ($\mathcal{U}_{N,\mathbb{R}}$) 和复系数多项式类 ($\mathcal{U}_N$)，其柯贝半径均由以下公式给出：
$$\rho(\mathcal{U}_N) = \rho(\mathcal{U}_{N,\mathbb{R}}) = \frac{1}{4 \cos^2(\pi/(N + 2))}$$
虽然实系数三次情形 ($N=3$) 已被证明满足该公式，其半径为 $(3-\sqrt{5})/2 \approx 0.381966$，但复系数情形仍是一个开放的猜想。本文旨在通过构造一个特定的复三次多项式来违背该猜想，从而证明等式 $\rho(\mathcal{U}_3) = \rho(\mathcal{U}_{3,\mathbb{R}})$ 不成立。

方法论
作者采用了一种结合严谨解析验证与形式化证明的构造性方法：

1. 反例构造： 作者定义了一个具有有理系数的特定归一化三次多项式：
   $$p(z) = z + \left( \frac{9}{10} + i\frac{1}{60} \right)z^2 + \frac{2}{7}z^3$$
2. 单变性验证： 为了证明 $p(z)$ 在圆盘 $D_R$（其中 $R = 1001/1000$）上是单变的，本文利用了经典的 Brannan 机制。这包括：
   • 将单射条件简化为“二次零点排除”问题。
   • 定义一系列二次多项式 $q_x(w) = 1 + 2axw + b(4x^2-1)w^2$，并证明对于所有的 $x \in [0,1]$，它们在 $|w| \le R$ 内没有零点。
   • 应用引理（Lemma 2.1），该引理指出如果 $|A - cA| < 1 - c^2$，则二次多项式 $1 + Aw + cw^2$ 在单位圆盘内没有零点。
3. 精确有理认证： 零点排除条件的验证依赖于精确算术而非浮点近似。作者将相关的不等式条件表示为一个多项式 $H(y)$，并使用 Bernstein 系数 证明了 $H(y)$ 在 $[0,1]$ 上大于 0。
   • 通过对区间 $[0,1]$ 进行细分，计算出 $H(y)$ 的 Bernstein 系数的精确有理下界。
   • 由于 Bernstein 基函数是非负且和为 1 的，因此系数的正下界保证了函数的正定性。
4. 形式化验证： 整个证明过程，包括多项式的定义、在扩大圆盘上的单变性以及严格边界的验证，均使用 Lean 4 定理证明器（版本 4.34.1）及其 mathlib 库进行了验证。该证明仅依赖于标准公理（propext, Classical.choice, Quot.sound），不依赖任何未经证实的假设。
5. 遗漏值计算： 作者确定了单位圆盘边界上的一个特定点 $\zeta = (-24 + 7i)/25$（满足 $|\zeta|=1$）。他们计算了其像 $w_0 = p(\zeta)$，并证明 $|w_0|$ 严格小于所猜想的半径。

关键结果

• 对猜想的驳斥： 多项式 $p(z)$ 在 $D_{1001/1000}$ 上是单射的，这意味着它在闭单位圆盘上是单变的。然而，单位圆盘在 $p$ 下的像遗漏了点 $w_0$，其中：
  $$|w_0| = \sqrt{\frac{641029}{4410000}} \approx 0.3812585$$
• 半径的严格分离： 计算出的遗漏模度满足：
  $$|w_0| < \frac{763}{2000} < \frac{3-\sqrt{5}}{2}$$
  这确立了严格不等式：
  $$\rho(\mathcal{U}_3) \le \sqrt{\frac{641029}{4410000}} < \rho(\mathcal{U}_{3,\mathbb{R}})$$
  因此，次数为 3 的复柯贝半径严格小于实柯贝半径，从而反驳了两者相等的猜想。
• 失效的最小次数： 本文验证了对于次数 $N=1$ 和 $N=2$，$\rho$ 是相等的（分别为 $\rho=1$ 和 $\rho=1/2$）。因此，次数 3 是该猜想失效的最小次数。

意义与主张
本文声称提供了第一个关于复多项式柯贝半径猜想在 $N=3$ 时失效的显式反例。其意义在于：

1. 驳斥复系数相等性： 它表明对于三次多项式，实系数多项式的极值行为并不能推广到复数域。
2. 建立上界： 它提供了一个具体的、严谨的复三次柯贝半径上界（$\approx 0.3812585$），将其与实系数情形（$\approx 0.3819660$）区分开来。
3. 方法论的严密性： 该工作强调了将经典复分析（Dieudonné 判别法、辐角原理）与现代形式化验证（Lean）以及精确有理算术（Bernstein 系数）相结合在解决涉及严格不等式的问题中的效用。

作者明确指出，虽然他们提供了一个上界，但并未确定复三次柯贝半径的最优（精确）值，也没有声称该猜想对于所有次数 $N > 3$ 均失效。该结果是针对三次情形的特定结论。