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(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))}$$
実係数の3次の場合 ($N=3$) は、この公式を満たす半径 $(3-\sqrt{5})/2 \approx 0.381966$ を持つことが証明されているが、複素数の場合は未解決の予想のまま残されていた。本論文は、特定の複素3次多項式を構成することにより、$\rho(\mathcal{U}_3) = \rho(\mathcal{U}_{3,\mathbb{R}})$ という等式を覆すことを目的としている。

手法
著者は、構成的なアプローチと厳密な解析的検証および形式的証明を組み合わせて用いている：

1. 反例の構成: 著者は、有理係数を持つ特定の正規化された3次多項式を定義する：
   $$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$ 内に零点を持たないことを証明する。
   • もし $|A - cA| < 1 - c^2$ ならば、二次式 $1 + Aw + cw^2$ は単位円内に零点を持たないという補題（補題 2.1）を適用する。
3. 厳密な有理数による証明: 零点排除条件の検証は、浮動小数点近似ではなく、厳密な有理演算に基づいて行われる。著者は、関連する不等式条件を多項式 $H(y)$ として表現し、**ベルンシュタイン係数（Bernstein coefficients）**を用いて $H(y) > 0$ が $[0,1]$ 上で成り立つことを証明する。
   • 区間 $[0,1]$ を細分化し、$H(y)$ のベルンシュタイン係数の厳密な有理数下限を計算する。
   • ベルンシュタイン基底関数は非負であり、その和は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次の複素ケーベ半径は実係数のケーベ半径よりも厳密に小さく、予想された等式 $\rho(\mathcal{U}_3) = \rho(\mathcal{U}_{3,\mathbb{R}})$ は誤りであることが示された。
• 失敗の最小次数: 本論文では、次数 $N=1$ および $N=2$ において、実および複素のケーベ半径が同一であること（$\rho=1$ および $\rho=1/2$）を検証している。したがって、次数3がこの予想が成立しない最小の次数である。

意義と主張
本論文は、3次における複素多項式ケーベ半径予想に対する最初の手続き的な反例を提供したと主張している。その意義は以下の点にある：

1. 複素等価性の反証: 実係数多項式の極限的な挙動が、3次多項式においては複素領域には拡張されないことを示している。
2. 上界の確立: 複素3次ケーベ半径の具体的な、かつ厳密な上界（$\approx 0.3812585$）を提示しており、これは実数の値（$\approx 0.3819660$）とは異なるものである。
3. 手法の厳密性: 古典的な複素解析（ディエンドリーの判定法、偏角の原理）と、現代的な形式検証（Lean）、および厳密な有理数演算（ベルンシュタイン係数）を組み合わせることで、厳密な不等式を伴う問題を解決する有用性を強調している。

著者は、上界を提示してはいるものの、複素3次ケーベ半径の最適な（正確な）値を決定したわけではなく、また、すべての次数 $N > 3$ において予想が失敗すると主張しているわけでもないことを明記している。この結果は、3次のケースに特化したものである。