Parameters for the direct proof of the criterion of Schneider–Lang: the hypotheses of Proposition 4.10 and the inequalities behind (4.17) and (4.19)

Let $1 \le n < d$ be integers, $C \ge 1$, $c_x, c_y \ge 0$ and $c_F \ge 1$. There are integers $S_1, T, E \ge 1$ and real numbers $U, N > 0$ such that, with $r = (c_y + 2)S_1$ and $R = Er$:

1. $12n^2 \le N + 2U$, $e \le E \le e^{(N + 2U)/6}$, $(T+1)^{d}R^{T}e^{c_xTR} \le e^{U}$ and $\bigl(2(N + 2U)\bigr)^{n+1} \le (T+1)^{d}N(\log E)^{n}$;
2. for every integer $k < nET$,

3. for all integers $u \ge ET$ and $M \le 2nu$, with $\rho' = c_FS_1u/T$,

In the proof of Transcendence.schneider_lang_cartesian, $C$ is the constant of (4.14) and $c_F$ that of the Schwarz step: condition 1 gives the auxiliary function (Transcendence.exists_exp_monomials_small_on_grid), condition 2 makes its derivatives of order less than $nET$ vanish at the grid points, and condition 3 rules out a 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: the choice of parameters at the end of §4.6 of Waldschmidt's book (p. 141), in its shape: $S_1$ is fixed and large, then $T = (S_1m)^n$, an $n$-th power and a multiple of $S_1^n$ as the book asks, and $E = S_1^{d-1-n}m^{d-n}$, for a large integer $m$; $U = S_1ET\log E/(2C\cdot6^{n+1})$ and $N = U/(2C)$. The role of the book's $S_0$ is played by $ET$, and $ET\cdot S_1 = T^{d/n}$. Conditions 2 and 3 are the inequalities that the book's (4.17) and (4.19) are imposed to guarantee. The book gives their asymptotics without proof; they are proved in Transcendence.schneider_lang_vanishing_ineq and Transcendence.schneider_lang_extrapolation_ineq, the second uniformly in $S_0' = u \ge ET$. The contribution of this node is the formal proof.