Exact rational certificates and a Lean formalization of the eleven-variable Vasc inequality

Abstract

We prove that the cyclic sum $\sum_{i=0}^{10}(x_i-x_{i+1})/(x_{i+1}+x_{i+2})$ is nonnegative for every strictly positive real eleven-tuple, with indices taken modulo eleven. Clearing denominators reduces the problem to a homogeneous polynomial. Subtracting the smallest coordinate then separates the proof into nonnegativity of a common-translation derivative and nonnegativity on a full boundary face. We supply exact rational polynomial certificates in Gram-matrix form for both statements. The derivative certificate uses a linear multiplier, centered monomials and cyclic averaging; the boundary certificate uses a strictly positive quadratic multiplier and uncentered monomials. Their verification requires 6,069 cyclic coefficient comparisons and 34,304 literal coefficient comparisons. All 606 certificate matrices are certified by integer congruences with strictly diagonally dominant images. A Lean 4 development formally verifies the certificate checks and their connection to the original inequality. The exact certificate data, replay programs, and formal sources are publicly available.