Farkas' lemma

Let $A \in \mathbb{R}^{m\times n}$ and $b \in \mathbb{R}^m$. Then exactly one of the following holds:

The two alternatives exclude each other for a one-line reason: if $Ax \ge b$ and $y \ge 0$ then $y^{\mathsf T} b \le y^{\mathsf T} A x = 0$. The content of the lemma is that one of them always holds, so that infeasibility of a linear system always admits a finite, checkable certificate: a nonnegative combination of the inequalities whose left-hand side cancels identically while the right-hand side stays positive, that is, an explicit derivation of $0 \ge \varepsilon > 0$.

The vector $y$ is the reason linear programming lies in NP $\cap$ co-NP, it is the dual solution in linear programming duality, and it is what an algorithm exhibits when it reports that a system has no solution. In the setting of Smale's ninth problem it makes the decision problem symmetric: both answers can be certified, so the question is entirely one of finding a certificate in a number of arithmetic operations polynomial in $m$ and $n$, not one of verifying it.

Formalization note. The proof is the classical constructive one by Fourier–Motzkin elimination, carried out by induction on the number of variables. Eliminating the last variable replaces the rows by those with vanishing last coefficient together with the pairwise combinations of rows whose last coefficients have opposite signs; multipliers for the reduced system lift to nonnegative multipliers for the original one, and the base case of zero variables is immediate. Both the elimination and the lifting are performed over an arbitrary finite index type, so that the pair index set of one step is available as the index type of the next.