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

技术摘要：正数 $n = 9$ Vasc 不等式的有限证书

问题陈述
本文解决了 Vasc 循环不等式中 $n=9$ 的正实数情况。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$ 的情况代表了一个关键的前沿，因为之前的连续差分代换（SDS）方法在此遇到了组合爆炸，需要分析 $8! = 40,320$ 个不同的排序区域。

方法论
证明策略将人类可验证的代数约化与机器生成的有限证书解耦。工作流程分为五个阶段：

1. 分母消除：通过乘以所有分母的正乘积 $D_9(x) = \prod (x_{i+1} + x_{i+2})$，将有理不等式转换为齐次多项式不等式 $P_9(x) \ge 0$。
2. 循环最大值约化：利用循环不变性，将验证域限制在第一个坐标为最大值的元组中（即对于所有 $i$，满足 $x_1 \ge x_i$）。
3. 排序锥参数化：在固定的最大值锥内，根据所有可能的排列（$\sigma \in S_8$）对剩余的八个变量进行排序。这创建了 $40,320$ 个“排序锥”。
4. 间隙坐标变换：每个排序锥使用累积间隙坐标（$y_1, \dots, y_9$）进行参数化，其中 $y_i \ge 0$ 表示相邻排序变量之间的差值。这把问题映射到了一个具有正总间隙的非负象限。
5. 有限证书验证：针对每个 40,320 个排序锥，生成一个特定的“终端行”。通过验证以下三种健全性机制之一，来确立不等式在每个锥体上的有效性：
   • 系数非负性：间隙坐标下的多项式所有系数均为非负。
   • Polya 乘子：将多项式乘以一个正因子（Polya 乘子），使其变为一个具有非负系数的多项式。
   • AM-GM 中点覆盖：通过算术平均-几何平均（AM-GM）电路覆盖来验证多项式。

核心贡献与执行
主要贡献是生成并验证了一个有限精确证书，该证书覆盖了 $n=9$ 的整个正实数空间。

• AI-人类协作：证明过程是在 MechMath Agent Team（一个由 LLM 驱动的智能体）的人类引导协助下完成的。该智能体自主执行了证书验证阶段，包括编写 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$ 的情况仍然开放，目前仅在小规模锥体上取得了部分正向结果。

意义
该论文声称其意义在于解决了一个此前因组合复杂度而被阻断的长期开放的自动不等式证明问题。通过展示一个有限证书可以被生成并独立验证，且该证书能够处理需要分析超过 40,000 个区域的问题，这项工作验证了一种混合方法，即由 AI 智能体处理计算密集型任务（案例拆分、程序生成和验证），而人类作者负责审计数学约化和验证逻辑。该工作提供了一条可复现的路径，包括证书、独立的验证器以及源码构建路径，为 $n=9$ 的 Vasc 不等式建立了新的基准。