Dependency graph

Legend

Boxes: definitions
Rounded boxes: theorems and lemmas
Double border: not found in the sources read, and not routine (chapter “Results not found in the sources read”)
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Corollary 9.25Baker’s theorem for two logarithms

Let \(x\) and \(y\) be logarithms of algebraic numbers, linearly independent over \(\mathbb {Q}\), and let \(a,b\) be algebraic numbers, not both zero. Then \(ax+by\) is transcendental.

Source: Baker [ Bak66 ] ; the proof follows [ Wal00 , Chapter 4 ] , after Bertrand–Masser [ BM80 ] and Masser [ Mas81 ] .

LaTeX Lean

Corollary 13.17Two candidates on an axis-parallel line

Let \(u\neq v\) be candidates with \(v-u\) real or purely imaginary. Then \(|v|^{2}/|u|^{2}\in \mathbb {Q}\) if and only if \(|v|=|u|\), and \(|v|=|u|\) if and only if \(v=\bar u\) when \(v-u\in i\mathbb {R}\) and \(v=-\bar u\) when \(v-u\in \mathbb {R}\).

Source: From the author’s unpublished manuscript on the conjecture, where it was derived from [ RW97 , Théorème 0.2 ] ; it is a direct instance of [ Wal73 , Corollaire 4 ] .

LaTeX Lean

Corollary 10.13Two exclusions at a candidate

Assume Roy’s strong six exponentials theorem, and let \(u\) be a candidate: \(u\neq 0\), \(|u|\) algebraic and \(e^{u}\) algebraic. Let \(a\in \overline{\mathbb {Q}}\), \(a\neq 0\), and \(\rho =u\bar u\). Then \(u/(u^{2}-a)\notin \widetilde{\mathcal L}\) if \(a\bar a\neq \rho ^{2}\), and \(u/(u^{2}-a)^{2}\notin \widetilde{\mathcal L}\) if \(a\bar a=\rho ^{2}\).

Source: One substitution in [ Dia04 , Théorème 2 ] , at \(x=(u,\bar u)\) and \(y=1/(u^{2}-a)\), and in [ Dia07 , Corollaire 4(4) and Théorème 7(1) ] ; the second part is [ Dia07 , Théorème 6(3) ] . Roy’s theorem is [ Roy92 ] .

LaTeX Lean

Corollary 13.16The pair dichotomy

Let \(u,v\) be candidates with \(|v|^{2}/|u|^{2}\in \mathbb {Q}\). Then \(v\in \mathbb {Q}^{\times }u\cup \mathbb {Q}^{\times }\bar u\) if and only if \(u\) and \(v\) are algebraically dependent over \(\mathbb {Q}\).

Source: From the author’s unpublished manuscript on the conjecture, where it was derived from [ RW97 , Théorème 0.2 ] ; it is a direct instance of [ Wal73 , Corollaire 4 ] .

LaTeX Lean

Corollary 10.32Pairs of powers at a candidate

Assume Roy’s strong six exponentials theorem and let \(u\) be a candidate. For \(4\le k\lt l\) with \(l\in \{ k+1,k+2,2k-1,2k,2k+1,3k\} \), \(u^k\) and \(u^l\) are not both in \(\widetilde{\mathcal L}\).

Source: Each case is one substitution in [ Dia07 ] : Corollaire 2(P)(1), Théorème 7(1), Corollaire 5(1)–(2), with \(\bar u^{k}=\rho ^{k}u^{-k}\).

LaTeX Lean

Corollary 10.37The third family at a candidate

Assume Roy’s strong six exponentials theorem, let \(u\) be a candidate and \(a_1\neq a_2\) algebraic with \(a_i\bar a_i=|u|^{4}\). Then \(u/(u^{2}-a_1)+u/(u^{2}-a_2)\notin \widetilde{\mathcal L}\).

Source: One line from a substitution in [ Dia07 , Théorème 7(2) ] .

LaTeX Lean

Corollary 10.26Not a matrix of logarithms

Let \(u\) be a candidate with \(u,w_1,\dots ,w_m\) algebraically independent over \(\overline{\mathbb {Q}}\). In every \(2\times 2\) configuration over \(\overline{\mathbb {Q}}\) in \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}w_1+\dots +\overline{\mathbb {Q}}w_m\), each row and each column has an entry outside \(\overline{\mathbb {Q}}\mathcal L\).

Source: Not found in the sources read; short (Chapter 14).

LaTeX Lean

Corollary 10.36Two poles at a candidate

Assume Roy’s strong six exponentials theorem and let \(u\) be a candidate. For distinct non-zero algebraic \(a_1,a_2\), the numbers \(u/(u^{2}-a_1)\) and \(u/(u^{2}-a_2)\) are not both in \(\widetilde{\mathcal L}\).

Source: One substitution in [ Dia07 , Théorème 7(2) ] , that is [ Fis01 , Lemma 6.1 ] .

LaTeX Lean

Corollary 10.20At most \(2\times 2\) near a point of a circle

Let \(u\) be transcendental over a subfield \(K\subseteq \mathbb {C}\) with \(\rho =u\bar u\in K\). Every \(p\times q\) configuration over \(K\) in \(K+Ku+K\bar u\) has \(p+q\le 4\).

Source: Not found in the sources read; short (Chapter 14). Over \(\overline{\mathbb {Q}}\) it is a case of Roy’s lemma [ Wal00 , Lemma 12.16 ] .

LaTeX Lean

Corollary 10.23The constant terms form an invertible matrix

In the setting of Corollary 10.21, for every \(2\times 2\) configuration there is an invertible \(c\in K^{2\times 2}\) with \(x_iy_j-c_{ij}\in Ku+K\bar u\). In particular no \(2\times 2\) configuration lies in \(Ku+K\bar u+Kw_1+\dots +Kw_m\).

Source: Not found in the sources read; short (Chapter 14). It sharpens Diaz.generic_qbar_homogeneous_four_exp_barrier, the homogeneous barrier of the companion note.

LaTeX Lean

Corollary 13.21Diaz under Kirby’s weak form

Assume the case \(n=2\) of Kirby’s weak Schanuel conjecture [ Kir18 , Conjecture 1.5 ] : if \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(a,b,e^{a},e^{b})\lt 2\), then \(ma+nb\in 2\pi i\mathbb {Z}\) for some integers \((m,n)\neq (0,0)\). Then Diaz’s conjecture holds if and only if \(t^{2}+\pi ^{2}\) is transcendental for every real \(t\neq 0\) with \(e^{t}\) algebraic.

Source: Not found in the sources read; short (Chapter 14).

LaTeX Lean

Corollary 11.2\(\mathrm{Li}_2(1/2)\) against \(e^{i/\pi }\)

Either \(\pi ^{2}/12-(\log 2)^{2}/2\) is irrational, or \(e^{i\gamma /\pi }\) is transcendental for every \(\gamma \in \mathbb {Q}\), \(\gamma \neq 0\).

Source: By Euler’s identity, \(\pi ^{2}/12-(\log 2)^{2}/2=\mathrm{Li}_2(1/2)=\sum _{n\ge 1}1/(n^{2}2^{n})\). Its irrationality is listed as unknown in [ Wal04 , p. 274 ] and is still open: [ Hat93 , RV05 , CDT24 ] cover \(\mathrm{Li}_2(1/q)\) only for \(q\ge 6\) and \(q\le -5\). The dichotomy was not found in the sources read.

LaTeX Lean

Corollary 10.21Generic numbers never enter

Let \(u,w_1,\dots ,w_m\) be algebraically independent over a subfield \(K\subseteq \mathbb {C}\), with \(\rho =u\bar u\in K\). Every \(p\times q\) configuration over \(K\) with \(p,q\ge 2\) in \(K+Ku+K\bar u+Kw_1+\dots +Kw_m\) is \(2\times 2\) and lies in \(K+Ku+K\bar u\).

Source: Not found in the sources read; short (Chapter 14). For \(K=\overline{\mathbb {Q}}\) it contains Theorem 10.1.

LaTeX Lean

Corollary 13.7Two named constants

The numbers \((\log 2)^{2}+\pi ^{2}\) and \((\log 3)^{2}+\pi ^{2}\) are not both rational.

Source: Not found in the sources read, but short (Chapter 14).

LaTeX Lean

Corollary 13.5Rational moduli over the field of pi

Let \(u,v\in \mathcal L\setminus \{ 0\} \) be algebraic over \(\mathbb {Q}(\pi )\), with \(|u|^{2}\) and \(|v|^{2}\) rational. Then \(v\in \mathbb {Q}u\) or \(v\in \mathbb {Q}\bar u\).

Source: A step of Corollary 13.6; one substitution in [ Bro74 , Corollary 7 ] .

LaTeX Lean

Corollary 13.10Rational data exclude one boundary failure

Let \(t\neq 0\) be real with \(e^{t}\) algebraic and \(t^{2}+\pi ^{2}\in \mathbb {Q}\). Then \(e^{i\gamma /\pi }\) is transcendental for every \(\gamma \in \mathbb {Q}\), \(\gamma \neq 0\).

Source: Not found in the sources read, but short (Chapter 14): the two open boundary statements of the library cannot both fail at rational data. The key step is [ Bro74 , Corollary 5 ] at \(\eta =t/\pi \).

LaTeX Lean

Corollary 13.6At most one rational value of t squared plus pi squared

Let \(t_0,t_1\) be real with \(e^{t_0},e^{t_1}\) algebraic. If \(t_0^{2}+\pi ^{2}\) and \(t_1^{2}+\pi ^{2}\) are both rational, then \(t_1=\pm t_0\).

Source: Not found in the sources read, but short (Chapter 14). One substitution in [ Bro74 , Corollary 7 ] .

LaTeX Lean

Lemma 10.25Baker: no algebraic number in \(\overline{\mathbb {Q}}\mathcal L\)

An algebraic number in the \(\overline{\mathbb {Q}}\)-span of the logarithms of algebraic numbers is \(0\).

Source: A consequence of Baker’s theorem [ Bak66 ] .

LaTeX Lean

Lemma 13.14Numbers on an axis

If \(\bar u=\pm u\) and \(|u|\) is algebraic, then \(u\) is algebraic.

Source: Known: the first step of Case 1 of the proof of [ Dia04 , Proposition 1 ] , p. 551.

LaTeX Lean

Lemma 4.3Gel’fond’s auxiliary function

Let \(\alpha ',\gamma '\neq 0\) and \(m\ge 1\). There is \(C\ge 1\) such that for all \(n\ge 1\) and \(q\) with \(q^{2}=2mn\) there are algebraic integers \(\eta _{ab}\in \mathcal{O}_K\), not all zero, with \(\overline{\left|\eta _{ab}\right|}\le C^{n}n^{(n+1)/2}\) and

\[ \sum _{a,b}\eta _{ab}(a+b\beta ')^{k}\alpha '^{\, aj}\gamma '^{\, bj}=0\qquad (1\le j\le m,\ 0\le k\lt n). \]

Source: A step of Gel’fond’s proof [ Gel34 ] .

LaTeX Lean

Lemma 6.19The linear system

Let \(x_1,x_2,y_1,y_2\in \mathbb {C}\) have presentation data, and suppose every \(e^{x_iy_j}\) is algebraic. There is \(\kappa _1\gt 0\) such that for every large \(N\) there are an integer \(M\) with \(0\lt M\le \kappa _1S\) and an \(R\times U\) integer matrix \(B\), where \(U=S(2N)^{2}Md\) and \(2R\le U\), with entries of absolute value at most \(e^{\kappa _1N^{2}\sqrt{\log N}}\), such that for every integer vector \(q\) with \(Bq=0\)

\[ F_q^{(m)}(ay_1+by_2)=0\qquad \text{for all }a\lt t_1,\ b\lt t_2,\ m\lt S. \]

Source: The equation count of [ Wal73 , Lemme 4 ] .

LaTeX Lean

Lemma 7.5The linear system, one algebraic column

Let \(x_1,x_2,y_1,y_2,\omega ,\omega _1\in \mathbb {C}\) and \(Q\in \mathbb {Z}[X][Y]\), and suppose that the derivatives of the functions \(F_q\) have reduced presentations as in the conclusion of Lemma 7.4. Then the conclusion of Lemma 6.19 holds, with \(d=\deg _YQ\).

Source: The equation count of [ Wal73 , Lemme 4 ] , pp. 197–198.

LaTeX Lean

Lemma 6.29The construction

Let \(l_{11},l_{12},l_{21},l_{22}\) satisfy the hypotheses of Lemma 6.14. Then there are a transcendental \(\omega \), functions \(\sigma _1,\sigma _2\) and constants \(a_1,a_2\ge 1\) satisfying the hypotheses of Theorem 6.6, and pairs \(x_1,x_2\) and \(y_1,y_2\), each linearly independent over \(\mathbb {Q}\), with the following property. For every \(C\) and every large \(N\) there are natural numbers \(S,T,R_1,R_2,S'\), coefficients \(c(i,j,h)\in \mathbb {C}\) (\(i\lt S\), \(j,h\lt T\)), not all zero, and \(\lambda \gt 0\) such that

the inequality of Lemma 6.13 holds, and
whenever \(a\lt R_1\), \(b\lt R_2\), \(s\lt S'\) and \(G^{(s)}(ay_1+by_2)\neq 0\), where

\[ G(z)=\sum _{i\lt S}\sum _{j,h\lt T}c(i,j,h)\, z^{i}e^{(jx_1+hx_2)z}, \]

some \(P\in \mathbb {Z}[X]\) is small at \(\omega \) for \((N,C)\) with respect to \(\sigma _1,\sigma _2\).

Source: [ Wal73 , § III, (4) and Lemmes 4, 5, 7 ] .

LaTeX Lean

Lemma 7.9The construction, one algebraic column

Let \(x_1,x_2,y_1,y_2\) satisfy the column hypotheses. Then there are a transcendental \(\omega \), and functions \(\sigma _1,\sigma _2\) and constants \(a_1,a_2\ge 1\) satisfying the hypotheses of Theorem 6.6, such that for every \(C\) and every large \(N\) there are natural numbers \(S,T,R_1,R_2,S'\), coefficients \(c(i,j,h)\in \mathbb {C}\) (\(i\lt S\), \(j,h\lt T\)), not all zero, and \(\lambda \gt 0\) with the two properties listed in Lemma 6.29, for these \(x_1,x_2,y_1,y_2\).

Source: [ Wal73 , Lemmes 4, 5 and 7 ] , with the growth functions of p. 201, and the count that [ Wal73 , Lemme 6 ] needs for the zero estimate [ Wal71 , § 4, Lemme 3 ] .

LaTeX Lean

Lemma 6.21The auxiliary function

Let \(x_1,x_2,y_1,y_2\in \mathbb {C}\) have presentation data, and suppose every \(e^{x_iy_j}\) is algebraic. There is \(\kappa \gt 0\) such that for every large \(N\) there are \(M\le \kappa S\) and integers \(q(i,j,h,\mu ,\nu )\) (\(i\lt S\), \(j,h\lt 2N\), \(\mu \lt M\), \(\nu \lt d\)) of absolute value at most \(e^{\kappa N^{2}\sqrt{\log N}}\), such that the coefficients \(c_q(i,j,h)\) are not all zero and of absolute value at most \(e^{\kappa N^{2}\sqrt{\log N}}\), and

\[ F_q^{(m)}(ay_1+by_2)=0\qquad \text{for all }a\lt t_1,\ b\lt t_2,\ m\lt S. \]

Source: [ Wal73 , Lemme 4 ] , with Siegel’s lemma.

LaTeX Lean

Lemma 7.6The auxiliary function, one algebraic column

Let \(x_1,x_2,y_1,y_2,\omega ,\omega _1\in \mathbb {C}\) and \(Q\in \mathbb {Z}[X][Y]\) with \(d=\deg _YQ\ge 1\), such that no non-zero \(A\in \mathbb {Z}[X][Y]\) with \(\deg _YA\lt d\) vanishes at \((\omega ,\omega _1)\), and suppose that the derivatives of the functions \(F_q\) have reduced presentations as in the conclusion of Lemma 7.4. Then the conclusion of Lemma 6.21 holds.

Source: [ Wal73 , Lemme 4 ] , pp. 197–198, with Siegel’s lemma, Lemme 1 there.

LaTeX Lean

Lemma 12.4Binary forms at a transcendental point

Let \(K\subseteq \mathbb {C}\) be a subfield and \(x,y\in \mathbb {C}\) with \(y\neq 0\) and \(x/y\) transcendental over \(K\). If \(\sum _{i=0}^{d}c_ix^{i}y^{d-i}=0\) with all \(c_i\in K\), then all \(c_i\) are zero.

Source: Elementary.

LaTeX Lean

Lemma 2.8Cauchy’s estimate with zeros

Let \(F\) be an entire function, \(c\in \mathbb {C}\), \(\rho \ge 0\) and \(R\gt \rho +1\). Let \(S\) be a finite set of points \(z\) with \(|z-c|\le \rho \), and put \(\sigma =\sum _{z\in S}\operatorname {ord}_zF\). If \(|F(z)|\le M\) whenever \(|z-c|=R\), then for every \(s\in \mathbb {N}\)

\[ |F^{(s)}(c)|\le s!\, \frac{R}{R-1}\Bigl(\frac{\rho +1}{R-\rho }\Bigr)^{\sigma }M. \]

Source: [ Wal71 , § 4, (4.3) ] .

LaTeX Lean

Lemma 10.4A progression through \(1\), \(u\) and \(\bar u\)

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) with \(u\bar u\) algebraic, let \(b\neq 0\) and \(h\notin \overline{\mathbb {Q}}\), and suppose that \(V=\overline{\mathbb {Q}}\, b+\overline{\mathbb {Q}}\, bh+\overline{\mathbb {Q}}\, bh^{2}+\overline{\mathbb {Q}}\, bh^{3}\) contains \(1\), \(u\) and \(\bar u\). Then \(V\) contains \(u^{2}\), or \(\bar u^{2}\), or \(1/(u-a)\) for some \(a\in \overline{\mathbb {Q}}\), \(a\neq 0\).

Source: A step of Theorem 10.6.

LaTeX Lean

Lemma 10.8What these spaces do not contain

With \(u\), \(a\) and \(z\) as in Proposition 10.7, the space \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}z+\overline{\mathbb {Q}}\bar z\) contains neither \(u^{2}\) nor \(\bar u^{2}\), nor \(1/(u-b)\) for any \(b\in \overline{\mathbb {Q}}\), \(b\neq 0\).

Source: Elementary.

LaTeX Lean

Lemma 10.34What two poles do not contain

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) with \(\rho =u\bar u\) algebraic, \(a_1\neq a_2\) non-zero algebraic numbers, \(z_i=u/(u^{2}-a_i)\) and \(W=\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}z_1+\overline{\mathbb {Q}}z_2\). Then \(W\) contains none of \(u^{2}\), \(\bar u^{2}\) and \(1/(u-c)\) with \(c\in \overline{\mathbb {Q}}\) non-zero.

Source: Elementary.

LaTeX Lean

Lemma 4.1One number field

Let \(l,\beta \in \mathbb {C}\) with \(\beta \), \(e^{l}\) and \(e^{\beta l}\) algebraic. There are a number field \(K\), a field embedding \(\sigma \colon K\to \mathbb {C}\) and \(\alpha ',\beta ',\gamma '\in K\) with \(\sigma (\alpha ')=e^{l}\), \(\sigma (\beta ')=\beta \) and \(\sigma (\gamma ')=e^{\beta l}\).

Source: A step of Gel’fond’s proof [ Gel34 ] .

LaTeX Lean

Lemma 6.26The core of the construction

Let \(x_1,x_2\) be linearly independent over \(\mathbb {Q}\), and likewise \(y_1,y_2\). Suppose every \(e^{x_iy_j}\) is algebraic and \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}[x_1,x_2,y_1,y_2]\le 1\). Then there are a transcendental \(\omega \in \mathbb {C}\) and \(k\gt 0\) such that for every \(C\) and every large \(N\) there are coefficients \(c(i,j,h)\), not all zero, with the following property: whenever \(a\lt R_1\), \(b\lt R_2\), \(s\lt S'\) and \(F^{(s)}(ay_1+by_2)\neq 0\), some \(P\in \mathbb {Z}[X]\) is small at \(\omega \) for \((N,C)\) with respect to the growth functions of constant \(k\).

Source: [ Wal73 , § III, (4) and Lemmes 4, 5, 7 ] .

LaTeX Lean

Lemma 7.8The core of the construction, one algebraic column

If \(x_1,x_2,y_1,y_2\) satisfy the column hypotheses, then the conclusion of Lemma 6.26 holds.

Source: [ Wal73 , Lemmes 4, 5 and 7 ] , with the parameters of p. 196.

LaTeX Lean

Lemma 6.28The parameters beat the zero count

Let \(X,Y_1,Y_2\ge 0\). There is \(N_0\) such that for every integer \(N\gt N_0\), with \(T=2N\), \(\lambda =1/20\) and \(n=ST^{2}\),

\[ \frac{n}{\lambda }+2\, \frac{1+n^{\lambda }}{\lambda \log n}\bigl(1+(R_1Y_1+R_2Y_2)\, TX\bigr)\le R_1R_2S'. \]

Source: The parameters of [ Wal73 , (4) and Lemme 6 ] against the zero estimate [ Wal71 , § 4, Lemme 3 ] .

LaTeX Lean

Lemma 6.27The growth functions

For every \(k\gt 0\) the growth functions \(\sigma _1,\sigma _2\) are strictly increasing and tend to \(+\infty \), and for every \(x\gt 0\)

\[ \sigma _2(x)\le \sigma _1(x),\qquad \sigma _i(x+1)\le 3\, \sigma _i(x)\quad (i=1,2). \]

Source: Elementary; the functions of the end of [ Wal73 , § III ] .

LaTeX Lean

Lemma 9.5Hermite interpolation in one coordinate

Let \(g\) be an entire function on \(\mathbb {C}^{\iota }\) with \(|g|\le K\) on the closed polydisc of radius \(R\) about \(0\), let \(i\in \iota \) and \(S_0\in \mathbb {N}\), and let \(E\) be a finite set of complex numbers of modulus at most \(r\), where \(0\lt r\) and \(5r\le R\); put \(p=|E|S_0\). There is an entire function \(h\) on \(\mathbb {C}^{\iota }\) such that:

\(|h|\le 3^{p}K\) on the closed polydisc of radius \(R\) about \(0\);
\(|g-h|\le (2r)^{p}(3/R)^{p}K\) on the closed polydisc of radius \(r\) about \(0\);
for every point \(\xi \) and every list \(v\) of \(m\) coordinate directions different from \(i\): if \(D_{(v,i^{k})}\, g(\xi [i:=\zeta ])=0\) for every \(\zeta \in E\) and every \(k\lt S_0\), where \((v,i^{k})\) is the list \(v\) followed by \(k\) times \(i\), then \(D_vh(\xi )=0\).

Source: A step of the proof of [ Wal00 , Proposition 4.7, pp. 122–130 ] : the case \(m=n\) of its Lemma 4.8 (pp. 123–126) in one coordinate, with the bounds of Step 2.4.

LaTeX Lean

Lemma 10.3A normal form for \(P_1P_2=P_0^2\)

Let \(K\) be a field and \(P_0,P_1,P_2\in K[X]\) with \(\deg P_1,\deg P_2\le 3\), \(P_1P_2=P_0^{2}\), and \(P_0,P_1\) linearly independent over \(K\). Then there are \(Q_0,Q_1\in K[X]\) of degree at most \(1\), linearly independent over \(K\), and \(a,b\in K\) such that, with \(g=aQ_0+bQ_1\),

\[ P_0=g\, Q_0Q_1,\qquad P_1=g\, Q_1^{2},\qquad P_2=g\, Q_0^{2}. \]

Source: Elementary.

LaTeX Lean

Lemma 4.4Derivatives at the integers

Let \(K\) be any field, \(\sigma \colon K\to \mathbb {C}\) a ring homomorphism, and \(l,\beta \in \mathbb {C}\) with \(\sigma (\beta ')=\beta \), \(\sigma (\alpha ')=e^{l}\) and \(\sigma (\gamma ')=e^{\beta l}\). For \(\eta _{ab}\in K\) put \(E(z)=\sum _{a,b}\sigma (\eta _{ab})e^{(a+b\beta )lz}\). Then for all \(k,j\in \mathbb {N}\)

\[ E^{(k)}(j)=l^{k}\, \sigma \Bigl(\sum _{a,b}\eta _{ab}(a+b\beta ')^{k}\alpha '^{\, aj}\gamma '^{\, bj}\Bigr). \]

Source: A step of Gel’fond’s proof [ Gel34 ] .

LaTeX Lean

Lemma 4.7Upper bound for the first non-zero derivative

Let \(l,\beta \in \mathbb {C}\), \(m\ge 1\) and \(C_0\ge 1\). There is \(C\ge 1\) with the following property. Let \(n\ge 1\), \(q^{2}=2mn\), \(n\le r\) and \(1\le l_0\le m\), and let \(E(z)=\sum _{a,b}c_{ab}e^{(a+b\beta )lz}\) with \(c_{ab}\in \mathbb {C}\), \(|c_{ab}|\le C_0^{n}n^{(n+1)/2}\). If \(E^{(k)}(j)=0\) for all \(1\le j\le m\) and \(k\lt r\), then

\[ |E^{(r)}(l_0)|\le C^{r}r^{\, r(3-m)/2+3/2}. \]

Source: A step of Gel’fond’s proof [ Gel34 ] .

LaTeX Lean

Lemma 5.2The descent step

Let \(d+l\lt dl\), let \(K\) be a number field containing every \(e^{x_iy_j}\), and let \(c\gt 0\). There is \(M_0\) such that for all \(M\ge M_0\), all \(L\ge 1\) with \(L^{d}\le cM^{l}\), all integers \(p_\lambda \) with \(|p_\lambda |\le e^{cLM}\) and all \(N\ge M\): if \(F_p(\langle m,y\rangle )=0\) for every \(m\in \mathbb {N}^{l}\) with all \(m_j\lt N\), then \(F_p(\langle m,y\rangle )=0\) for every \(m\in \mathbb {N}^{l}\) with all \(m_j\lt N+1\).

Source: [ Lang66 , Ch. II ] , [ Ram68 ] ; see [ Wal09 , § 3.4 ] .

LaTeX Lean

Lemma 12.1The lemma on linear forms

Let \(F\) be a field of characteristic \(0\) and let \(M\) be a \(2\times 2\) matrix whose entries are linear forms over \(F\) in \(n\) variables. If \(\det M\) vanishes identically, then the rows of \(M\) are linearly dependent over \(F\), or its columns are.

Source: Elementary.

LaTeX Lean

Lemma 13.15Candidates are off the axes

Let \(u\neq 0\) be real or purely imaginary with \(|u|\) algebraic. Then \(e^{u}\) is transcendental.

Source: A consequence of Hermite–Lindemann (Theorem 3.2).

LaTeX Lean

Lemma 6.3Small values force divisibility

Let \(P,Q\in \mathbb {Z}[X]\) with \(Q\) irreducible, let \(\alpha \in \mathbb {C}\), and let \(H,h\ge 1\) bound the absolute values of the coefficients of \(P\) and of \(Q\) respectively. Put \(d=\deg P\) and \(\delta =\deg Q\). If

\[ \bigl((1+|\alpha |)(d+\delta )\bigr)^{d+\delta }H^{\delta }h^{d}\bigl(|P(\alpha )|+|Q(\alpha )|\bigr)\lt 1, \]

then \(Q\) divides \(P\).

Source: [ Wal71 , § 3, (3.13) ] , citing [ Lang66 , Ch. V, § 2 ] .

LaTeX Lean

Lemma 6.4Divisibility at one scale

Let \(\alpha \in \mathbb {C}\) and \(\varepsilon \gt 0\). There is \(U\) such that for all real \(u\ge U\) and \(1\le v\le u\) the following holds. Let \(P,Q\in \mathbb {Z}[X]\) with \(Q\) irreducible, the coefficients of \(P\) of absolute value at most \(e^{u}\) and \(\deg P\le v\), the coefficients of \(Q\) of absolute value at most \(e^{3u}\) and \(\deg Q\le (1+\varepsilon /2)v\), and \(|P(\alpha )|\lt e^{-(4+\varepsilon )uv}\), \(|Q(\alpha )|\lt e^{-(4+\varepsilon )uv}\). Then \(Q\) divides \(P\).

Source: A step of the proof of [ Wal71 , § 3, Lemme fondamental ] .

LaTeX Lean

Lemma 5.3Vanishing on the whole lattice

Let \(l\ge 2\), \(L\in \mathbb {N}\) and \(p_\lambda \) integers. If \(F_p(\langle m,y\rangle )=0\) for every \(m\in \mathbb {N}^{l}\), then \(p_\lambda =0\) for every \(\lambda \in \{ 0,\dots ,L-1\} ^{d}\).

Source: [ Lang66 , Ch. II ] , [ Ram68 ] ; see [ Wal09 , § 3.4 ] .

LaTeX Lean

Lemma 5.1The auxiliary function

Let \(d+l\lt dl\), and let \(K\) be a number field containing every \(e^{x_iy_j}\). There is \(c\gt 0\) such that for every large \(M\) there are an integer \(L\ge 1\) with \(L^{d}\le cM^{l}\) and integers \(p_\lambda \) with \(|p_\lambda |\le e^{cLM}\), not all zero for \(\lambda \in \{ 0,\dots ,L-1\} ^{d}\), such that \(F_p(\langle m,y\rangle )=0\) for every \(m\in \mathbb {N}^{l}\) with \(m_j\lt M\) for all \(j\).

Source: [ Lang66 , Ch. II ] , [ Ram68 ] ; see [ Wal09 , § 3.4 ] .

LaTeX Lean

Lemma 2.2A common denominator for monomials

Let \(K\) be a number field and \((\theta _i)_{i\in I}\) a finite family in \(K\). There are a non-zero algebraic integer \(b\in K\) and a real number \(H\ge 1\) such that for every \(e\in \mathbb {N}^{I}\) and every \(E\in \mathbb {N}\) with \(\sum _ie_i\le E\), the number \(b^{E}\prod _i\theta _i^{e_i}\) is an algebraic integer whose house is at most \(H^{E}\).

Source: Standard.

LaTeX Lean

Lemma 9.17An auxiliary function small at the grid points

Let \(k_0\in \iota \), \(d_0\le 1\) and \(d=d_0+d_1\), and let \(x_1,\dots ,x_{d_1}\) and \(y_j\) (\(j\in \iota \)) be vectors in \(\mathbb {C}^{\iota }\) with \(\sum _{i,\nu }|x_{i\nu }|\le c_x\) and \(\sum _j\| y_j\| \le c_y\). Let \(S_1,T\ge 1\) be integers and \(U,N\gt 0\) and \(E\) real numbers; put \(r=(c_y+2)S_1\) and \(R=Er\), and assume

\[ 12n^{2}\le N+2U,\qquad e\le E\le e^{(N+2U)/6}, \]

\[ (T+1)^{d}R^{T}e^{c_xTR}\le e^{U},\qquad \bigl(2(N+2U)\bigr)^{n+1}\le (T+1)^{d}N(\log E)^{n}. \]

Then there are integers \(p_{\tau ,t}\), not all zero, with \(|p_{\tau ,t}|\le e^{N}\), such that, with \(T_0=d_0T\) and \(T_1=T\):

\(\bigl|D_LF_p\bigl(\sum _js_jy_j\bigr)\bigr|\le k!\, e^{-U}\) at every grid point and for every list \(L\) of \(k\) coordinate directions;
\(|F_p(w)|\le (T+1)^{d}e^{N}\rho ^{T}e^{c_xT\rho }\) whenever \(\rho \ge 1\) and \(\| w\| \le \rho \).

Source: [ Wal00 , § 4.6, step 3 and (4.16), pp. 138–139 ] .

LaTeX Lean

Lemma 6.24Norms down to \(\mathbb {Q}(\omega )\)

Let \(\omega ,\omega _1\in \mathbb {C}\) and let \(Q\in \mathbb {Z}[X][Y]\) be monic in \(Y\) of degree \(d\), with \(Q(\omega ,\omega _1)=0\) and minimal there. There is \(c\in \mathbb {N}\) such that for every \(A\in \mathbb {Z}[X][Y]\) of \(Y\)-degree less than \(d\), length at most \(b\) and \(X\)-degree at most \(e\), with \(A(\omega ,\omega _1)\neq 0\), there is a non-zero \(P\in \mathbb {Z}[X]\) of length at most \((cb)^{d}\) and degree at most \(d(e+c)\) with

\[ |P(\omega )|\le |A(\omega ,\omega _1)|\, \bigl(cb\max (1,|\omega |)^{e}\bigr)^{d}. \]

Source: The core of the proof of [ Wal73 , Lemme 7 ] .

LaTeX Lean

Lemma 2.3Scaled powers of an algebraic number

Let \(K\) be a field of characteristic zero and let \(\alpha \in K\) be algebraic over \(\mathbb {Q}\). There are \(\ell ,A\in \mathbb {N}\) and an integer \(L\neq 0\) such that for every \(n\in \mathbb {N}\) there are integers \(r_0,\dots ,r_{\ell -1}\) with \(|r_l|\le A^{n}\) and

\[ L^{n}\alpha ^{n}=\sum _{l\lt \ell }r_l\, \alpha ^{l}. \]

Source: Standard.

LaTeX Lean

Lemma 2.15The cofactor of an irreducible factor

Let \(P\in \mathbb {Z}[X]\) have positive degree and let \(\theta \in \mathbb {C}\). Then \(P=Q^{e}R\) with \(Q,R\in \mathbb {Z}[X]\), \(Q\) irreducible of positive degree, \(e\ge 1\), and

\[ 1\le 2^{\deg Q\deg R}M(Q)^{\deg R}M(R)^{\deg Q}|R(\theta )|. \]

Source: The multiplicative step of Gel’fond’s lemma [ Gel52 ] , as in [ Wal71 , § 3, Lemme 2 ] .

LaTeX Lean

Lemma 6.17Derivatives at a grid point, presented

Let \(x_1,x_2,y_1,y_2\in \mathbb {C}\) with every \(e^{x_iy_j}\) algebraic. Let \(\omega ,\omega _1\in \mathbb {C}\), let \(\varphi \) be evaluation at \((\omega ,\omega _1)\), and let \(D,E_i,G_j,H_{ij}\in \mathbb {Z}[X][Y]\) with \(\varphi (D)\neq 0\), \(x_i\varphi (D)=\varphi (E_i)\), \(y_j\varphi (D)=\varphi (G_j)\) and \(e^{x_iy_j}\varphi (D)=\varphi (H_{ij})\). There is \(c\in \mathbb {N}\) such that for all \(S,T,a,b,m\in \mathbb {N}\) there are \(\Lambda \in \mathbb {C}\), \(\Lambda \neq 0\), with \(|\Lambda |\le c^{\, c(1+m+S+T(a+b))}\), and \(P_{ijh}\in \mathbb {Z}[X][Y]\) (\(i\lt S\), \(j,h\lt T\)) of degree at most \(c(1+m+S)\) in \(X\) and in \(Y\) and of length at most

\[ c^{\, c(1+m+S+T(a+b))}\, (1+m+S+T+a+b)^{c(1+m+S)}, \]

such that for all \(f_{ijh}\in \mathbb {C}\)

\[ \Lambda \cdot \frac{d^{m}}{dz^{m}}\Bigl(\sum _{i,j,h}f_{ijh}\, z^{i}e^{(jx_1+hx_2)z}\Bigr)\Big|_{z=ay_1+by_2}=\sum _{i,j,h}f_{ijh}\, \varphi (P_{ijh}). \]

Source: A step of the proofs of [ Wal73 , Lemmes 4 and 7 ] .

LaTeX Lean

Lemma 7.3Derivatives at a grid point, one algebraic column

Let \(x_1,x_2,y_1,y_2\in \mathbb {C}\) with \(e^{x_1y_2}\) and \(e^{x_2y_2}\) algebraic, and let \(\omega ,\omega _1\), \(\varphi \) and \(D,E_i,G_j,H_{ij}\) be as in Lemma 6.17. There is \(c\in \mathbb {N}\) such that for all \(S,T,a,b,m\in \mathbb {N}\) there are \(\Lambda \neq 0\) with \(|\Lambda |\le c^{\, c(1+m+S+T(a+b))}\) and \(P_{ijh}\in \mathbb {Z}[X][Y]\) (\(i\lt S\), \(j,h\lt T\)), of degree at most \(c(1+m+S+Ta)\) in \(X\) and in \(Y\) and of length at most

\[ c^{\, c(1+m+S+T(a+b))}\, (1+m+S+T+a+b)^{c(1+m+S)}, \]

for which the identity of Lemma 6.17 holds for all \(f_{ijh}\in \mathbb {C}\).

Source: A step of the proofs of [ Wal73 , Lemmes 4 and 7 ] , pp. 197 and 200.

LaTeX Lean

Lemma 7.2Presentations from the exponential factor

Let \(x_1,x_2,y_1,y_2,\omega ,\omega _1\in \mathbb {C}\), let \(\varphi \) be evaluation at \((\omega ,\omega _1)\), and let \(D,E_i,G_j\in \mathbb {Z}[X][Y]\) with \(x_i\varphi (D)=\varphi (E_i)\) and \(y_j\varphi (D)=\varphi (G_j)\). There is \(c\in \mathbb {N}\) with the following property. Let \(S,T,a,b,m,L,\delta \in \mathbb {N}\) and \(\Lambda _1\in \mathbb {C}\), and let \(U_{jh}\in \mathbb {Z}[X][Y]\) (\(j,h\lt T\)), of length at most \(L\) and of degree at most \(\delta \) in \(X\) and in \(Y\), satisfy

\[ \varphi (U_{jh})=\Lambda _1\, e^{(jx_1+hx_2)(ay_1+by_2)}. \]

Then there are \(P_{ijh}\in \mathbb {Z}[X][Y]\) (\(i\lt S\), \(j,h\lt T\)), of length at most \(c^{c(1+m+S)}(1+m+S+T+a+b)^{c(1+m+S)}L\) and of degree at most \(c(1+m+S)+\delta \) in \(X\) and in \(Y\), such that for all \(f_{ijh}\in \mathbb {C}\)

\[ \varphi (D)^{m+S}\, \Lambda _1\cdot \frac{d^{m}}{dz^{m}}\Bigl(\sum _{i,j,h}f_{ijh}\, z^{i}e^{(jx_1+hx_2)z}\Bigr)\Big|_{z=ay_1+by_2}=\sum _{i,j,h}f_{ijh}\, \varphi (P_{ijh}). \]

Source: The presentation step that the proofs of [ Wal73 , Lemmes 4 and 7 ] share between the four exponentials case and the case of one algebraic column; the derivatives are expanded as in [ Wal73 , (7), p. 197 ] .

LaTeX Lean

Lemma 6.18Reduced presentations

In the setting of Lemma 6.17, let moreover \(Q\in \mathbb {Z}[X][Y]\) be monic in \(Y\) with \(\varphi (Q)=0\). There is \(c\in \mathbb {N}\) such that for all \(S,T,M,a,b,m\in \mathbb {N}\) there are \(\Lambda \neq 0\) with \(|\Lambda |\le c^{\, c(1+m+S+T(a+b))}\) and \(R_{ijh\mu \nu }\in \mathbb {Z}[X][Y]\) (\(i\lt S\), \(j,h\lt T\), \(\mu \lt M\), \(\nu \lt \deg _YQ\)) of \(Y\)-degree less than \(\deg _YQ\) and \(X\)-degree at most \(M+c(1+m+S)\), and of length at most

\[ c^{\, c(1+m+S+T(a+b))}\, (1+m+S+T+a+b)^{c(1+m+S)}, \]

such that for every integer array \(q\)

\[ \Lambda \, F_q^{(m)}(ay_1+by_2)=\varphi \Bigl(\sum _{i,j,h,\mu ,\nu }q(i,j,h,\mu ,\nu )\, R_{ijh\mu \nu }\Bigr), \]

where \(F_q\) is formed with \(T\) in place of \(2N\).

Source: A step of the proofs of [ Wal73 , Lemmes 4 and 7 ] .

LaTeX Lean

Lemma 7.4Reduced presentations, one algebraic column

In the setting of Lemma 7.3, let moreover \(Q\in \mathbb {Z}[X][Y]\) be monic in \(Y\) with \(\varphi (Q)=0\). Then the conclusion of Lemma 6.18 holds with the \(X\)-degree bound \(M+c(1+m+S+Ta)\) in place of \(M+c(1+m+S)\).

Source: A step of the proofs of [ Wal73 , Lemmes 4 and 7 ] , pp. 197 and 200.

LaTeX Lean

Lemma 2.13Reduction modulo a polynomial

Let \(Q\in \mathbb {Z}[X][Y]\). There is \(C\in \mathbb {N}\) such that for all \(b,e,n\in \mathbb {N}\) and every \(P\in \mathbb {Z}[X][Y]\) with \(L(P)\le b\), every coefficient of \(X\)-degree at most \(e\), and \(Y\)-degree at most \(n\), the remainder \(P\bmod Q\) of the division by \(Q\) in \(Y\) satisfies

\[ L(P\bmod Q)\le C^{n}b, \]

and every coefficient of \(P\bmod Q\) has \(X\)-degree at most \(e+Cn\). (When \(Q\) is not monic in \(Y\), the remainder is \(P\), as in Mathlib’s modByMonic.)

Source: Standard.

LaTeX Lean

Lemma 2.16A monic integral model

Let \(\omega \in \mathbb {C}\) be transcendental and let \(\theta \in \mathbb {C}\) be algebraic over \(\mathbb {Q}(\omega )\). There are \(\omega _1\in \mathbb {C}\) and \(Q\in \mathbb {Z}[X][Y]\), monic in \(Y\) of degree \(d\ge 1\), with \(Q(\omega ,\omega _1)=0\) and minimal there: no non-zero \(A\in \mathbb {Z}[X][Y]\) with \(\deg _YA\lt d\) vanishes at \((\omega ,\omega _1)\). Moreover \(\omega _1=v(\omega )\, \theta \) for some \(v\in \mathbb {Z}[X]\) with \(v(\omega )\neq 0\).

Source: Standard; the normalisation at the start of [ Wal73 , § III ] .

LaTeX Lean

Lemma 2.17One model for finitely many numbers

Let \(\omega \in \mathbb {C}\) be transcendental and let \((z_i)_{i\in I}\) be a finite family of complex numbers algebraic over \(\mathbb {Q}(\omega )\). There are \(\omega _1\in \mathbb {C}\) and \(Q\in \mathbb {Z}[X][Y]\), monic in \(Y\) of degree \(d\ge 1\), with \(Q(\omega ,\omega _1)=0\) and minimal there in the sense of Lemma 2.16, and \(D,E_i\in \mathbb {Z}[X][Y]\) with \(D(\omega ,\omega _1)\neq 0\) and

\[ z_i\, D(\omega ,\omega _1)=E_i(\omega ,\omega _1)\qquad \text{for every }i. \]

Source: Standard; the presentation used in [ Wal73 , § III ] .

LaTeX Lean

Lemma 6.16The size estimate

For all \(c,r\in \mathbb {N}\) there is \(\kappa \gt 0\) such that for all integers \(N\ge 3\) and \(S,T,a,b,m\in \mathbb {N}\) with

\[ S\le \frac{N^{2}}{\sqrt{\log N}},\quad m\le S,\quad T\le rN,\quad a\le r\frac{N}{\sqrt{\log N}},\quad b\le rN\sqrt{\log N}, \]

one has

\[ c^{\, c(1+m+S+T(a+b))}(1+m+S+T+a+b)^{c(1+m+S)}\le e^{\kappa N^{2}\sqrt{\log N}}. \]

Source: The parameter estimates in the proofs of [ Wal73 , Lemmes 4 and 7 ] .

LaTeX Lean

Lemma 9.21The parameters of the criterion

Let \(1\le n\lt 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\gt 0\) such that, with \(r=(c_y+2)S_1\) and \(R=Er\):

the four assumptions of Lemma 9.17 hold;
the inequality of Lemma 9.19 holds for every integer \(k\lt nET\);
the inequality of Lemma 9.20 holds for all integers \(u\ge ET\) and \(M\le 2nu\), with \(\rho '=c_FS_1u/T\).

Source: [ Wal00 , § 4.6: the conditions (4.15)–(4.19) and the choice of parameters in step 6, pp. 138–141 ] .

LaTeX Lean

Lemma 9.13Derivatives of one exponential monomial

Let \(K\) be a number field with an embedding \(\varphi \colon K\to \mathbb {C}\), let \(w\in K^{\iota }\), \(\tau \in \mathbb {N}\), \(k_0\in \iota \), and \(g(z)=z_{k_0}^{\tau }\exp \bigl(\sum _\nu \varphi (w_\nu )z_\nu \bigr)\). Let \(q\in \mathbb {C}^{\iota }\) and \(v\in K\), with \(\varphi (v)=q_{k_0}\) if \(\tau \gt 0\). Suppose that \(A\ge 1\), \(\overline{\left|w_\nu \right|}\le A\) for every \(\nu \), \(\overline{\left|v\right|}\le B\), and that \(\delta w_\nu \) and \(\delta v\) are algebraic integers for an integer \(\delta \). Then for every list \(L\) of \(k\) coordinate directions

\[ D_Lg(q)=\varphi (\gamma )\exp \Bigl(\sum _\nu \varphi (w_\nu )q_\nu \Bigr) \]

for some \(\gamma \in K\) with \(\overline{\left|\gamma \right|}\le A^{k}(B+k)^{\tau }\) and \(\delta ^{k+\tau }\gamma \) an algebraic integer.

Source: [ Wal00 , Lemma 4.9, p. 130 ] , in the form used in its §4.6.

LaTeX Lean

Lemma 9.15Derivatives at the grid points

Let \(K\) be a number field with an embedding \(\varphi \colon K\to \mathbb {C}\), let \(k_0\in \iota \), and let \(x_1,\dots ,x_{d_1}\) and \(y_j\) (\(j\in \iota \)) be vectors in \(\mathbb {C}^{\iota }\). Suppose that \(x_{i\nu }=\varphi (\xi _{i\nu })\) and \(e^{\langle x_i,y_j\rangle }=\varphi (a_{ij})\) with \(\xi _{i\nu },a_{ij}\in K\), and that \(\eta _j\in K\) satisfy \(\varphi (\eta _j)=y_{jk_0}\) if \(T_0\gt 0\). Suppose that an integer \(\delta \) makes every \(\delta \xi _{i\nu }\), \(\delta \eta _j\) and \(\delta a_{ij}\) an algebraic integer, and that all their houses are at most \(H\ge 1\). Let \(T_1\ge 1\) and \(X\in \mathbb {R}\), and let the coefficients \(p_{\tau ,t}\) be integers with \(|p_{\tau ,t}|\le X\). Then at every grid point \(\sum _js_jy_j\) and for every list \(L\) of \(k\) coordinate directions, \(D_LF_p\bigl(\sum _js_jy_j\bigr)=\varphi (\gamma )\) for some \(\gamma \in K\) with

\[ \overline{\left|\gamma \right|}\le (T_0+1)(T_1+1)^{d_1}X\, \bigl((d_1+1)T_1H\bigr)^{k}\, (nS_1H+k)^{T_0}\, H^{d_1nT_1S_1} \]

and \(\delta ^{k+T_0+d_1nT_1S_1}\gamma \) an algebraic integer.

Source: A step of [ Wal00 , § 4.6, step 2, p. 137 ] , with Lemma 4.9 (pp. 130–131).

LaTeX Lean

Lemma 9.16Liouville’s lower bound at the grid points

Let \(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. There is \(C\ge 1\) with the following property. Let \(T\ge 1\) and \(S_1\) be integers and \(N\ge 0\), and let \(F_p\), with \(T_0=d_0T\) and \(T_1=T\), have integer coefficients with \(|p_{\tau ,t}|\le e^{N}\). If \(\Delta =D_LF_p\bigl(\sum _js_jy_j\bigr)\neq 0\) for a list \(L\) of \(k\) coordinate directions and a grid point \(\sum _js_jy_j\), then

\[ \log |\Delta |\ge -C\bigl(N+k(1+\log T)+T(S_1+\log (1+k))\bigr). \]

Source: [ Wal00 , (4.14), § 4.6, step 2, p. 137 ] , with a bracket of a slightly different shape.

LaTeX Lean

Lemma 9.14Exponential monomials are independent

Let \(x_1,\dots ,x_{d_1}\in \mathbb {C}^{\iota }\) be linearly independent over \(\mathbb {Q}\), let \(k_0\in \iota \) and \(T_0,T_1\in \mathbb {N}\), and let the coefficients \(p_{\tau ,t}\in \mathbb {C}\) be not all zero. Then \(D^{k}F_p(0)\neq 0\) for some \(k\).

Source: [ Wal00 , Exercises 2.4–2.5, p. 60 ] , in the form used in its §4.6.

LaTeX Lean

Lemma 2.4Rational multiples of logarithms

Let \(u\in \mathbb {C}\) with \(e^{u}\) algebraic, and let \(a\in \mathbb {Q}\). Then \(e^{au}\) is algebraic.

Source: Standard.

LaTeX Lean

Lemma 2.9Cauchy’s estimate on a grid of zeros

Let \(y_1,\dots ,y_l\in \mathbb {C}\) be linearly independent over \(\mathbb {Q}\), and let \(F(z)=\sum _{k\in s}c_kz^{e_k}e^{\omega _kz}\) be a finite sum with \(|\omega _k|\le W\) and \(e_k\le E\) for all \(k\). Let \(t_j\le A_j\) (\(1\le j\le l\)) and \(n\) be natural numbers, and suppose that \(F^{(i)}\bigl(\sum _jm'_jy_j\bigr)=0\) for all \(i\lt n\) and all \(m'\in \mathbb {N}^{l}\) with \(m'_j\lt t_j\) for every \(j\). Let \(u\ge 2\) and \(Z\ge \bigl(\sum _jA_j|y_j|+1\bigr)(u+1)\). Then for every \(m\in \mathbb {N}^{l}\) with \(m_j\lt A_j\) for every \(j\), every \(r\in \mathbb {N}\) and \(w=\sum _jm_jy_j\),

\[ |F^{(r)}(w)|\le 2\, r!\, (u-1)^{-n\prod _jt_j}\Bigl(\sum _{k\in s}|c_k|\Bigr)Z^{E}e^{WZ}. \]

Source: The analytic step of the extrapolation in [ Wal73 , Lemme 5 ] and in the six exponentials theorem [ Lang66 , Ch. II ] ; it rests on [ Wal71 , § 4, (4.3) ] .

LaTeX Lean

Lemma 2.10Derivatives at a point

Let \(f(z)=\sum _{j\in J}P_j(z)e^{w_jz}\), over a finite set \(J\), with \(|w_j|\le W\) for some \(W\ge 0\), and each \(P_j\in \mathbb {C}[z]\) zero or of degree less than \(q_j\); put \(N=\sum _jq_j\). Let \(c\in \mathbb {C}\) and \(D\ge 0\). If \(|f^{(s)}(c)|\le D\) for every \(s\lt N\), then

\[ |f^{(n)}(c)|\le D\, (W+1)^{n+N}\qquad \text{for every }n\in \mathbb {N}. \]

The \(w_j\) need not be distinct.

Source: No source is claimed; an elementary induction.

LaTeX Lean

Lemma 2.6Distinct frequencies

Let \(\omega _1,\dots ,\omega _l\in \mathbb {C}\) be pairwise distinct, let \(q_1,\dots ,q_l\in \mathbb {N}\), and let \(b_{j,i}\in \mathbb {C}\) (\(1\le j\le l\), \(0\le i\lt q_j\)) be not all zero. Then the function

\[ f(z)=\sum _{j=1}^{l}\sum _{i=0}^{q_j-1}b_{j,i}\, z^{i}e^{\omega _jz} \]

takes a non-zero value at some point of \(\mathbb {C}\).

Source: Classical; see [ Tij71 ] or [ Wal71 , § 4 ] .

LaTeX Lean

Lemma 6.7Values from low-order derivatives

Let \(w_1,\dots ,w_l\in \mathbb {C}\) be pairwise distinct with \(|w_j|\le W\) for some \(W\ge 0\). For each \(j\) let \(P_j\in \mathbb {C}[z]\) be zero or of degree less than \(q_j\), and put \(g(z)=\sum _jP_j(z)e^{w_jz}\) and \(n=\sum _jq_j\). Let \(R\ge 0\). If \(|g^{(s)}(0)|\le D\) for every \(s\lt n\), then

\[ |g(u)|\le n\, (W+1)^{n+1}e^{R(W+1)}D\qquad \text{whenever }|u|\le R. \]

Source: [ Wal71 , § 4, (4.5)–(4.13) ] .

LaTeX Lean

Lemma 6.8The rescaled inequality

Let \(f(z)=\sum _{j=1}^{l}\sum _{i\lt q_j}b_{j,i}z^{i}e^{\omega _jz}\) with pairwise distinct \(\omega _j\) and \(b_{j,i}\) not all zero; put \(n=\sum _jq_j\) and \(\Omega =\max _j|\omega _j|\), and suppose \(\Omega \gt 0\). Let \(z_0\in \mathbb {C}\), \(\rho \ge 0\), let \(S\) be a finite set of points of the disc \(|z-z_0|\le \rho \), and put \(\sigma =\sum _{z\in S}\operatorname {ord}_zf\) and \(x=\rho \Omega \). Then for every \(R\gt x+1\)

\[ \sigma \log \frac{R-x}{x+1}\le \log \Bigl(n!\, 2^{n+1}\frac{R}{R-1}\Bigr)+2R. \]

Source: [ Wal71 , § 4, (4.14) ] and the rescaling that follows it.

LaTeX Lean

Lemma 2.7First non-vanishing derivative

Let \(F(z)=\sum _{i\in I}c_ie^{\rho _iz}\) be a finite exponential sum with pairwise distinct \(\rho _i\in \mathbb {C}\) and coefficients \(c_i\in \mathbb {C}\) not all zero. Let \(m\ge 1\) and \(n\in \mathbb {N}\), and suppose that \(F^{(k)}(j)=0\) for all \(j\in \{ 1,\dots ,m\} \) and \(k\lt n\). Then there are \(r\ge n\) and \(l_0\in \{ 1,\dots ,m\} \) with \(F^{(r)}(l_0)\neq 0\) and \(F^{(k)}(j)=0\) for all \(j\in \{ 1,\dots ,m\} \) and \(k\lt r\).

Source: Standard.

LaTeX Lean

Lemma 6.23Extrapolation

Let \(x_1,x_2\in \mathbb {C}\), let \(y_1,y_2\) be linearly independent over \(\mathbb {Q}\), and let \(\kappa \gt 0\). There are \(\kappa '\gt 0\) and \(N_0\) such that for every \(N\gt N_0\) and all coefficients with \(|c(i,j,h)|\le e^{\kappa N^{2}\sqrt{\log N}}\): if \(F^{(m)}(ay_1+by_2)=0\) for all \(a\lt t_1\), \(b\lt t_2\) and \(m\lt S\), then

\[ |F^{(s)}(ay_1+by_2)|\le \exp \bigl(-N^{4}\sqrt{\log N}/\kappa '\bigr)\qquad \text{for all }s\lt S',\ a\lt R_1,\ b\lt R_2. \]

Source: [ Wal73 , Lemme 5 ] .

LaTeX Lean

Lemma 6.22The numbers of the extrapolation

Let \(X\ge 0\), \(Y\ge 1\) and \(\kappa \ge 0\) be real, and let \(N,S,t_1,t_2,s\) be natural numbers with \(s\le S\) and \(N\ge 32(13+\kappa +\log Y+2XY)\). Write \(w=\sqrt{\log N}\) and suppose \(Sw\le N^{2}\le 2Sw\), \(N\le 2t_1w\) and \(Nw\le 2t_2\). Then

\[ 2\, s!\, (N-1)^{-t_1t_2S}\cdot S(2N)^{2}e^{\kappa N^{2}w}\, (YN^{2}w)^{S}\, e^{2NX\cdot YN^{2}w}\le e^{-N^{4}w/32}. \]

Source: The parameter estimate in the proof of [ Wal73 , Lemme 5 ] .

LaTeX Lean

Lemma 9.18Schwarz’s lemma at the grid points, then Cauchy

Let \(n=|\iota |\ge 1\) and let \((y_j)_{j\in \iota }\) be a basis of \(\mathbb {C}^{\iota }\). There is \(c\ge 1\) with the following property. Let \(F\) be an entire function on \(\mathbb {C}^{\iota }\), let \(S_0\), \(S_1\ge 1\) and \(M\ge nS_0\) be integers, and let \(\rho \ge 1\) and \(B\) be real numbers. Suppose that every derivative of \(F\) of total order less than \(M\) vanishes at every grid point, and that \(|F(w)|\le B\) whenever \(\| w\| \le cS_1\rho \). Then at every grid point and for every list \(L\) of \(M\) coordinate directions

\[ \Bigl|D_LF\Bigl(\sum _js_jy_j\Bigr)\Bigr|\le M!\cdot n\, \rho ^{-S_0S_1}B. \]

Source: [ Wal00 , § 4.6, step 5, p. 140 ] , with Proposition 4.7 (p. 122) and Cauchy’s inequalities (p. XVII).

LaTeX Lean

Lemma 6.1Height of a divisor

Let \(P\in \mathbb {Z}[X]\) be non-zero and let \(Q\in \mathbb {Z}[X]\) divide \(P\). If every coefficient of \(P\) has absolute value at most \(H\), then every coefficient of \(Q\) has absolute value at most \(e^{\deg P}H\).

Source: [ Wal71 , § 3, Lemme 1 ] (Gel’fond; a generalisation of a lemma of Popken and Koksma).

LaTeX Lean

Lemma 9.3Hermite interpolation

Let \(K\) be a field of characteristic \(0\), \(E\subset K\) a finite set and \(S_0\in \mathbb {N}\), and write \(q^{(k)}\) for the \(k\)-th formal derivative of \(q\in K[X]\). There are polynomials \(b_{\zeta ,k}\in K[X]\) (\(\zeta \in E\), \(0\le k\lt S_0\)) of degree less than \(|E|S_0\) such that, for \(\zeta '\in E\) and \(0\le k'\lt S_0\), \(b_{\zeta ,k}^{(k')}(\zeta ')\) is \(1\) if \((\zeta ',k')=(\zeta ,k)\) and \(0\) otherwise, and every \(q\in K[X]\) of degree less than \(|E|S_0\) satisfies

\[ q=\sum _{\zeta \in E}\ \sum _{k\lt S_0}q^{(k)}(\zeta )\, b_{\zeta ,k}. \]

Source: Standard (Hermite interpolation).

LaTeX Lean

Lemma 9.4Hermite division with bounds

Let \(0\lt r\) and \(5r\le R\), let \(Z\) be a finite multiset of complex numbers of modulus at most \(r\), put \(p=|Z|\) and \(P(x)=\prod _{\zeta \in Z}(x-\zeta )\), and let \(u\) be an entire function with \(|u|\le M\) on the closed disc of radius \(R\) about \(0\). Then \(u=\rho +Pq\) for a polynomial \(\rho \) of degree less than \(p\) and an entire function \(q\), such that \(\rho ^{(k)}(\zeta )=u^{(k)}(\zeta )\) whenever \(k\) is less than the multiplicity of \(\zeta \) in \(Z\), and for \(|x|\le R\)

\[ 2|\rho (x)|+M\le 3^{p}M,\qquad |q(x)|\le (3/R)^{p}M. \]

Source: [ Wal00 , Lemma 4.8 c)–d), p. 123 ] in one variable, with the bounds of Step 2.4 of its proof (pp. 125–126).

LaTeX Lean

Lemma 2.19A dependent pair

Let \(R\) be a commutative ring, \(A\) a commutative \(R\)-algebra and \(t\in A\) transcendental over \(R\). If \(t\) and \(z\in A\) are not algebraically independent over \(R\), then \(z\) is algebraic over the subalgebra \(R[t]\).

Source: Standard.

LaTeX Lean

Lemma 2.12Length of a product

For all \(P,Q\in \mathbb {Z}[X][Y]\), \(L(PQ)\le L(P)\, L(Q)\).

Source: Standard.

LaTeX Lean

Lemma 2.11Length of a sum

For every finite family \((f_i)_{i\in s}\) in \(\mathbb {Z}[X][Y]\),

\[ L\Bigl(\sum _{i\in s}f_i\Bigr)\le \sum _{i\in s}L(f_i). \]

Source: Standard.

LaTeX Lean

Lemma 2.1Liouville’s inequality, house form

Let \(K\) be a number field of degree \(d\), let \(\sigma \colon K\to \mathbb {C}\) be a field embedding, and let \(\alpha \in K\), \(\alpha \neq 0\). If \(c\alpha \) is an algebraic integer for some integer \(c\neq 0\), then

\[ 1\le |c|^{d}\, |\sigma (\alpha )|\, \overline{\left|\alpha \right|}^{\, d-1}. \]

Source: Standard (Liouville’s inequality).

LaTeX Lean

Lemma 10.11Conjugation keeps the logarithms

If \(\lambda \) is a logarithm of an algebraic number, so is \(\bar\lambda \).

Source: Elementary.

LaTeX Lean

Lemma 10.12Conjugation keeps \(\widetilde{\mathcal L}\)

The \(\overline{\mathbb {Q}}\)-vector space \(\widetilde{\mathcal L}\) spanned by \(1\) and the logarithms of algebraic numbers is closed under complex conjugation.

Source: Elementary; it is the stability that [ Dia04 , Théorème 2 ] uses.

LaTeX Lean

Lemma 4.8Gel’fond’s main estimate

Let \(K\) have degree \(h\), let \(l\in \mathbb {C}\), \(l\neq 0\), and let \(\beta \in \mathbb {C}\setminus \mathbb {Q}\), with \(\sigma (\alpha ')=e^{l}\), \(\sigma (\beta ')=\beta \) and \(\sigma (\gamma ')=e^{\beta l}\). There is \(C\ge 1\) such that for every \(N\in \mathbb {N}\) there is an integer \(r\ge \max (N,1)\) with

\[ r^{(r-3h)/2}\le C^{r}. \]

Source: A step of Gel’fond’s proof [ Gel34 ] .

LaTeX Lean

Lemma 6.13A non-zero derivative on the grid

Let \(x_1,x_2\) be linearly independent over \(\mathbb {Q}\), and likewise \(y_1,y_2\). Let \(S,T,R_1,R_2,S'\in \mathbb {N}\) and let \(c(i,j,h)\in \mathbb {C}\) (\(i\lt S\), \(j,h\lt T\)) be not all zero; put

\[ G(z)=\sum _{i\lt S}\sum _{j,h\lt T}c(i,j,h)\, z^{i}e^{(jx_1+hx_2)z},\qquad n=ST^{2}. \]

If for some \(\lambda \gt 0\)

\[ \frac{n}{\lambda }+2\, \frac{1+n^{\lambda }}{\lambda \log n}\Bigl(1+(R_1|y_1|+R_2|y_2|)\, T(|x_1|+|x_2|)\Bigr)\le R_1R_2S', \]

then \(G^{(s)}(ay_1+by_2)\neq 0\) for some \(a\lt R_1\), \(b\lt R_2\) and \(s\lt S'\).

Source: [ Wal73 , Lemme 6 ] , with the zero estimate [ Wal71 , § 4, Lemme 3 ] in place of Gel’fond’s zero lemma.

LaTeX Lean

Lemma 2.14Liouville’s inequality through the resultant

Let \(F,G\in \mathbb {C}[X]\) with \(M(F)\ge 1\) and \(M(G)\ge 1\). Then for every \(\theta \in \mathbb {C}\)

\[ |\operatorname {Res}(F,G)|\le 2^{\deg F\deg G}M(F)^{\deg G}M(G)^{\deg F}\max \bigl(|F(\theta )|,|G(\theta )|\bigr). \]

Source: [ RW97 , Corollary 3.7 ] , in the complex form of their Lemma 3.4; they describe the inequality as well known.

LaTeX Lean

Lemma 6.25From a small value to a small polynomial

Let \(x_1,x_2,y_1,y_2\in \mathbb {C}\) have presentation data, suppose every \(e^{x_iy_j}\) is algebraic, and let \(\kappa ,\kappa '\gt 0\). There is \(k\gt 0\) such that for every \(C\) there is \(N_0\) with the following property. Let \(N\gt N_0\), \(M\le \kappa S\), and let \(q(i,j,h,\mu ,\nu )\) be integers of absolute value at most \(e^{\kappa N^{2}\sqrt{\log N}}\). If \(a\lt R_1\), \(b\lt R_2\), \(s\lt S'\) and

\[ 0\lt |F_q^{(s)}(ay_1+by_2)|\le \exp \bigl(-N^{4}\sqrt{\log N}/\kappa '\bigr), \]

then some \(P\in \mathbb {Z}[X]\) is small at \(\omega \) for \((N,C)\) with respect to the growth functions of constant \(k\).

Source: [ Wal73 , Lemme 7 ] .

LaTeX Lean

Lemma 7.7A small polynomial, one algebraic column

Let \(x_1,x_2,y_1,y_2,\omega ,\omega _1\in \mathbb {C}\) and let \(Q\in \mathbb {Z}[X][Y]\) be monic in \(Y\) with \(Q(\omega ,\omega _1)=0\) and minimal there, and suppose that the derivatives of the functions \(F_q\) have reduced presentations as in the conclusion of Lemma 7.4. Then the conclusion of Lemma 6.25 holds.

Source: [ Wal73 , Lemme 7 ] , pp. 200–201.

LaTeX Lean

Lemma 13.13Algebraic modulus

Let \(u\neq 0\). Then \(|u|\) is algebraic if and only if \(u\bar u\) is, and then \(u\bar u=\rho \) for a positive real algebraic \(\rho \).

Source: Elementary.

LaTeX Lean

Lemma 13.12Rational multiples are dependent

Let \(u,v\in \mathbb {C}\) with \(u\bar u\) algebraic. If \(v=cu\) or \(v=c\bar u\) for some \(c\in \mathbb {Q}^{\times }\), then \(u\) and \(v\) are algebraically dependent over \(\mathbb {Q}\).

Source: Elementary.

LaTeX Lean

Lemma 9.1Partial derivatives along a list of directions

Let \(\mathbb {K}\) be a nontrivially normed field, \(F\) a normed space over \(\mathbb {K}\), and \(g\colon \mathbb {K}^{\iota }\to F\) a function of class \(C^{k}\). For \(i\in \iota \) and a function \(h\) on \(\mathbb {K}^{\iota }\), let \(\partial _ih(z)\) be the derivative at \(w=z_i\) of \(w\mapsto h(z[i:=w])\), where \(z[i:=w]\) is \(z\) with its coordinate \(z_i\) replaced by \(w\). Then for every list \(L\) of \(k\) coordinate directions and every \(z\in \mathbb {K}^{\iota }\)

\[ \partial _{L(0)}\, \partial _{L(1)}\cdots \partial _{L(k-1)}\, g(z)=D_Lg(z), \]

the partial derivative in the direction \(L(k-1)\) being taken first.

Source: Standard.

LaTeX Lean

Lemma 9.2Cauchy’s inequalities on a polydisc

Let \(F\) be an entire function on \(\mathbb {C}^{\iota }\) with \(|F|\le M\) on the closed polydisc of radius \(\rho \gt 0\) about \(p\). For a list \(L\) of \(k\) coordinate directions, let \(\sigma _\nu \) be the number of times \(\nu \) occurs in \(L\). Then

\[ |D_LF(p)|\le \Bigl(\prod _\nu \sigma _\nu !\Bigr)\frac{M}{\rho ^{k}}. \]

Source: Classical; in the form of [ Wal00 , p. XVII ] .

LaTeX Lean

Lemma 10.18Linear Cauchy–Davenport for polynomials

For non-zero finite-dimensional \(K\)-spaces \(X,Y\subseteq K[X]\), the span \(XY\) of the products satisfies \(\dim X+\dim Y\le \dim XY+1\).

Source: A case of the linear Cauchy–Davenport theorem of Eliahou and Lecouvey, as stated in [ BSZ17 , Theorem 2 ] .

LaTeX Lean

Lemma 10.17Orders at zero of a space of polynomials

Let \(K\) be a field and \(X\subseteq K[X]\) a finite-dimensional \(K\)-space. The orders at \(0\) of the non-zero elements of \(X\) take exactly \(\dim X\) values.

Source: Standard: the valuation argument of [ BSZ17 , proof of Theorem 33 ] .

LaTeX Lean

Lemma 10.29Three equal differences in \(\{ 0,\pm 1,\pm k,\pm l\} \)

For integers \(4\le k\lt l\), some difference occurs three times in \(\{ 0,\pm 1,\pm k,\pm l\} \) if and only if \(l\in \{ k+1,k+2,2k-1,2k,2k+1,3k\} \).

Source: Elementary.

LaTeX Lean

Lemma 10.15Separation for one number

Let \(K\subseteq F\) be subfields of \(\mathbb {C}\), \(V_0\subseteq F\) a \(K\)-space and \(w\) transcendental over \(F\). If \(x_1,x_2\) and \(y_1,y_2\) are each linearly independent over \(K\) and every \(x_iy_j\) lies in \(V_0+Kw\), then every \(x_iy_j\) lies in \(V_0\).

Source: Not found in the sources read; short (Chapter 14).

LaTeX Lean

Lemma 6.14A rank-one matrix of logarithms

Let \(l_{11},l_{12},l_{21},l_{22}\) be non-zero complex numbers with every \(e^{l_{ij}}\) algebraic, \(l_{11}l_{22}=l_{12}l_{21}\) and \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}[l_{11},l_{12},l_{21},l_{22}]\le 1\), and suppose that neither the rows nor the columns of \((l_{ij})\) are linearly dependent over \(\mathbb {Q}\). Then there are \(x_1,x_2,y_1,y_2\in \mathbb {C}\), with \(x_1,x_2\) linearly independent over \(\mathbb {Q}\) and likewise \(y_1,y_2\), such that every \(e^{x_iy_j}\) is algebraic and \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}[x_1,x_2,y_1,y_2]\le 1\).

Source: Elementary; as in [ Wal73 , § I ] .

LaTeX Lean

Lemma 4.5A common denominator

Let \(m\in \mathbb {N}\). There is an integer \(D\neq 0\) such that for all \(n,q,r,l_0\) with \(n\ge 1\), \(q^{2}=2mn\), \(n\le r\) and \(1\le l_0\le m\), and all \(\eta _{ab}\in \mathcal{O}_K\), the number

\[ D^{r}\sum _{a,b}\eta _{ab}(a+b\beta ')^{r}\alpha '^{\, al_0}\gamma '^{\, bl_0} \]

is an algebraic integer.

Source: A step of Gel’fond’s proof [ Gel34 ] .

LaTeX Lean

Lemma 4.6House of the first non-zero derivative

Let \(m\ge 1\) and \(C_0\ge 1\). There is \(C\ge 1\) such that whenever \(n\ge 1\), \(q^{2}=2mn\), \(n\le r\), \(1\le l_0\le m\), and \(\eta _{ab}\in \mathcal{O}_K\) satisfy \(\overline{\left|\eta _{ab}\right|}\le C_0^{n}n^{(n+1)/2}\),

\[ \overline{\left|\sum _{a,b}\eta _{ab}(a+b\beta ')^{r}\alpha '^{\, al_0}\gamma '^{\, bl_0}\right|}\le C^{r}r^{\, r+3/2}. \]

Source: A step of Gel’fond’s proof [ Gel34 ] .

LaTeX Lean

Lemma 9.20The inequality behind (4.19)

Let \(n\ge 1\) and \(d\) be integers, \(C\ge 1\), \(c_x\in \mathbb {R}\) and \(c_F\ge 1\). There is an integer \(s_0\) such that for every integer \(S_1\ge s_0\) there is \(e_0\) with the following property. Let \(T\ge 1\) and \(E\ge e_0\) be integers with \(\log T\le n\log S_1+n\log E\), and let \(U\) and \(N\) be as in Lemma 9.19. Then for all integers \(u\ge ET\) and \(M\le 2nu\), with \(\rho '=c_FS_1u/T\),

\[ \begin{aligned} & C\bigl(N+M(1+\log T)+T(S_1+\log (1+M))\bigr)+\log M!+\log n\\ & \qquad +d\log (T+1)+N+T\log \rho ’+c_xT\rho ’\lt uS_1\log (u/T). \end{aligned} \]

Source: [ Wal00 , § 4.6, step 6 and (4.19), pp. 140–141 ] .

LaTeX Lean

Lemma 9.19The inequality behind (4.17)

Let \(n\ge 1\) be an integer and \(C\ge 1\). There is an integer \(s_0\) such that for every integer \(S_1\ge s_0\) there is \(e_0\) with the following property. Let \(T\ge 1\) and \(E\ge e_0\) be integers with \(\log T\le n\log S_1+n\log E\), and put

\[ U=\frac{S_1ET\log E}{2C\cdot 6^{n+1}},\qquad N=\frac{U}{2C}. \]

Then for every integer \(k\lt nET\)

\[ C\bigl(N+k(1+\log T)+T(S_1+\log (1+k))\bigr)+\log k!\lt U. \]

Source: [ Wal00 , § 4.6, step 4 and (4.17), p. 139 ] .

LaTeX Lean

Lemma 6.20Solving the system

Let \(\omega ,\omega _1\in \mathbb {C}\) and \(Q\in \mathbb {Z}[X][Y]\) with \(d=\deg _YQ\ge 1\), such that no non-zero \(A\in \mathbb {Z}[X][Y]\) with \(\deg _YA\lt d\) vanishes at \((\omega ,\omega _1)\), and let \(\kappa _1\gt 0\). There is \(\kappa \ge \kappa _1\) such that for every large \(N\), every \(M\) with \(0\lt M\le \kappa _1S\), and every \(R\times U\) integer matrix \(B\) with \(U=S(2N)^{2}Md\), \(2R\le U\) and entries of absolute value at most \(e^{\kappa _1N^{2}\sqrt{\log N}}\), there is an integer vector \(q\) with \(Bq=0\) such that every \(|q(i,j,h,\mu ,\nu )|\le e^{\kappa N^{2}\sqrt{\log N}}\), some \(c_q(i,j,h)\neq 0\), and every \(|c_q(i,j,h)|\le e^{\kappa N^{2}\sqrt{\log N}}\).

Source: Siegel’s lemma [ Lang66 , Ch. I, § 2 ] , as used in [ Wal73 , Lemme 4 ] .

LaTeX Lean

Lemma 2.5Siegel’s lemma with an entrywise bound

Let \(A\) be an \(m\times n\) matrix with integer entries, where \(n\ge 1\) and \(2m\le n\), and suppose that every entry satisfies \(|A_{ab}|\le B\) for some real \(B\ge 1\). Then there is \(t\in \mathbb {Z}^{n}\), \(t\neq 0\), with \(At=0\) and \(|t_b|\le nB\) for every \(b\).

Source: Siegel’s lemma [ Lang66 , Ch. I, § 2 ] , in the form Mathlib states it for integer matrices.

LaTeX Lean

Lemma 9.10A small integer combination, parameters free

Let \(\Lambda \) be a finite set, \(L=|\Lambda |\), and let \(\varphi _\lambda \) (\(\lambda \in \Lambda \)) be entire functions on \(\mathbb {C}^{\iota }\) with \(|\varphi _\lambda |\le B_\lambda \) on the closed polydisc of radius \(R\) about \(0\) and \(\sum _\lambda B_\lambda \le C\), where \(C\gt 0\). Let \(0\lt r\lt R\), and let \(T\), \(X\) and \(\ell \ge 1\) be integers with \(\ell ^{2T^{n}}\lt (X+1)^{L}\). Then there are integers \(p_\lambda \), not all zero, with \(|p_\lambda |\le X\), such that on the closed polydisc of radius \(r\) about \(0\)

\[ \Bigl|\sum _\lambda p_\lambda \varphi _\lambda \Bigr|\le T^{n}\cdot \frac{2CX}{\ell }+\frac{XC(r/R)^{T}}{1-r/R}. \]

Source: [ Wal00 , § 4.5: Lemmas 4.11–4.13 and the proof of Proposition 4.10, pp. 132–136 ] , with \(T\), \(X\) and \(\ell \) left free.

LaTeX Lean

Lemma 9.11The parameters of Proposition 4.10

Let \(n\ge 1\) and \(L\) be integers and \(N,U,V,r,R\) real numbers with \(r\gt 0\), \(W=N+U+V\ge 12n^{2}\), \(er\le R\le re^{W/6}\) and

\[ (2W)^{n+1}\le L\, N\, \bigl(\log (R/r)\bigr)^{n}. \]

Then there are integers \(T\), \(X\) and \(\ell \ge 1\) with \(X\le e^{N}\) and \(\ell ^{2T^{n}}\lt (X+1)^{L}\) such that

\[ T^{n}\cdot \frac{2e^{U}X}{\ell }\le \frac34e^{-V},\qquad \frac{Xe^{U}(r/R)^{T}}{1-r/R}\le \frac14e^{-V}. \]

Source: The numerical part of the proof of [ Wal00 , Proposition 4.10, pp. 135–136 ] .

LaTeX Lean

Lemma 8.1Roy’s lemma

Let \(F\) be an infinite field and \(E\) a linear subspace of the \(n\times n\) matrices over \(F\), all of whose elements are singular. Then there are non-zero \(v,w\in F^{n}\) with

\[ w^{\mathsf T}Av=0\qquad \text{for every }A\in E. \]

Source: [ DK24 , Theorem 2.2 ] , with a proof communicated by D. Roy; a stronger form is [ Wal00 , Proposition 12.5 ] , credited there to Roy (1990).

LaTeX Lean

Lemma 6.2Gel’fond’s lemma

Let \(\alpha \in \mathbb {C}\) be transcendental and let \(P\in \mathbb {Z}[X]\) be primitive, with every coefficient of absolute value at most \(H\). Let \(n,\lambda \in \mathbb {R}\) with \(\deg P\le n\le \log H\) and \(\lambda \gt 6\). If \(|P(\alpha )|\lt H^{-\lambda n}\), then there are a primitive irreducible divisor \(Q\) of \(P\) and an integer \(s\ge 1\) with

\[ |Q(\alpha )|\lt H^{-(\lambda -6)n/s},\qquad \deg Q\le n/s, \]

and every coefficient of \(Q\) of absolute value at most \(H^{1/s}e^{2n/s}\).

Source: [ Wal71 , § 3, Lemme 2 ] , after Gel’fond [ Gel52 ] .

LaTeX Lean

Lemma 7.10One algebraic column gives small polynomials

Let \(x_1,x_2,y_1,y_2\) satisfy the column hypotheses. Then there are a transcendental \(\omega \in \mathbb {C}\), functions \(\sigma _1,\sigma _2\) and constants \(a_1,a_2\ge 1\) satisfying the hypotheses of Theorem 6.6, such that for every \(C\in \mathbb {R}\) there is \(N_0\) and for every \(N\gt N_0\) a polynomial \(P_N\in \mathbb {Z}[X]\) that is small at \(\omega \) for \((N,C)\) with respect to \(\sigma _1,\sigma _2\).

Source: [ Wal73 , Lemmes 4–7 ] , with the zero estimate [ Wal71 , § 4, Lemme 3 ] in place of Gel’fond’s zero lemma in Lemme 6.

LaTeX Lean

Lemma 6.30A counterexample gives small polynomials

Let \(l_{11},l_{12},l_{21},l_{22}\) be non-zero complex numbers with every \(e^{l_{ij}}\) algebraic, \(l_{11}l_{22}=l_{12}l_{21}\) and \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}[l_{11},l_{12},l_{21},l_{22}]\le 1\), and suppose that neither the rows nor the columns of \((l_{ij})\) are linearly dependent over \(\mathbb {Q}\). Then there are a transcendental \(\omega \in \mathbb {C}\), functions \(\sigma _1,\sigma _2\) and constants \(a_1,a_2\ge 1\) satisfying the hypotheses of Theorem 6.6, such that for every \(C\in \mathbb {R}\) there is \(N_0\) and for every \(N\gt N_0\) a polynomial \(P_N\in \mathbb {Z}[X]\) that is small at \(\omega \) for \((N,C)\) with respect to \(\sigma _1,\sigma _2\).

Source: [ Wal73 , § III, Lemmes 4–7 ] , with the zero estimate of [ Wal71 , § 4, Lemme 3 ] ; see also [ Bro74 ] .

LaTeX Lean

Lemma 4.2Entries of the linear system

Let \(m\ge 1\). There is \(C\ge 1\) such that for all \(n\ge 1\) and \(q\) with \(q^{2}=2mn\), all \(1\le a,b\le q\), \(1\le j\le m\) and \(k\lt n\),

\[ \overline{\left|(a+b\beta ')^{k}\alpha '^{\, aj}\gamma '^{\, bj}\right|}\le C^{n}n^{(n-1)/2}. \]

Source: A step of Gel’fond’s proof [ Gel34 ] .

LaTeX Lean

Lemma 9.9Taylor coefficients as linear forms

Let \(\Lambda \) be a finite set, let \(\varphi _\lambda \) (\(\lambda \in \Lambda \)) be entire functions on \(\mathbb {C}^{\iota }\) with \(|\varphi _\lambda |\le B_\lambda \) on the closed polydisc of radius \(r\gt 0\) about \(0\), and let \(T\in \mathbb {N}\). There are \(u_{\tau \lambda }\in \mathbb {C}\), for \(\lambda \in \Lambda \) and \(\tau \in \{ 0,\dots ,T-1\} ^{\iota }\), with \(|u_{\tau \lambda }|\le B_\lambda \), such that for all \(c\in \mathbb {C}^{\Lambda }\) and \(z\in \mathbb {C}^{\iota }\) the function \(F=\sum _\lambda c_\lambda \varphi _\lambda \) satisfies

\[ \sum _{k\lt T}\frac{1}{k!}\, D^{k}F(0)(z,\dots ,z)=\sum _{\tau }\Bigl(\sum _\lambda u_{\tau \lambda }c_\lambda \Bigr)\prod _{\nu \in \iota }\Bigl(\frac{z_\nu }{r}\Bigr)^{\tau _\nu }. \]

Source: A step of the proof of [ Wal00 , Proposition 4.10, p. 135 ] , with Cauchy’s inequalities (p. XVII).

LaTeX Lean

Lemma 9.8The tail of a Taylor series

Let \(E\) be a complex normed space and \(G\colon E\to \mathbb {C}\) analytic at every point, with \(|G|\le M\) on the closed ball of radius \(R\) about \(0\), and let \(0\lt r\lt R\). For every \(z\in E\) with \(\| z\| \le r\) and every \(T\in \mathbb {N}\)

\[ \Bigl|G(z)-\sum _{k\lt T}\frac{1}{k!}\, D^{k}G(0)(z,\dots ,z)\Bigr|\le \frac{M(r/R)^{T}}{1-r/R}. \]

Source: The tail bound in the proof of [ Wal00 , Lemma 4.13, pp. 134–135 ] , with \(1/(1-r/R)\) in place of \(1+\sqrt{T}\).

LaTeX Lean

Lemma 9.7Thue–Siegel’s lemma for real linear forms

Let \(J\) and \(\Lambda \) be finite sets, \(\mu =|J|\) and \(\nu =|\Lambda |\), and let \(v_{j\lambda }\in \mathbb {R}\) with \(\sum _\lambda |v_{j\lambda }|\le C\) for every \(j\), where \(C\gt 0\). Let \(X\ge 0\) and \(\ell \ge 1\) be integers with \(\ell ^{\mu }\lt (X+1)^{\nu }\). Then there is \(\xi \in \mathbb {Z}^{\Lambda }\), \(\xi \neq 0\), with \(|\xi _\lambda |\le X\) for every \(\lambda \) and

\[ \Bigl|\sum _\lambda v_{j\lambda }\xi _\lambda \Bigr|\le \frac{CX}{\ell }\qquad (j\in J). \]

Source: [ Wal00 , Lemma 4.11, pp. 132–133 ] , with any real \(C\gt 0\) in place of an integer.

LaTeX Lean

Lemma 6.5The criterion for continuous growth functions

Let \(\alpha \in \mathbb {C}\) and \(\varepsilon \gt 0\). Let \(\sigma _1,\sigma _2\colon \mathbb {R}\to \mathbb {R}\) be continuous, strictly increasing and tending to \(+\infty \), and let \(a_1,a_2\ge 1\) be such that for every \(x\ge 1\)

\[ \sigma _2(x)\le \sigma _1(x),\qquad \sigma _i(x+1)\le a_i\, \sigma _i(x)\quad (i=1,2). \]

Put \(C=\max \{ 10+\varepsilon ,(4+\varepsilon )a_1a_2\} \). Suppose that for every integer \(N\gt N_0\) there is a non-zero \(P_N\in \mathbb {Z}[X]\) with every coefficient of absolute value at most \(e^{\sigma _1(N)}\), \(\deg P_N\le \sigma _2(N)\) and \(|P_N(\alpha )|\lt e^{-C\sigma _1(N)\sigma _2(N)}\). Then \(\alpha \) is algebraic.

Source: [ Wal71 , § 3, Lemme fondamental ] and its proof, where continuity of the \(\sigma _i\) is assumed without loss of generality.

LaTeX Lean

Lemma 2.18Transcendence degree at most one

Let \(K\subseteq L\) be fields, \(x\in L\), and \(S\subseteq L\) a set each of whose elements is algebraic over the ring \(K[x]\). Then the \(K\)-algebra \(K[S]\) generated by \(S\) has transcendence degree at most one over \(K\).

Source: Standard.

LaTeX Lean

Lemma 6.15Presenting the field

Let \(x_1,x_2\) be linearly independent over \(\mathbb {Q}\), and likewise \(y_1,y_2\). If every \(e^{x_iy_j}\) is algebraic and \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}[x_1,x_2,y_1,y_2]\le 1\), then \(x_1,x_2,y_1,y_2\) have presentation data.

Source: The opening of [ Wal73 , § III ] .

LaTeX Lean

Lemma 7.1Presenting the field, one algebraic column

If \(x_1,x_2,y_1,y_2\) satisfy the column hypotheses, then they have presentation data.

Source: The reduction to \(\omega \) in the proof of the Théorème, [ Wal73 , p. 196 ] .

LaTeX Lean

Lemma 10.2A configuration in dimension four is a progression

Let \(V\subseteq \mathbb {C}\) be a \(\overline{\mathbb {Q}}\)-vector subspace of dimension at most \(4\), and let \(x_1,x_2\) and \(y_1,y_2,y_3\) be linearly independent over \(\overline{\mathbb {Q}}\) with all six products \(x_iy_j\) in \(V\). Then

\[ V=\overline{\mathbb {Q}}\, b+\overline{\mathbb {Q}}\, bh+\overline{\mathbb {Q}}\, bh^{2}+\overline{\mathbb {Q}}\, bh^{3} \]

for some \(b\neq 0\) and \(h\notin \overline{\mathbb {Q}}\).

Source: The converse direction, that such a progression carries a configuration, is used in [ Fis01 , Lemma 6.1 ] and [ Dia07 , Théorème 7(2) ] . This direction was not found in the sources read.

LaTeX Lean

Lemma 10.24Three products: a progression

Let \(x_1,x_2\) and \(y_1,y_2\) be pairs, each linearly independent over a subfield \(K\subseteq \mathbb {C}\), whose four products span a \(K\)-space of dimension \(3\). Then \(\operatorname {span}(x_1,x_2)=Ka+Kah\) and \(\operatorname {span}(y_1,y_2)=Kb+Kbh\) for some \(h\notin K\) and \(a,b\neq 0\).

Source: The dimension-2 case of [ BSZ17 , Lemmas 4–5 ] , stated there for a base field algebraically closed in the extension; here over any subfield.

LaTeX Lean

Lemma 10.27Sumsets with two summands

A finite \(S\subseteq \mathbb {Z}\) contains \(A+B\) with \(|A|=2\), \(|B|=q\) if and only if some \(d\gt 0\) has \(\# \{ s\in S:s+d\in S\} \ge q\).

Source: Elementary.

LaTeX Lean

Lemma 6.9From the rescaled inequality to the count

Let \(n\ge 2\) be an integer and let \(x\ge 0\), \(\lambda \gt 0\) and \(\sigma \ge 0\) be real. If for every \(R\gt x+1\)

\[ \sigma \log \frac{R-x}{x+1}\le \log \Bigl(n!\, 2^{n+1}\frac{R}{R-1}\Bigr)+2R, \]

then

\[ \sigma \lt \frac{n}{\lambda }+2\, \frac{1+n^{\lambda }}{\lambda \log n}\, (1+x). \]

Source: After [ Wal71 , § 4, (4.14) ] .

LaTeX Lean

Lemma 6.10Few zeros beat the bound

For every integer \(n\ge 1\), real \(x\ge 0\) and \(\lambda \gt 0\), and every integer \(0\le \sigma \le n-1\),

\[ \sigma \lt \frac{n}{\lambda }+2\, \frac{1+n^{\lambda }}{\lambda \log n}\, (1+x), \]

where for \(n=1\) the second term is read as \(0\).

Source: Elementary.

LaTeX Lean

Lemma 6.11The degenerate cases

Let \(f\), \(n\) and \(\Omega \) be as in Lemma 6.8, without the hypothesis \(\Omega \gt 0\), and suppose that \(n\le 1\) or \(\Omega =0\). Then for every finite set \(S\subset \mathbb {C}\)

\[ \sum _{z\in S}\operatorname {ord}_zf\le n-1. \]

Source: Elementary; the degenerate cases of [ Wal71 , § 4, Lemme 3 ] .

LaTeX Lean

Proposition 13.20Kirby’s weak form at a candidate

Assume the case \(n=2\) of Kirby’s weak Schanuel conjecture [ Kir18 , Conjecture 1.5 ] : if \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(a,b,e^{a},e^{b})\lt 2\), then \(ma+nb\in 2\pi i\mathbb {Z}\) for some integers \((m,n)\neq (0,0)\). Then every candidate \(u\) has \(\operatorname {Re}u\neq 0\) and \(\operatorname {Im}u\in \pi \mathbb {Q}^{\times }\).

Source: Not found in the sources read; short (Chapter 14). It is not the “weak Schanuel” of Calegari and Mazur, which is the algebraic independence of logarithms.

LaTeX Lean

Proposition 10.7Two families of five-dimensional spaces that carry a configuration

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) with \(\rho =u\bar u\) algebraic, let \(a\in \overline{\mathbb {Q}}\), \(a\neq 0\), and let \(z=u/(u^{2}-a)\) if \(a\bar a\neq \rho ^{2}\), or \(z=u/(u^{2}-a)^{2}\) if \(a\bar a=\rho ^{2}\). Then there are \(x_1,x_2\), linearly independent over \(\overline{\mathbb {Q}}\), and \(y_1,y_2,y_3\), linearly independent over \(\overline{\mathbb {Q}}\), with all six products \(x_iy_j\) in \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}z+\overline{\mathbb {Q}}\bar z\).

Source: Rescaled, the configuration is the one in the proofs of [ Dia04 , Théorème 2 ] and [ Dia07 , Théorèmes 6(1) and 7(1) ] , and the progression of [ Fis01 , Lemma 6.1 ] .

LaTeX Lean

Proposition 10.5Three spaces that carry a configuration

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) with \(u\bar u\) algebraic, and let \(w\) be \(u^{2}\), \(\bar u^{2}\), or \(1/(u-a)\) with \(a\in \overline{\mathbb {Q}}\), \(a\neq 0\). Then there are \(x_1,x_2\), linearly independent over \(\overline{\mathbb {Q}}\), and \(y_1,y_2,y_3\), linearly independent over \(\overline{\mathbb {Q}}\), with all six products \(x_iy_j\) in \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}w\).

Source: The configurations behind [ Dia07 , Corollaire 5(1) and 5(4) ] , used there with Roy’s strong six exponentials theorem [ Roy92 ] .

LaTeX Lean

Proposition 10.33Two poles carry a configuration

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) with \(\rho =u\bar u\) algebraic, \(a_1\neq a_2\) non-zero algebraic numbers, \(z_i=u/(u^{2}-a_i)\) and \(W=\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}z_1+\overline{\mathbb {Q}}z_2\). Then \(W\) carries a \(2\times 3\) configuration: \(x=(1,u^{2})\), \(y=(b,bu^{2},bu^{4})\) with \(b=1/(u(u^{2}-a_1)(u^{2}-a_2))\).

Source: The progression of [ Fis01 , Lemma 6.1 ] and [ Dia07 , Théorème 7(2) ] , with ratio \(u^{2}\).

LaTeX Lean

Proposition 10.10The conjugation-stable case carries none

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) with \(\rho =u\bar u\) algebraic, and let \(a\in \overline{\mathbb {Q}}\), \(a\neq 0\), with \(a\bar a=\rho ^{2}\). Then there are no \(x_1,x_2\), linearly independent over \(\overline{\mathbb {Q}}\), and \(y_1,y_2,y_3\), linearly independent over \(\overline{\mathbb {Q}}\), with all six products \(x_iy_j\) in \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}\, u/(u^{2}-a)\).

Source: A consequence of Theorem 10.9. It is where the hypotheses of [ Dia04 , Théorème 2 ] and of [ Dia07 , Corollaire 4(4) and Théorème 7(1) ] fail for this family.

LaTeX Lean

Proposition 10.31The powers \(u^{4^j}\)

Let \(u\) be transcendental over a subfield \(K\subseteq \mathbb {C}\). The span of the \(u^s\), \(s\in \{ 0,\pm 1\} \cup \{ \pm 4^j:j\ge 1\} \), carries no \(2\times 3\) configuration. So at a candidate, Roy’s theorem used through Laurent hulls cannot exclude \(u^{4^j}\in \widetilde{\mathcal L}\) for all \(j\).

Source: Not found in the sources read; short (Chapter 14). Not in [ Dia07 ] (p. 390) nor [ Fis01 ] .

LaTeX Lean

Proposition 13.8No geometric triple of logarithms

Let \(w\neq 0\) and \(z\notin \mathbb {Q}\) with \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(w,z)\le 1\). Then \(w\), \(wz\) and \(wz^{2}\) are not all in \(\mathcal L\).

Source: A step of Theorem 13.9.

LaTeX Lean

Proposition 13.2Purely imaginary products of logarithms

Let \(\lambda ,\mu \in \mathcal L\setminus \{ 0\} \) with \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(\lambda ,\mu ,\bar\lambda ,\bar\mu )\le 1\). If \(\lambda \mu \) is purely imaginary, then one of \(\lambda ,\mu \) is real and the other purely imaginary.

Source: A step of Theorem 13.3.

LaTeX Lean

Proposition 13.1Real products of logarithms

Let \(\lambda ,\mu \in \mathcal L\setminus \{ 0\} \) with \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(\lambda ,\mu ,\bar\lambda ,\bar\mu )\le 1\). If \(\lambda \mu \) is real, then \(\lambda \) and \(\mu \) are both real, or both purely imaginary, or \(\mu \in \mathbb {Q}\bar\lambda \).

Source: A step of Theorem 13.3.

LaTeX Lean

Proposition 10.30Pairs of powers

Let \(u\) be transcendental over a subfield \(K\subseteq \mathbb {C}\) and \(4\le k\lt l\). The span of the \(u^s\), \(s\in \{ 0,\pm 1,\pm k,\pm l\} \), carries a \(2\times 3\) configuration if and only if \(l\in \{ k+1,k+2,2k-1,2k,2k+1,3k\} \).

Source: Not found in the sources read; short (Chapter 14). The exclusions it gives at a candidate are substitutions in [ Dia07 ] (Corollary 10.32).

LaTeX Lean

Proposition 10.19Configurations in a space of rational functions

Let \(u\) be transcendental over a subfield \(K\subseteq \mathbb {C}\) and \(V_0\subseteq K(u)\) a finite-dimensional \(K\)-space. Every \(p\times q\) configuration over \(K\) in \(V_0\) has \(p+q\le \dim V_0+1\).

Source: Not found in the sources read; short (Chapter 14).

LaTeX Lean

Proposition 11.1A rational quadratic relation between \(t\) and \(\pi \)

Let \(t\neq 0\) be real with \(e^{t}\) algebraic, and let \(a,b,c\in \mathbb {Q}\) with \(a\neq 0\) and \(at^{2}+b\pi ^{2}=c\). Then \(e^{i\gamma /\pi }\) is transcendental for every \(\gamma \in \mathbb {Q}\), \(\gamma \neq 0\).

Source: Brownawell’s Corollary 5 [ Bro74 , p. 23 ] at \(\eta =t/\pi \), followed by rational scaling. The statement for general \(a,b\) was not found in the sources read.

LaTeX Lean

Proposition 9.12Thue–Siegel: a small auxiliary function

Let \(n=|\iota |\ge 1\), let \(\Lambda \) be a finite set, and let \(\varphi _\lambda \) (\(\lambda \in \Lambda \)) be entire functions on \(\mathbb {C}^{\iota }\). Let \(N,U,V,r\gt 0\) and \(R\) be real numbers with \(W=N+U+V\ge 12n^{2}\) and \(er\le R\le re^{W/6}\). Suppose that \(|\varphi _\lambda |\le B_\lambda \) on the closed polydisc of radius \(R\) about \(0\), with \(\sum _\lambda B_\lambda \le e^{U}\), and that

\[ (2W)^{n+1}\le |\Lambda |\, N\, \bigl(\log (R/r)\bigr)^{n}. \]

Then there are integers \(p_\lambda \), not all zero, with \(|p_\lambda |\le e^{N}\), such that \(\bigl|\sum _\lambda p_\lambda \varphi _\lambda \bigr|\le e^{-V}\) on the closed polydisc of radius \(r\) about \(0\).

Source: [ Wal00 , Proposition 4.10 with Lemmas 4.11–4.13, pp. 131–136 ] .

LaTeX Lean

Theorem 9.24Baker’s theorem

Let \(\ell _1,\dots ,\ell _n\) be logarithms of algebraic numbers, linearly independent over \(\mathbb {Q}\), and let \(\beta _0,\beta _1,\dots ,\beta _n\) be algebraic numbers, not all zero. Then

\[ \beta _0+\beta _1\ell _1+\dots +\beta _n\ell _n\neq 0. \]

Equivalently, \(1,\ell _1,\dots ,\ell _n\) are linearly independent over \(\overline{\mathbb {Q}}\).

Source: Baker [ Bak66 ] ; see [ Bak75 , Theorem 2.1 ] . The route is that of Bertrand–Masser [ BM80 ] , as in [ Wal00 , Chapter 4 ] .

LaTeX Lean

Theorem 9.23Baker’s theorem for a basis of a number field

Let \(K\subset \mathbb {C}\) be a number field, \((\beta _k)\) a basis of \(K\) over \(\mathbb {Q}\), and \(\ell _k\) logarithms of algebraic numbers. If \(\sum _k\beta _k\ell _k\) is algebraic, then \(\ell _k=0\) for every \(k\).

Source: [ Wal00 , Theorem 4.5 with Lemma 4.6, pp. 119–121 ] ; the route is that of Bertrand–Masser [ BM80 ] and Masser [ Mas81 ] .

LaTeX Lean

Theorem 13.18Mixed rigidity

Let \(u\) be a candidate and \(\mu \in \mathcal L\) with \(\mu \notin \mathbb {Q}u\cup \mathbb {Q}\bar u\). Then \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(u,\mu ,e^{u\bar u/\mu })\ge 2\).

Source: From the author’s unpublished manuscript on the conjecture; it is [ Wal73 , Corollaire 4 ] at \((u,\bar u,\mu )\).

LaTeX Lean

Theorem 9.6Schwarz’s lemma for Cartesian products

Let \(n\ge 1\) and let \(f\) be an entire function on \(\mathbb {C}^{n}\). Let \(E_1,\dots ,E_n\) be sets of \(S_1\) complex numbers each, all of modulus at most \(r\gt 0\), and let \(R\ge 5r\). Suppose that \(|f|\le M\) on the closed polydisc of radius \(R\) about \(0\), and that every derivative of \(f\) of total order less than \(nS_0\) vanishes at every point of \(E_1\times \dots \times E_n\). Then on the closed polydisc of radius \(r\) about \(0\)

\[ |f|\le n\Bigl(\frac{2\cdot 3^{n}r}{R}\Bigr)^{S_0S_1}M. \]

Source: [ Wal00 , Proposition 4.7, pp. 122–130 ] , in the form used in its §4.6, with \(2\cdot 3^{n}\) in place of \(18^{n}\).

LaTeX Lean

Theorem 10.9Configurations invisible to the four-dimensional extensions

With \(u\), \(a\) and \(z\) as in Proposition 10.7, put \(H_0=\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u\) and \(W=H_0+\overline{\mathbb {Q}}z+\overline{\mathbb {Q}}\bar z\). Then \(W\) carries a configuration, but for no \(w\in W\setminus H_0\) does \(H_0+\overline{\mathbb {Q}}w\) carry one.

Source: Not found in the sources read, but short (Chapter 14). The shape of the configuration is printed; see Proposition 10.7.

LaTeX Lean

Theorem 10.6The four-dimensional extensions that carry a configuration

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) with \(u\bar u\) algebraic, put \(H_0=\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u\), and let \(z\notin H_0\). There are \(x_1,x_2\), linearly independent over \(\overline{\mathbb {Q}}\), and \(y_1,y_2,y_3\), linearly independent over \(\overline{\mathbb {Q}}\), with all six products \(x_iy_j\) in \(H_0+\overline{\mathbb {Q}}z\) if and only if \(z\in H_0+\overline{\mathbb {Q}}w\) for \(w=u^{2}\), \(w=\bar u^{2}\), or \(w=1/(u-a)\) with \(a\in \overline{\mathbb {Q}}\), \(a\neq 0\).

Source: Not found in the sources read, and not routine (Chapter 14). With Roy’s strong six exponentials theorem [ Roy92 ] , the “if” direction gives at a candidate the exclusions of [ Dia07 , Corollaire 5(1) and 5(4) ] ; every configuration has the shape of [ Fis01 , Lemma 6.1 ] and [ Dia07 , Théorème 7(2) ] .

LaTeX Lean

Theorem 10.22The normal form

Let \(u\) be transcendental over a subfield \(K\subseteq \mathbb {C}\) with \(\rho =u\bar u\in K\). Then \(x_1,x_2\) and \(y_1,y_2\) form a \(2\times 2\) configuration over \(K\) in \(K+Ku+K\bar u\) if and only if \(x_i=\mu (P_{i1}+P_{i2}u)\) and \(y_j=\mu ^{-1}(Q_{1j}+Q_{2j}\bar u)\) for some \(\mu \neq 0\) and invertible \(P,Q\in K^{2\times 2}\): the configurations form the orbit of \((1,u)\otimes (1,\bar u)\) under \(\mathrm{GL}_2(K)\times \mathrm{GL}_2(K)\).

Source: Not found in the sources read, and not routine (Chapter 14).

LaTeX Lean

Theorem 10.35Invisible to four-dimensional extensions

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) with \(\rho =u\bar u\) algebraic, \(a_1\neq a_2\) non-zero algebraic numbers, \(z_i=u/(u^{2}-a_i)\) and \(W=\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}z_1+\overline{\mathbb {Q}}z_2\). Then \(W\) carries a \(2\times 3\) configuration, but no \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}w\) with \(w\in W\) outside \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u\) does.

Source: Not found in the sources read; short (Chapter 14). It drops the conjugation condition of Theorem 10.9.

LaTeX Lean

Theorem 12.6The only singular pencil

Let \(K\subseteq \mathbb {C}\) be a subfield, let \(u\neq 0\) be transcendental over \(K\) with \(u\bar u\in K\), and let \(A,B,C\) be \(2\times 2\) matrices over \(K\) with \(\det (A+uB+\bar uC)=0\). Then there is \(c\in K\) with

\[ \det (xA+yB+zC)=c\, \bigl(yz-(u\bar u)\, x^{2}\bigr)\qquad \text{for all }x,y,z\in \mathbb {C}. \]

Source: Not found in the sources read, and not routine (Chapter 14). Roy has neither this classification nor Theorem 12.5; the nearest printed passage is [ Roy95 , § 3.2, p. 65 ] .

LaTeX Lean

Theorem 13.3Diaz’s (Qr2) in transcendence degree one

Let \(\ell _0,\ell _1\in \mathcal L\), neither real nor purely imaginary, with \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(\ell _0,\ell _1,\bar\ell _0,\bar\ell _1)\le 1\). If \(\ell _1/\ell _0\) is real or purely imaginary, then \(\ell _1/\ell _0\in \mathbb {Q}\).

Source: Not found in the sources read, but short (Chapter 14). The statement is Diaz’s conjecture (Qr2) [ Dia07 , p. 376 ] , here in transcendence degree one; Diaz derives (Qr2) from the four exponentials conjecture with the same matrix [ Dia07 , p. 377 ] . It is one substitution in [ Bro74 , Corollary 7 ] , at \((\ell _1/\ell _0,\bar\ell _0/\ell _0,\ell _0)\).

LaTeX Lean

Theorem 13.9Three transcendental exponentials

Let \(t\neq 0\) be real with \(e^{t}\) algebraic, and suppose that \(\rho =t^{2}+\pi ^{2}\) is algebraic. Then \(e^{it^{2}/\pi }\), \(e^{\pi ^{2}/t}\) and \(e^{\rho /(i\pi )}\) are transcendental.

Source: The first number is [ Bro74 , Corollary 5 ] at \(\eta =t/\pi \).

LaTeX Lean

Theorem 13.11The strong five exponentials conjecture implies Diaz’s

Assume Waldschmidt’s strong five exponentials conjecture: if \(x_1,x_2\) are linearly independent over \(\mathbb {Q}\), \(y_1,y_2\) are linearly independent over \(\mathbb {Q}\), \(\eta \neq 0\), the \(\alpha _{ij}\) and \(\beta \) are algebraic, and the five numbers \(e^{x_iy_j-\alpha _{ij}}\) and \(e^{\eta x_2/x_1-\beta }\) are algebraic, then \(x_iy_j=\alpha _{ij}\) for all \(i,j\) and \(\eta x_2=\beta x_1\). Then for every \(u\neq 0\) with \(|u|\) algebraic, \(e^{u}\) is transcendental.

Source: Not found in the sources read, but short (Chapter 14): the derivation is one line. The conjecture is [ Wal04 , Conjecture 3.5 ] .

LaTeX Lean

Theorem 4.10Transcendence of \(e^{\pi }\)

The number \(e^{\pi }\) is transcendental.

Source: Gel’fond (1929).

LaTeX Lean

Theorem 7.12Schneider’s eighth problem

At least one of the numbers \(e^{e}\) and \(e^{e^{2}}\) is transcendental.

Source: The problem: Schneider [ Sch57 ] , as quoted in [ Wal73 , p. 191 ] . The solution: [ Wal73 , p. 192 ] , the case \(r=1\) of the solution of Schneider’s problem, deduced from Corollaire 1; found independently by Brownawell [ Bro74 ] .

LaTeX Lean

Theorem 6.12Zeros of an exponential polynomial in a disc

\[ f(z)=\sum _{j=1}^{l}\sum _{i=0}^{q_j-1}b_{j,i}\, z^{i}e^{\omega _jz},\qquad n=\sum _jq_j,\qquad \Omega =\max _j|\omega _j|. \]

Let \(z_0\in \mathbb {C}\), \(\rho \ge 0\) and \(\lambda \gt 0\). Then for every finite set \(S\) of points of the disc \(|z-z_0|\le \rho \)

\[ \sum _{z\in S}\operatorname {ord}_zf\lt \frac{n}{\lambda }+2\, \frac{1+n^{\lambda }}{\lambda \log n}\, (1+\rho \Omega ), \]

where for \(n=1\) the second term is read as \(0\). No separation between the \(\omega _j\) is assumed.

Source: [ Wal71 , § 4, Lemme 3, (4.2) ] ; compare [ Tij71 ] .

LaTeX Lean

Theorem 6.31Four exponentials in transcendence degree one

Let \(l_{11},l_{12},l_{21},l_{22}\) be non-zero logarithms of algebraic numbers with

\[ l_{11}l_{22}=l_{12}l_{21},\qquad \operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(l_{11},l_{12},l_{21},l_{22})\le 1. \]

Then the two rows, or the two columns, of \(\begin{pmatrix} l_{11} & l_{12} \\ l_{21} & l_{22} \end{pmatrix}\) are linearly dependent over \(\mathbb {Q}\). Equivalently, if \(x_1,x_2\) and \(y_1,y_2\) are pairs of complex numbers linearly independent over \(\mathbb {Q}\) and the four products \(x_iy_j\) are logarithms of algebraic numbers, then \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(x_1,x_2,y_1,y_2)\ge 2\).

Source: Waldschmidt [ Wal73 , Cor. 4 ] and Brownawell [ Bro74 , Cor. 7 ] ; stated in this form as [ RW95 , Theorem 1 ] .

LaTeX Lean

Theorem 4.9Gelfond–Schneider

Let \(l\in \mathbb {C}\), \(l\neq 0\), with \(e^{l}\) algebraic, and let \(\beta \) be an algebraic number that is not rational. Then \(e^{\beta l}\) is transcendental.

Source: Gel’fond [ Gel34 ] and Schneider [ Sch34 ] , Hilbert’s seventh problem; see [ Bak75 , Theorem 2.1 ] .

LaTeX Lean

Theorem 10.1No configuration on generic data

Let \(u\neq 0\) with \(u\bar u\) algebraic, and let \(w_1,\dots ,w_m\in \mathbb {C}\) be such that \(u,w_1,\dots ,w_m\) are algebraically independent over \(\overline{\mathbb {Q}}\). Then there are no \(x_1,x_2\), linearly independent over \(\overline{\mathbb {Q}}\), and \(y_1,y_2,y_3\), linearly independent over \(\overline{\mathbb {Q}}\), with all six products \(x_iy_j\) in \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\sum _j\overline{\mathbb {Q}}w_j\).

Source: Not found in the sources read, and not routine (Chapter 14). The case \(m=0\) is [ Roy95 , Theorem 3.4 ] and [ Wal00 , Lemma 12.16 and Exercise 12.10 ] ; see also [ Roy95 , § 3.2 ] and [ Fis01 , p. 186 ] . The general statement was not found in the sources read.

LaTeX Lean

Theorem 12.3The period never enters

Let \(u\neq 0\) with \(\rho =u\bar u\) algebraic, and suppose that \(u\) and \(i\pi \) are algebraically independent over \(\overline{\mathbb {Q}}\). Let \(M\) be a singular \(2\times 2\) matrix with entries \(c_{ij0}+c_{ij1}u+c_{ij2}\bar u+c_{ij3}\, i\pi \), \(c_{ijk}\) algebraic, whose rows are linearly independent over \(\overline{\mathbb {Q}}\) and whose columns are linearly independent over \(\overline{\mathbb {Q}}\). Then \(c_{ij3}=0\) for all \(i,j\): the coefficient of \(i\pi \) vanishes in every entry.

Source: Not found in the sources read, and not routine (Chapter 14). No source read considers the triple \((u,\bar u,i\pi )\).

LaTeX Lean

Theorem 12.2Every quadratic relation is the norm form

Let \(u\neq 0\) with \(\rho =u\bar u\) algebraic, and suppose that \(u\) and \(i\pi \) are algebraically independent over \(\overline{\mathbb {Q}}\). Every quadratic form with algebraic coefficients that vanishes at \((1,u,\bar u,i\pi )\) is an algebraic multiple of \(X_1X_2-\rho X_0^{2}\).

Source: Not found in the sources read, and not routine (Chapter 14). No source read considers the triple \((u,\bar u,i\pi )\).

LaTeX Lean

Theorem 3.3Hermite–Lindemann, logarithmic form

Let \(u\in \mathbb {C}\), \(u\neq 0\), with \(e^{u}\) algebraic. Then \(u\) is transcendental.

Source: Hermite [ Her1873 ] , Lindemann [ Lin1882 ] ; see [ Bak75 , Theorem 1.4 ] .

LaTeX Lean

Theorem 3.2Hermite–Lindemann

If \(a\) is a non-zero algebraic number, then \(e^{a}\) is transcendental.

Source: Hermite [ Her1873 ] for \(a=1\), Lindemann [ Lin1882 ] in general; see [ Bak75 , Theorem 1.4 ] .

LaTeX Lean

Theorem 10.28Configurations in Laurent hulls

A \(p\times q\) configuration over \(K\) in a \(K\)-space \(V\subseteq \mathbb {C}\) is a pair of families \(x_1,\dots ,x_p\) and \(y_1,\dots ,y_q\), each linearly independent over \(K\), with every product \(x_iy_j\) in \(V\).

Let \(u\) be transcendental over a subfield \(K\subseteq \mathbb {C}\) and \(S\subseteq \mathbb {Z}\) finite. The \(K\)-span of the \(u^s\), \(s\in S\), carries a \(p\times q\) configuration (\(p,q\ge 1\)) if and only if \(A+B\subseteq S\) for some \(|A|=p\), \(|B|=q\).

Source: Not found in the sources read, and not routine (Chapter 14). Theorem 10.14 is the case \(S=\{ 0,\pm 1,\pm k\} \); the nearest printed result is [ Fis01 , Lemma 6.1 ] .

LaTeX Lean

Theorem 13.19One relation

The following are equivalent: (i) for every \(u\neq 0\) off both axes with \(|u|\) algebraic, \(e^{u}\) real and \(e^{u}\neq 1\), \(e^{u}\) is transcendental; (ii) for every real \(t\neq 0\) with \(e^{t}\) algebraic, \(t^{2}+\pi ^{2}\) is transcendental.

Source: Elementary, from the quantisation of the imaginary part.

LaTeX Lean

Theorem 3.1Lindemann–Weierstrass

Let \(\alpha _1,\dots ,\alpha _n\) be pairwise distinct algebraic numbers. Then \(e^{\alpha _1},\dots ,e^{\alpha _n}\) are linearly independent over \(\overline{\mathbb {Q}}\): if \(\beta _1,\dots ,\beta _n\in \overline{\mathbb {Q}}\) are not all zero, then \(\sum _i\beta _ie^{\alpha _i}\neq 0\).
If algebraic numbers \(\alpha _1,\dots ,\alpha _n\) are linearly independent over \(\mathbb {Q}\), then \(e^{\alpha _1},\dots ,e^{\alpha _n}\) are algebraically independent over \(\overline{\mathbb {Q}}\).

(The Lean statements take families indexed by any type; in (b) they ask for linear independence over \(\mathbb {N}\), which for a family in a \(\mathbb {Q}\)-vector space is the same.)

Source: Lindemann [ Lin1882 ] , Weierstrass [ Wei1885 ] ; see [ Bak75 , Theorem 1.4 ] .

LaTeX

Lean

linearIndependent_exp
algebraicIndependent_exp

Theorem 13.4Pair rigidity in transcendence degree one

Let \(u,v\in \mathcal L\setminus \{ 0\} \) with \(|u|^{2}/|v|^{2}\in \mathbb {Q}\) and \(\operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}(u,v,\bar u,\bar v)\le 1\). Then \(v\in \mathbb {Q}u\) or \(v\in \mathbb {Q}\bar u\).

Source: Not found in the sources read, but short (Chapter 14). It is [ Bro74 , Corollary 7 ] at \((v/u,c\bar v/u,u)\), word for word.

LaTeX Lean

Theorem 12.5No vanishing coefficient

Let \(K\subseteq \mathbb {C}\) be a subfield, \(r\in K\), and \(u\notin K\) with \(u\bar u=r^{2}\), and put \(H=\begin{pmatrix} u & r \\ r & \bar u \end{pmatrix}\). Then \(w^{\mathsf T}Hv\neq 0\) for all non-zero \(w,v\in K^{2}\).

Source: Not found in the sources read, and not routine (Chapter 14). The nearest printed passage is [ Roy95 , § 3.2, p. 65 ] : Roy’s rank method cannot exclude points of \(xy=z^{2}\) with \(\overline{\mathbb {Q}}\)-free coordinates, and \((u,\bar u,r)\) is such a point; see also [ Fis01 , p. 186 ] .

LaTeX Lean

Theorem 10.14Configurations in the power hulls

Let \(u\in \mathbb {C}\setminus \overline{\mathbb {Q}}\) and \(k\ge 1\). There are \(x_1,x_2\), linearly independent over \(\overline{\mathbb {Q}}\), and \(y_1,y_2,y_3\), linearly independent over \(\overline{\mathbb {Q}}\), with all six products \(x_iy_j\) in \(\overline{\mathbb {Q}}u^{-k}+\overline{\mathbb {Q}}u^{-1}+\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}u^{k}\) if and only if \(k=2\) or \(k=3\).

Source: Not found in the sources read, and not routine (Chapter 14). For \(k=2,3\) the configurations are geometric progressions of four elements, which [ Fis01 , Lemma 6.1 ] and [ Dia07 , Théorème 7(2) ] exclude from \(\widetilde{\mathcal L}\) with Roy’s theorem; at a candidate they give [ Dia07 , Corollaire 5(1) and 5(2) ] . The direction “only for \(k=2,3\)” was not found; Diaz remarks that inside that theorem one cannot hope to go very far [ Dia07 , p. 390 ] .

LaTeX Lean

Theorem 10.16Separation

Let \(K\subseteq F\) be subfields of \(\mathbb {C}\), \(V_0\subseteq F\) a \(K\)-space and \(w_1,\dots ,w_m\) algebraically independent over \(F\). Every \(p\times q\) configuration over \(K\) with \(p,q\ge 2\) in \(V_0+Kw_1+\dots +Kw_m\) lies in \(V_0\).

Source: Not found in the sources read, and not routine (Chapter 14). It contains the separation steps of Theorems 10.1 and 12.3, which are over \(\overline{\mathbb {Q}}\).

LaTeX Lean

Theorem 9.22The criterion of Schneider–Lang

Let \(x_1,\dots ,x_{d_1}\in \mathbb {C}^{\iota }\) have algebraic coordinates and be linearly independent over \(\mathbb {Q}\), and let \((y_j)_{j\in \iota }\) be a basis of \(\mathbb {C}^{\iota }\). Either let \(d_0=0\), or let \(d_0=1\) and fix a coordinate \(k\) such that every \(y_{jk}\) is algebraic. If \(|\iota |\lt d_0+d_1\), then the numbers

\[ e^{\langle x_i,y_j\rangle }\qquad (1\le i\le d_1,\ j\in \iota ) \]

are not all algebraic.

Source: Schneider (1949), Lang [ Lang66 ] ; this form is [ Wal00 , Corollary 4.2, p. 117 ] for \(d_0\le 1\), proved directly as in its §4.6 (pp. 136–141), on the route of Bertrand–Masser [ BM80 ] and Masser [ Mas81 ] .

LaTeX Lean

Theorem 5.5The six exponentials theorem

Let \(x_1,x_2\) be complex numbers linearly independent over \(\mathbb {Q}\), and let \(y_1,y_2,y_3\) be complex numbers linearly independent over \(\mathbb {Q}\). Then at least one of the six numbers \(e^{x_iy_j}\) (\(i=1,2\), \(j=1,2,3\)) is transcendental.

Source: Lang [ Lang66 , Ch. II ] , Ramachandra [ Ram68 ] ; see [ Wal00 , § 1.3, Theorem 1.12 ] .

LaTeX Lean

Theorem 5.4Six exponentials over a number field

Let \(d,l\in \mathbb {N}\) with \(d+l\lt dl\), let \(x_1,\dots ,x_d\) and \(y_1,\dots ,y_l\) be complex numbers, each family linearly independent over \(\mathbb {Q}\), and let \(K\) be a number field. Then some \(e^{x_iy_j}\) does not lie in \(K\).

Source: [ Lang66 , Ch. II ] , [ Ram68 ] ; see [ Wal00 , Theorem 1.12 ] .

LaTeX Lean

Theorem 6.6Waldschmidt’s transcendence criterion

Let \(\alpha \in \mathbb {C}\) and \(\varepsilon \gt 0\). Let \(\sigma _1,\sigma _2\colon \mathbb {R}\to \mathbb {R}\) be strictly increasing and tending to \(+\infty \), and let \(a_1,a_2\ge 1\) be such that for every \(x\gt 0\)

\[ \sigma _2(x)\le \sigma _1(x),\qquad \sigma _i(x+1)\le a_i\, \sigma _i(x)\quad (i=1,2). \]

Source: [ Wal71 , § 3, Lemme fondamental ] , with constant \(a_i\) as in Remark 2 there; a refinement of Gel’fond’s criterion [ Gel52 , Ch. III, § 4, Lemma VII ] .

LaTeX Lean

Theorem 7.11Waldschmidt 1973

Let \(x_1,x_2\) be complex numbers linearly independent over \(\mathbb {Q}\), and \(y_1,y_2\) complex numbers linearly independent over \(\mathbb {Q}\). If \(e^{x_1y_2}\) and \(e^{x_2y_2}\) are algebraic, then two of the eight numbers

\[ x_1,\ x_2,\ y_1,\ y_2,\ e^{x_1y_1},\ e^{x_1y_2},\ e^{x_2y_1},\ e^{x_2y_2} \]

are algebraically independent over \(\mathbb {Q}\).

Source: Waldschmidt [ Wal73 , Théorème, p. 192 ] ; found independently by Brownawell [ Bro74 ] .

LaTeX Lean