Transcendence theory in Lean 4

7 Waldschmidt 1973 in full, and Schneider’s eighth problem

Waldschmidt’s Théorème of 1973 (Theorem 7.11): if one column \(e^{x_1y_2}\), \(e^{x_2y_2}\) of the four exponentials is algebraic, then two of the eight numbers \(x_i\), \(y_j\), \(e^{x_iy_j}\) are algebraically independent. Brownawell found it independently. Its proof reuses 33 results of the four exponentials development unchanged. The lemmas below carry the column case, where \(e^{x_1y_1}\) and \(e^{x_2y_1}\) are only algebraic over \(\mathbb {Q}(\omega )\), so that their powers cost degree in \(\omega \); they are sampled along the short side of the interpolation grid, where the degree budget absorbs them. Schneider’s eighth problem, which gave the 1973 paper its title, follows (Theorem 7.12).

The notation is that of Chapter 6. The column hypotheses on \(x_1,x_2,y_1,y_2\in \mathbb {C}\) are: \(x_1,x_2\) are linearly independent over \(\mathbb {Q}\), and so are \(y_1,y_2\); \(e^{x_1y_2}\) and \(e^{x_2y_2}\) are algebraic; and

\[ \operatorname {trdeg}_{\mathbb {Q}}\mathbb {Q}[x_1,x_2,y_1,y_2,e^{x_1y_1},e^{x_2y_1}]\le 1. \]

7.1 One algebraic column

Lemma 7.1 Presenting 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 ] .

Proof ▶

Take \(\omega =x_1y_2\), which is transcendental by Theorem 3.2. All eight numbers are algebraic over \(\mathbb {Q}(\omega )\), and Lemma 2.17 presents them at once.

Lemma 7.2 Presentations 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 ] .

Proof ▶

Leibniz’s rule; \(\varphi (D)^{m+S}\) clears the denominators of \(jx_1+hx_2\) and of the powers of \(ay_1+by_2\). Lengths are tracked with Lemmas 2.11 and 2.12.

Lemma 7.3 Derivatives 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.

Proof ▶

At \(ay_1+by_2\) the exponential factor is \((e^{x_1y_1})^{ja}(e^{x_1y_2})^{jb}(e^{x_2y_1})^{ha}(e^{x_2y_2})^{hb}\). The powers of the algebraic column reduce through integer relations (Lemma 2.3) and cost only height; the powers of \(e^{x_1y_1}\) and \(e^{x_2y_1}\), written through \(H_{11}\) and \(H_{21}\), cost degree proportional to \(Ta\). Lemma 7.2 does the rest.

Lemma 7.4 Reduced 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.

Proof ▶

From Lemma 7.3, reducing modulo \(Q\) with Lemma 2.13.

Lemma 7.5 The 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.

Proof ▶

As for Lemma 6.19, with the bounds of Lemma 6.16. Since \(a\lt t_1\) gives \(Ta\le 2Nt_1\le 2S\), a larger multiple of \(S\) for \(M\) still leaves twice as many unknowns as equations.

Lemma 7.6 The 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.

Proof ▶

Lemma 7.5, then Lemma 6.20.

Lemma 7.7 A 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.

Proof ▶

As for Lemma 6.25, with the norm of Lemma 6.24. Since \(a\lt R_1\) gives \(2Na\le 28N^{2}/\sqrt{\log N}\), the \(X\)-degree stays \(O(N^{2}/\sqrt{\log N})\) and only the constant \(k\) grows.

Lemma 7.8 The 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.

Proof ▶

Lemmas 7.1, 7.4, 7.6, 6.23 and 7.7, in this order. The numbers \(e^{x_1y_1}\) and \(e^{x_2y_1}\) are read only at the short index \(a\) of the grid.

Lemma 7.9 The 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 ] .

Proof ▶

Lemma 7.8, with the growth functions of Lemma 6.27 and the count of Lemma 6.28.

Lemma 7.10 One 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.

Proof ▶

Lemma 7.9, with a non-zero derivative supplied by Lemma 6.13.

7.2 The theorems

Theorem 7.11 Waldschmidt 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 ] .

Proof ▶

Suppose not. One of \(x_1\), \(y_2\) is transcendental by Theorem 3.2, since \(x_1y_2\neq 0\) and \(e^{x_1y_2}\) is algebraic. Lemma 2.19 makes all eight numbers algebraic over the ring it generates, so by Lemma 2.18 the column hypotheses hold. Lemma 7.10 then gives polynomials too small at a transcendental number, which Theorem 6.6 makes algebraic.

Theorem 7.12 Schneider’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 ] .

Proof ▶

The number \(e=e^{1}\) is transcendental by Theorem 3.2. Apply Theorem 7.11 at \(x=y=(1,e)\): the column \(y_2=e\) carries \(e^{e}\) and \(e^{e^{2}}\), and if both were algebraic, all eight numbers would be algebraic over \(\mathbb {Q}[e]\), of transcendence degree one by Lemma 2.18.