4 Gelfond–Schneider

The Gelfond–Schneider theorem in logarithmic form, by Gel’fond’s method, and the transcendence of \(e^{\pi }\). The Lean proof restructures the formalisation of M. Karatarakis and F. Wiedijk [ KW26 ] (Apache 2.0), which the library first carried as a single module of 5,388 lines. It is now a tree of eleven results, 1,409 lines in all: two tools of Chapter 2, Lemmas 2.1 and 2.7; the eight steps of Gel’fond’s method below; and Theorem 4.9. Lemma 4.7 goes through the grid estimate of Lemma 2.9, which the four exponentials development shares.

Unless said otherwise, \(K\) is a number field, \(\sigma \colon K\to \mathbb {C}\) a field embedding and \(\alpha ',\beta ',\gamma '\in K\); sums over \(a,b\) run over \(1\le a,b\le q\).

Lemma 4.1 One 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 ] .

Proof ▶

Take \(K=\mathbb {Q}(e^{l},\beta ,e^{\beta l})\) and its inclusion in \(\mathbb {C}\).

Lemma 4.2 Entries 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 ] .

Proof ▶

Lemma 4.3 Gel’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 ] .

Proof ▶

There are \(q^{2}=2mn\) unknowns and \(mn\) equations, so Mathlib’s Siegel lemma over \(\mathcal{O}_K\) applies with exponent one once denominators are cleared; Lemma 4.2 bounds the entries.

Lemma 4.4 Derivatives 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 ] .

Proof ▶

Differentiate term by term: \(e^{(a+b\beta )lj}=\sigma (\alpha '^{\, aj}\gamma '^{\, bj})\).

Lemma 4.5 A 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 ] .

Proof ▶

The powers of \(\alpha '\), \(\beta '\) and \(\gamma '\) that occur have exponents at most linear in \(r\), since \(q\le q^{2}=2mn\le 2mr\).

Lemma 4.6 House 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 ] .

Proof ▶

Lemma 4.7 Upper 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 ] .

Proof ▶

Lemma 2.9 for \(F(z)=E(z+1)\) on the one-dimensional grid \(\{ 0,\dots ,m-1\} \), with vanishing order \(r\), at the point \(l_0-1\) and with \(u=2+r/q\). The zeros at all of \(1,\dots ,m\), \(l_0\) included, give the factor \((u-1)^{-mr}\), and \(1/(u-1)\le q/r\le \sqrt{2m}\, r^{-1/2}\) turns it into \(r^{-rm/2}\) up to a factor \(C^{r}\).

Lemma 4.8 Gel’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 ] .

Proof ▶

Take \(m=2h+2\) and the auxiliary function of Lemma 4.3; its frequencies are distinct because \(\beta \notin \mathbb {Q}\). Lemma 2.7 gives a first non-zero derivative \(E^{(r)}(l_0)\), which by Lemma 4.4 is \(l^{r}\) times the image of an element of \(K\). Lemmas 4.5, 4.6 and 2.1 bound it from below, and Lemma 4.7 from above.

Theorem 4.9 Gelfond–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 ] .

Proof ▶

If \(e^{\beta l}\) were algebraic, Lemma 4.1 would put \(e^{l}\), \(\beta \) and \(e^{\beta l}\) in one number field, and Lemma 4.8 would give \(r^{(r-3h)/2}\le C^{r}\) for arbitrarily large \(r\), which is false.

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

✓

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

Source: Gel’fond (1929).

Proof ▶

Theorem 4.9 with \(l=i\pi \) and \(\beta =-i\): \(e^{i\pi }=-1\) is algebraic, and \(e^{\beta l}=e^{\pi }\).