Brumer's theorem, Lemme 1: integer coefficients of controlled size for the auxiliary function (Siegel's lemma)

Let $L$ be a number field of degree $d$, let $a_1,\dots,a_n, c_1,\dots,c_n \in L$, let $k \in \{1,\dots,n\}$ be an index (the pivot) and let $q \ge 0$ be an integer. For $\lambda \in \{0,\dots,N-1\}^n$ put

and for integers $P(\lambda)$, a multi-index $m \in \mathbb{N}^n$ and $\ell \ge 1$ put

The statement asserts that there is a constant $C \ge 1$, which depends only on $L, a, c, k, q$, with this property: for all integers $N \ge 1$, $S \ge 0$, $H \ge 0$ with

there are integers $P(\lambda)$, not all zero, with

Meaning. If $\sum_i c_i \log a_i = 0$, then $c_k \log u_\lambda = \sum_i \gamma_i(\lambda) \log a_i$, and $Q(m,\ell)$ is, up to non-zero factors, the partial derivative of order $m$ of the auxiliary function $\sum_\lambda P(\lambda) \prod_i a_i^{\gamma_i(\lambda) z_i}$ at the diagonal point $(q\ell,\dots,q\ell)$. The lemma itself is algebraic: it does not use a place of $L$, a logarithm or the relation.

Proof idea. Since $\gamma_k = 0$, the equations with $m_k > 0$ hold for all $P$. There are at most $(S+1)^{n-1} H$ other equations in $L$. After multiplication by a common denominator and expansion in an integral basis they become at most $d (S+1)^{n-1} H$ linear equations with integer coefficients of size at most $C^{NH+S} N^S$ in the $N^n$ unknowns $P(\lambda)$. Siegel's lemma with at least twice as many unknowns as equations gives a non-zero solution with $|P(\lambda)| \le N^n \cdot (\text{coefficient bound})$.

Use. This is the first step of the proof of NumberField.Brumer.exists_auxiliary_polynomial.

Formalization Note. The box is Fin n → Fin N; $\lambda_i$ is (lam i : ℕ); $|m| \le S$ is ∑ i, m i ≤ S; the exponent $n - 1$ is natural subtraction (the existence of k : Fin n gives $n \ge 1$). The constant is chosen after $q$, so it can depend on $q$; the exponent of $C$ has $N H$ and not $q N H$. For $H = 0$ there are no equations. The platform has an entrywise Siegel lemma, Transcendence.siegel_entrywise; Mathlib has Int.Matrix.exists_ne_zero_int_vec_norm_le and the house of an algebraic number (NumberField.house).