Brumer's theorem, main step: an auxiliary integer polynomial that vanishes at $N^n$ consecutive powers

Let $p$ be a prime, $L$ a number field, $w$ a prime of $L$ above $p$, and $a_1, \dots, a_n \in L$ with $\|a_i - 1\|_w \le \|p\|_w^2$ in the completion $L_w$. Assume that the $p$-adic logarithms satisfy a non-trivial linear relation with coefficients in $L$:

The statement asserts that there are integers $q \ge 1$ and $N \ge 0$ and rational integers $P(\lambda)$, $\lambda \in \{0,\dots,N-1\}^n$, not all zero, such that

The identity is an equality in the number field $L$. Only the hypotheses use the prime $w$ and the logarithm.

Why this is the main step. The $N^n$ numbers $a^{q\lambda} = \prod_i a_i^{q\lambda_i}$ and the $N^n$ exponents $\ell$ give a Vandermonde system. A non-zero solution $P$ forces two of the numbers $a^{q\lambda}$ to be equal, so $\prod_i a_i^{q(\lambda_i - \lambda_i')} = 1$ with $\lambda \ne \lambda'$, and the logarithms satisfy a non-trivial relation with integer coefficients. Thus this statement gives Brumer's theorem NumberField.Brumer.linearIndependent_log_algebraMap: logarithms that are linearly independent over $\mathbb{Z}$ are linearly independent over $L$.

Proof idea (Baker's method). (1) Siegel's lemma gives integers $P(\lambda)$ of controlled size such that the exponential polynomial $\Phi(z_1,\dots,z_n) = \sum_\lambda P(\lambda) \prod_i a_i^{\gamma_i(\lambda) z_i}$, where the exponents $\gamma_i(\lambda)$ are linear in $\lambda$ and use the relation, vanishes with all partial derivatives up to a high order at the points $(q\ell,\dots,q\ell)$, $1 \le \ell \le h$. (2) A $p$-adic Schwarz lemma shows that the values at more points $q\ell$ are $w$-adically very small. (3) These values are algebraic numbers of controlled height, so the product formula shows that they are zero. (4) The steps (2) and (3) are repeated, with half the order of vanishing and more points each time, until there are $N^n$ points.

Formalization Note. $L_w$ is w.1.adicCompletion L with the norm of Definitions.Def_PrimesOverNorm; $\log_p$ is PadicLog.log (p := p) from Definitions.Def_PadicLog; the box is Fin n → Fin N and $\lambda_i$ is (lam i : ℕ). For $n = 0$ the hypothesis c ≠ 0 is impossible. For $n = 1$ the relation gives $\log_p a_1 = 0$, so $a_1 = 1$ and $N = 2$, $P = (1, -1)$ is a solution.