I want to prove that a given set of quadratic and linear inequalities has no solution. The set size is of 13 equations, or, including the positiveness constrain, 21 equations.
I already used a python library to try to find solution, and it couldn't find one; However, this is not a proof of non-existence, since the constraints are not convex. I tried to add manually inequalities and do some multiplication in order to reach a contradiction, but couldn't. I even created a program to do it automatically (by adding positive equations together\multiply them) and the program reached hundreds of thousands of equations, but no contradiction.
By emperical tests of the original problem I want to solve, I have a strong reason to believe the set have no solution. But how can I prove it?
For the sake of completeness, I'll provide the inequalities: All the following are strictly positive:
- $-a_1*b_2 - a_1*b_3 + a_2*b_1 + a_2*b_3 + a_3*b_1 - a_3*b_2$
- $a_2*b_3 - a_3*b_2$
- $a_2*b_3 + a_2*b_4 - a_3*b_2 + a_3*b_4 - a_4*b_2 - a_4*b_3$
- $a_1*b_2 + a_1*b_4 - a_2*b_1 + a_2*b_4 - a_4*b_1 - a_4*b_2$
- $a_2*b_4 - a_4*b_2$
- $-a_2*b_3 + a_2*b_4 + a_3*b_2 + a_3*b_4 - a_4*b_2 - a_4*b_3$
- $a_1*b_2 + a_1*b_4 - a_2*b_1 - a_2*b_4 - a_4*b_1 + a_4*b_2$
- $a_1*b_3 + a_1*b_4 - a_3*b_1 - a_3*b_4 - a_4*b_1 + a_4*b_3$
- $a_1*b_4 - a_4*b_1$
- $-a_1 + a_2$
- $-a_3 + a_4$
- $-b_1 + b_2$
- $-b_3 + b_4$
In addition, all the variables are positive (real numbers).
It is surprisingly easy?
There are $13$ inequality constraints, denoted by $f_1, f_2, \cdots, f_{13}$.
We have the identity $$(a_2 + a_4) f_1 + (a_2 - a_1) f_6 + (a_2 + a_3)f_7 = 0.$$ So it is impossible that $f_1 > 0, f_6 > 0, f_7>0, f_{10} > 0$ and all the variables are positive real numbers.
Note: $$f_1 = -a_1b_2 - a_1b_3 + a_2b_1 + a_2b_3 + a_3b_1 - a_3b_2,$$ $$f_6 = -a_2b_3 + a_2b_4 + a_3b_2 + a_3b_4 - a_4b_2 - a_4b_3,$$ $$f_7 = a_1b_2 + a_1b_4 - a_2b_1 - a_2b_4 - a_4b_1 + a_4b_2,$$ $$f_{10} = -a_1 + a_2.$$