An inequality for circle packings proved by semidefinite programming (Q701787)

The following inequality, used in the theory of circle packings, is proved. Consider a triangle with sides of lengths \(a,b,c\), a second triangle with sides of lengths \(x,y,z\), and a third triangle with sides of lengths \(a+x,b+y,c+z\). Let \(\alpha, \beta, \gamma\) be the angles opposite the sides of length \(c,z,c+z\), respectively. Then \(\alpha(a+b-c)+\beta(x+y-z)\leq\gamma(a+x+b+y-c-z)\). This is equivalent to the nonnegativity of a certain polynomial of degree \(20\) in four real variables. The proof uses semidefinite programming to find a representation of the polynomial as a sum of squares. In order to make the problem algorithmically feasible, the sparsity and the symmetry of \(P\) are exploited. Although floating point arithmetic was used, the solution is easily verifiable once obtained using only integer arithmetic.