A Finite Certificate for the Positive $n=9$ Vasc Inequality

技術要約：正の $n = 9$ Vasc 不等式に対する有限証明書

問題提起
本論文は、正の実数における $n=9$ の Vasc 循環不等式の正のケースを扱う。Vasc の式は、$C_n(x_1, \dots, x_n) = \sum_{i=1}^n \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}}$ （添字は循環的）と定義される。この $C_n \ge 0$ という予想は、$n=3,4,5,7$ では証明されているが、$n=6, 13$（およびその結果としてすべての偶数 $n \ge 6$ と奇数 $n \ge 13$）では反証されている。一方で、$n=9$ および $n=11$ のケースは未解決のままであった。特に $n=9$ のケースは、従来の逐次差分置換（Successive Difference Substitution; SDS）手法が $8! = 40,320$ 個の異なる順序領域の解析を必要とする組合せ爆発に直面する、極めて重要な境界線となっている。

手法
証明戦略は、人間が検証可能な代数的簡約と、有限の機械生成証明書を分離することである。ワークフローは以下の5つの段階で進行する：

1. 分母の消去： 有理不等式に対し、すべての分母の正の積 $D_9(x) = \prod (x_{i+1} + x_{i+2})$ を掛けることで、同次多項式不等式 $P_9(x) \ge 0$ へと変換する。
2. 循環最大値による簡約： 循環不変性を利用し、検証領域を最初の座標が最大値となるタプル（すべての $i$ に対して $x_1 \ge x_i$）に制限する。
3. ソートされた錐（Cone）によるパラメータ化： 固定された最大値の錐内において、残りの8つの変数をすべての置換（$\sigma \in S_8$）に従ってソートする。これにより、40,320個の「ソートされた錐」が作成される。
4. ギャップ座標変換： 各ソートされた錐を、累積ギャップ座標（$y_1, \dots, y_9$）を用いてパラメータ化する。ここで $y_i \ge 0$ は、隣接するソートされた変数間の差を表す。これにより、問題は正の総ギャップを持つ非負直交領域へと写像される。
5. 有限証明書の検証： 40,320個の各ソートされた錐に対して、特定の「終端行（terminal row）」が生成される。各錐における不等式の妥当性は、以下の3つの健全性メカニズムのいずれかを検証することで確立される：
   • 係数の非負性： ギャップ座標における多項式のすべての係数が非負であること。
   • Polya 乗数： 多項式に正の因子（Polya 乗数）を掛け、係数がすべて非負となる多項式を得ること。
   • AM-GM 中点オーバーレイ： 相加相乗平均（AM-GM）回路のオーバーレイを介して多項式を検証すること。

主要な貢献と実行
主な貢献は、$n=9$ の全正の実数空間をカバーする有限の厳密な証明書の生成と検証である。

• AI-人間協調： 証明は、LLM駆動のエージェントである MechMath Agent Team による人間の誘導付き支援によって得られた。エージェントは、Python 検証プログラムの記述、ケース分割、および終端分類の整理を含む、証明書検証フェーズを自律的に実行した。
• 証明書の規模： 公開される証明書には、36,815 個の係数リーフ、2,236 個の通常の Polya 乗数リーフ、および 1,269 個の AM-GM 中点オーバーレイリーフが含まれる。
• 検証の厳密性： 著者らは、この証明書が単なる計算の記録ではなく、形式的なアーティファクトであることを強調している。これには、固定最大値のストリーム、多項式のハッシュ、および残留チェックを、保存されたデータから直接再計算する独立した検証器（Python の標準ライブラリのみを使用）が含まれており、証明書を生成したコードからの隔離を保証している。

結果
本論文は、定理 1 を成功裏に証明した：任意の正の実数 $x_1, \dots, x_9$ に対して、不等式 $\sum_{i=1}^9 \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}} \ge 0$ が成立する。

• 本研究は、Vasc 不等式のステータステーブル（表1）における最初の未解決項目を解決した。
• $n=11$ のケースは依然として未解決であり、現在は小さな錐に関する部分的な正の結果のみが得られている。

意義
本論文は、組合せ的な複雑さによって阻まれていた自動不等式証明における長年の未解決問題を解決したことを主張している。有限の証明書が、4万件以上の領域の解析を必要とする問題に対して、どのように生成され、独立して検証され得るかを示すことで、本研究は、AI エージェントが計算上の重作業（ケース分割、プログラム生成、および検証）を担い、人間の著者が数学的な簡約と検証ロジックを監査するというハイブリッドなアプローチの有効性を実証した。本研究は、証明書、独立した検証器、およびソースの再構築パスを含む再現可能なルートを提供しており、$n=9$ の Vasc 不等式に関する新たなベンチマークを確立している。