 Rational feasibility certificate for integer inequalities

A nonempty linear polyhedron with integer inequality coefficients and right sides bounded by $U\ge 1$ 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\le (nU{)}^n$. The resulting rational witness has polynomial binary length and is verifiable in polynomial time, proving that integer linear feasibility is in NP.