Solution (source code)

= Solution

The <dual linear program> is the <minimization problem>
$$
\boxed{\min\{b^Ty:A^Ty\geq c,\ y\geq0\}.}
$$
Indeed, for $y\geq0$ the <optimization Lagrangian> $c^Tx+y^T(b-Ax)$ bounds the primal objective above on its <feasible points>. Its supremum over $x\geq0$ is finite precisely when $A^Ty\geq c$, and then equals $b^Ty$. The two labelled parts below establish the relevant <weak duality> and <strong duality> conclusions.

For the subsequent infeasibility argument, introduce nonnegative <slack variables> $s$ and the <convex cone>
$$
C=\{Ax+s:x\geq0,\ s\geq0\}.
$$
This is generated by the columns of $A$ and the coordinate vectors. Here is why this <finitely generated cone> is closed. Any representation with a minimal number of positive coefficients uses linearly independent generators: otherwise subtract a suitable multiple of a dependence until one positive coefficient vanishes, preserving nonnegativity. For each fixed independent selection of generators, its nonnegative combinations form a closed set, because the inverse coordinate map on its span is continuous. There are finitely many selections, so their union $C$ is closed. This is the <closedness of finitely generated cones> used in <Farkas' lemma>.

When the primal <linear program> is infeasible, $b\notin C$. Let $p$ be the nearest point of $C$ to $b$, and set $h=p-b$. The minimizing property gives $h^T(z-p)\geq0$ for every $z\in C$. Taking $z=0,2p$ gives $h^Tp=0$. Consequently
$$
h^Tz\geq0\quad(z\in C),\qquad h^Tb=-\|p-b\|^2<0.
$$
In particular $h\geq0$ and $A^Th\geq0$. Rescaling $h$ by the positive number $-h^Tb$ produces the requested <Farkas' lemma> certificate:
$$
\boxed{\lambda\geq0,\qquad A^T\lambda\geq0,\qquad\lambda^Tb=-1.}
$$
Now a <feasible point> of the relaxed inequalities would satisfy
$$
0\leq\lambda^TAx\leq\lambda^T(b+\varepsilon\mathbf1)
=-1+\varepsilon\sum_i\lambda_i.
$$
Since $\lambda^Tb=-1$, the sum of the nonnegative $\lambda_i$ is positive. Thus <robust infeasibility under uniform constraint relaxation> gives
$$
\boxed{\Pi(\varepsilon)=\varnothing\quad\text{for }0\leq\varepsilon<\frac1{\sum_i\lambda_i}.}
$$
The <ellipsoid method> makes progress by reducing the volume of a containing ellipsoid. A nonempty <linear polyhedron> may have empty interior, so small volume alone cannot certify that the original system is infeasible. Relaxing the inequalities remedies this difficulty, but must not make an infeasible system appear feasible. The displayed positive gap proves exactly that sufficiently small relaxations preserve infeasibility. For rational input, determinant bounds give a <Farkas' lemma> certificate of polynomial encoding length, so a sufficiently small rational relaxation can be chosen from the input encoding length. Together with a bounding box and bounds on the volume of a relaxed feasible system, this lets the <ellipsoid method> distinguish infeasibility from a feasible system of very small or zero original volume in <polynomial time>. The certificate argument alone does not assert a polynomial precision bound for arbitrary unencoded real coefficients.