Pigeonhole proof of integer Siegel lemma (source code)

= Pigeonhole proof of integer Siegel lemma
{title2=$0<\|z\|_\infty\leq\lfloor(2NA)^{M/(N-M)}\rfloor$}

For $M<N$ homogeneous equations with integer coefficients of absolute value at most $A\geq1$, map the box $\{0,\ldots,Q\}^N$ to its $M$ equation values. There are $(Q+1)^N$ inputs and at most $(2NAQ+1)^M$ outputs. Taking $Q=\lfloor(2NA)^{M/(N-M)}\rfloor$ makes the first count larger, since $2NAQ+1\leq2NA(Q+1)$. The difference of two inputs with the same output is the required nonzero bounded integer solution. Clearing denominators also treats rational equations; expanding a number-field basis replaces each field equation by finitely many rational equations.