Liouville's lower bound (4.14) for the non-zero derivatives of an integer combination of exponential monomials at lattice points

Let $\iota$ be a finite set, $k_0 \in \iota$ and $d_0 \le 1$, and let $x_1, \dots, x_{d_1}$ and $y_j$ ($j \in \iota$) be vectors in $\mathbb{C}^\iota$ such that every coordinate $x_{i\nu}$ and every $e^{\langle x_i, y_j\rangle}$ is algebraic and, if $d_0 = 1$, every $y_{jk_0}$ is algebraic; here $\langle w, z\rangle = \sum_\nu w_\nu z_\nu$. There is a constant $C \ge 1$ with the following property. Let $T \ge 1$ and $S_1$ be integers, $N \ge 0$, and

with integers $|p_{\tau,t}| \le e^{N}$. If the derivative $D$ of $F$ along a list of $k$ coordinate directions, at a point $\sum_j s_jy_j$ with $0 \le s_j < S_1$, is not zero, then

The proof of Transcendence.schneider_lang_cartesian sets it against two upper bounds: (4.16) for the derivatives of order less than $nET$, and the Schwarz step for the first non-vanishing one.

It is one step of the proof of Baker's theorem formalised in this mission, which follows Chapter 4 of Waldschmidt's book: Baker's theorem from the criterion of Schneider–Lang for Cartesian products, as observed by Bertrand and Masser (1980).

Novelty. None: this is (4.14) of Waldschmidt's book (§4.6, step 2, p. 137) with $T_0 = d_0T$, $T_1 = T$, and a bracket of a slightly different shape from the book's $N + \|\sigma\|\log T_1 + T_0\log(S_1 + \|\sigma\|) + T_1S_1$. The number field $K$, a common denominator $\delta$ and a bound $H$ for the houses are built inside, and Liouville's inequality is Transcendence.liouville_house. The book states that $c_1$ can be computed explicitly; here $C = D\bigl(2 + 2(1 + d_1n)(\log\delta + \log H) + \log(d_1 + 1) + d_0 + d_1 + \log n\bigr)$, with $D = [K : \mathbb{Q}]$ and $n = |\iota|$. The field contains the coordinates of the $x_i$, which step 1 of the book leaves out of it. The contribution of this node is the formal proof.