Finite inequality alternative by Fourier–Motzkin elimination

If $b$ solves the system and ${\lambda }_j\ge 0$ with ${\sum }_j{\lambda }_j{c}_j=0$, multiply row $j$ by ${\lambda }_j$ and add the finitely many inequalities. By [F3] each row inequality is preserved under its nonnegative multiplier. By the coordinatewise definitions in the Statement and finite-sum distributivity with Fubini from [F2], ${\sum }_{j<m}{\lambda }_j(c_j\cdot b)=({\sum }_{j<m}{\lambda }_j{c}_j)\cdot b=0$. Hence $0\ge {\sum }_{j<m}{\lambda }_j{h}_j$. This proves necessity.

For sufficiency, prove by induction on $n$ the alternative: if the finite system has no solution, there is a nonnegative combination of its rows whose coefficient vector is zero and whose right side is positive. If $n=0$, every row has zero left side; infeasibility means some $h_j>0$, and that single row is the certificate. If $m=0$, the system is feasible, so this case cannot occur under the induction claim's antecedent.

Let $n>0$ and assume the alternative for $n^{\mathrm{\prime }}$ variables, where $n=\sigma (n^{\mathrm{\prime }})=n^{\mathrm{\prime }}\cup \{n^{\mathrm{\prime }}\}$ by [F5] and The natural numbers $\mathbb{N}$ (von Neumann). For $c\in {\mathbb{R}}^n$ define $a\in {\mathbb{R}}^{n^{\mathrm{\prime }}}$ by $a(k):=c(k)$ for $k<n^{\mathrm{\prime }}$, and put $\alpha :=c(n^{\mathrm{\prime }})\in \mathbb{R}$; this separates its first $n^{\mathrm{\prime }}$ coordinates and its last coordinate. Conversely, each $u\in {\mathbb{R}}^{n^{\mathrm{\prime }}}$ and $t\in \mathbb{R}$ determine the unique $b\in {\mathbb{R}}^n$ with $b(k)=u(k)$ for $k<n^{\mathrm{\prime }}$ and $b(n^{\mathrm{\prime }})=t$. For every row $c_j$, define $a_j(k):=c_j(k)$ for $k<n^{\mathrm{\prime }}$ and ${\alpha }_j:=c_j(n^{\mathrm{\prime }})$. Partition the row indices into $P=\{j:{\alpha }_j>0\}$, $N=\{j:{\alpha }_j<0\}$, and $Z=\{j:{\alpha }_j=0\}$. Retain each row $(a_j,h_j)$ for $j\in Z$. For every $p\in P$ and $q\in N$, add the reduced row $((-{\alpha }_q)a_p+{\alpha }_p{a}_q,(-{\alpha }_q)h_p+{\alpha }_p{h}_q)$. Every multiplier used is positive, so these row combinations preserve the inequality directions by [F3].

The reduced system in $u\in {\mathbb{R}}^{n^{\mathrm{\prime }}}$ is feasible exactly when the original is, using the coordinate reconstruction in step 1.3. Indeed, a solution $(u,t)$ implies every retained inequality; adding row $p$ multiplied by $-{\alpha }_q>0$ to row $q$ multiplied by ${\alpha }_p>0$ cancels $t$ and gives each pair row. Conversely, if $u$ satisfies the reduced system, rows in $P$ impose finitely many lower bounds $t\ge L_p:=(h_p-a_p\cdot u)\mathrm{/}{\alpha }_p$, and rows in $N$ impose finitely many upper bounds $t\le U_q:=(h_q-a_q\cdot u)\mathrm{/}{\alpha }_q$. Each pair row is exactly $L_p\le U_q$. To justify the finite extrema, enumerate any nonempty finite list ${\mathrm{\ell }}_0,\dots ,{\mathrm{\ell }}_{k-1}$ of lower bounds and define $M_1={\mathrm{\ell }}_0$; for $1\le j<k$, recursively set $M_{j+1}=M_j$ if $M_j\ge {\mathrm{\ell }}_j$, and $M_{j+1}={\mathrm{\ell }}_j$ otherwise. Totality of the real order makes $M_{j+1}$ the larger of $M_j$ and ${\mathrm{\ell }}_j$; induction [F4] shows that $M_k$ is a member of the list and dominates every entry. Thus a finite nonempty list has a maximum. For an upper-bound list $v_0,\dots ,v_{\mathrm{\ell }-1}$, define $m_1=v_0$ and, for $1\le j<\mathrm{\ell }$, set $m_{j+1}=m_j$ if $m_j\le v_j$, and $m_{j+1}=v_j$ otherwise. The same totality and induction argument shows $m_{\mathrm{\ell }}$ is a member no greater than any entry, so every finite nonempty list has a minimum. If both $P,N$ are nonempty, these extrema and all pair inequalities give ${\max }_{p\in P}{L}_p\le {\min }_{q\in N}{U}_q$, so choose $t={\max }_{p\in P}{L}_p$. If only lower bounds occur choose their finite maximum; if only upper bounds occur choose their finite minimum; if neither occurs choose $t=0$. Thus the original system has a solution.

If the original system is infeasible, step 2.1 makes the reduced system infeasible. By induction there are nonnegative multipliers on reduced rows with zero combined first $n^{\mathrm{\prime }}$ coordinates and positive combined right side. Lift each retained zero-row multiplier to its original row; lift each pair-row multiplier ${\mu }_{pq}$ to coefficients $-{\alpha }_q{\mu }_{pq}$ on row $p$ and ${\alpha }_p{\mu }_{pq}$ on row $q$. All lifted coefficients are nonnegative by [F3]. Every pair lift has last coordinate $(-{\alpha }_q){\alpha }_p+{\alpha }_p{\alpha }_q=0$; the total first coordinates vanish by the reduced certificate, and its right side remains positive. This is the required certificate for the original system and completes the induction.

If the stated multiplier condition holds, the certificate from step 3.1 cannot exist, because it would have zero combined left coefficient and positive combined right side. Therefore the system is feasible. Together with step 1.1 this proves both directions, including the empty-variable base case in step 1.2, the zero/positive/negative sign partition and bound reconstruction in steps 1.3–2.1, and the lifted certificate in step 3.1.