Rational feasibility certificate for integer inequalities (source code)

= Rational feasibility certificate for integer inequalities
{title2=$|p_i|,|q_i|\leq(nU)^n$}

A nonempty <linear polyhedron> with integer inequality coefficients and right sides bounded by $U\geq1$ contains a point $x_i=p_i/q_i$ with the displayed bounds. Intersect with an orthant containing a feasible point. Moving along directions annihilating the active constraints, until another constraint becomes active, produces a vertex: the orthant prevents a whole nontrivial line from remaining feasible. At that vertex, choose $n$ independent active inequalities, including coordinate constraints as necessary. <Cramer's rule> and the <Hadamard determinant inequality> bound both determinants by $n^{n/2}U^n\leq(nU)^n$. The resulting rational witness has polynomial binary length and is verifiable in <polynomial time>, proving that integer linear feasibility is in <NP>.