证明了9元Vasc不等式在正实数下的成立，具可验证的有限证书。
A Finite Certificate for the Positive $n=9$ Vasc Inequality
- 通过变量排序和累积差分参数化，将不等式转化为多项式形式。
- 构造了包含36,815个系数叶的验证证书，覆盖全部40,320种排序情况。
- 结合人类引导与AI生成，适合对不等式证明与自动化验证感兴趣者。
本文证明了Vasc循环不等式在n=9且变量为正实数时的成立性。人类主导的数学简化将原有理不等式转化为齐次多项式不等式，并固定循环最大值，利用累积间隙参数化每种排序的最大值锥体。完整的验证证书涵盖全部8! = 40,320种排序锥体。该证书由机械数学智能体团队通过Python工具链自动生成，包括分支策略、验证程序及终端分类。证书包含36,815个系数叶、2,236个普通Polya乘子叶和1,269个AM-GM中点叠加叶。所有数学推导与验证逻辑经人类作者审核，相关代码、独立验证器及源码重建路径均以附加资源形式发布。
原文摘要 · Abstract (English)
We prove the positive-real $n=9$ case of the Vasc cyclic inequality. The proof was obtained with human-guided assistance from the AI agent MechMath Agent Team: the human-readable part reduces the rational inequality to a homogeneous polynomial inequality, fixes a cyclic maximum, and parametrizes each sorted fixed-maximum cone by cumulative gaps; the finite part is a certificate covering all $8!=40320$ sorted cones. MechMath Agent Team generated the certificate verification workflow through Python tool calls, including the case split, verification programs, and terminal classifications. The published certificate has $36815$ coefficient leaves, $2236$ ordinary Polya multiplier leaves, and $1269$ AM-GM midpoint overlay leaves. Human authors audited the mathematical reductions and verification logic, and a separate artifact contains the certificate, an independent verifier, and a from-source rebuild route.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。