The Gelfond–Schneider theorem for real numbers

This file proves the Gelfond–Schneider theorem in the real case: if α > 0 and β are real algebraic numbers with α ≠ 1 and β irrational, then α ^ β = exp (β log α) is transcendental (TauCeti.transcendental_rpow).

The proof is Schneider's. Suppose that γ = α ^ β is algebraic, and let K = ℚ(α, β, γ) ⊂ ℝ, a number field of degree d. For an integer M ≥ 2 put L = 2 d M², D₁ = (2 d)² M³ and D₂ = 2 d M, so that D₁ D₂ = 2 d L². Siegel's lemma gives integers a_{ij}, not all zero, such that the auxiliary function F(z) = ∑_{i < D₁, j < D₂} a_{ij} z ^ i exp (j z log α) vanishes at the L² points u + v β, 1 ≤ u, v ≤ L (RingHom.exists_schneider_auxiliary). On the larger grid 1 ≤ u, v ≤ 2 d L:

• F(u + v β) is the image of an element y_{uv} of K whose house is at most exp (O (L ^ (3 / 2) log L)) and which becomes an algebraic integer after multiplication by an integer of size exp (O (L ^ (3 / 2))) (TauCeti.exists_house_schneider_value_le_exp_rpow, TauCeti.isIntegral_intCast_pow_mul_schneider_value, TauCeti.exists_abs_pow_schneider_exponent_le_exp_rpow);
• |F(u + v β)| ≤ exp (O (L ^ (3 / 2) log L) - L ²) by Schwarz's lemma (TauCeti.exists_norm_schneider_auxiliary_le_exp_rpow).

By Liouville's inequality (NumberField.eq_zero_of_norm_le_exp_of_house_le_exp), these bounds force y_{uv} = 0 once M is large. Then the real exponential polynomial F has (2 d L)² real zeros, whereas it has at most D₁ D₂ - 1 = 2 d L² - 1 of them (TauCeti.card_lt_of_sum_eval_mul_exp_eq_zero); this is the contradiction.

Main results

• TauCeti.transcendental_rpow: the Gelfond–Schneider theorem for Real.rpow.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 4, §4.4, Theorem 4.21 and its proof.

theorem TauCeti.transcendental_rpow {α β : ℝ} (hα : IsAlgebraic ℚ α) (hβ : IsAlgebraic ℚ β) (h0 : 0 < α) (h1 : α ≠ 1) (hirr : Irrational β) : Transcendental ℚ (α ^ β)

The Gelfond–Schneider theorem for real numbers (Evertse, Theorem 4.21). If α > 0 and β are real algebraic numbers with α ≠ 1 and β irrational, then α ^ β is transcendental.