Exact verification of eleven-term Vasc inequality using finite certificates
A Finite Certificate for the Positive $n=11$ Vasc Inequality
Symbolic Computation
Summary
The paper deals with a complicated inequality involving eleven positive numbers, known as the Vasc cyclic inequality. The authors prove this inequality always holds by breaking it down into millions of smaller polynomial problems and then rigorously checking each one using exact mathematical tools. They create special certificates—mathematical proofs that are easy to verify—to cover all tricky cases. This method ensures the inequality is true for all positive eleven-tuples by combining detailed math with computer-aided exact checks.
What this means in practice
- •For mathematicians working in inequalities: Provide a verified exact method to prove complex cyclic inequalities involving multiple variables using finite certificates and polynomial decomposition.
- •For computer algebra system developers: Inspire development of algorithms for rigorous polynomial inequality verification with exact integer certificate generation and validation.
A theory result. No direct application yet.
Authors
Tiancheng Xu, Wensheng Yu
Abstract
We establish the Vasc cyclic inequality for all strictly positive real eleven-tuples by a finite exact certificate. Cyclic rotation places a minimum at the first position, and rank words together with cumulative gaps reduce the problem to $10!=3{,}628{,}800$ homogeneous integer polynomials of degree eleven. Independent coefficient reconstruction proves $3{,}358{,}617$ roots directly. The remaining $270{,}183$ roots are covered by $267{,}952$ ordinary midpoint certificates, $2{,}195$ complete binary subdivision certificates, and $36$ complete certificates containing partial sorting nodes. Each nontrivial leaf is checked by subtracting weighted AM-GM midpoint circuits from a positive multiple of the transformed polynomial and verifying every residual coefficient. Explicit word-set comparisons certify disjointness and exact coverage. We prove the soundness of the leaves and both subdivision rules, then recover the rational inequality by positive denominator clearing and continuity. The resulting proof combines explicit mathematical reductions with independently checked exact integer certificates.