Hermite–Lindemann and Gel'fond–Schneider for ℒ_u = ℒ + ℚu + ℚū (u transcendental over the field of ℒ̃, uū algebraic): 0 is its only algebraic element, and l, βl ∈ ℒ_u, l ≠ 0, β ∈ Q̄ force β ∈ ℚ

Proved

DiazModulus.logAlg_adjoin_circle_point_hermite_lindemann_gelfond_schneider

by carlok · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theorytranscendence

Here $\mathcal{L}$ is the set of logarithms of algebraic numbers (the $z \in \mathbb{C}$ with $e^z$ algebraic), and $\widetilde{\mathcal{L}}$ is the $\overline{\mathbb{Q}}$ -vector space spanned by $1$ and $\mathcal{L}$ . Let $F$ be the subfield of $\mathbb{C}$ generated by $\widetilde{\mathcal{L}}$ , that is, by $\overline{\mathbb{Q}}$ and $\mathcal{L}$ . Let $u \in \mathbb{C}$ be transcendental over $F$ , with $u\bar u$ algebraic, and put $\mathcal{L}_u = \mathrm{span}_{\mathbb{Q}}(\mathcal{L}) + \mathrm{span}_{\mathbb{Q}}(u, \bar u)$ ; as $\mathcal{L}$ is a $\mathbb{Q}$ -vector space, this is $\mathcal{L} + \mathbb{Q}u + \mathbb{Q}\bar u$ . Then:

(Hermite–Lindemann) every algebraic $z \in \mathcal{L}_u$ is $0$ ;
(Gel'fond–Schneider) if $l_0 \neq 0$ and $\beta l_0$ both lie in $\mathcal{L}_u$ and $\beta$ is algebraic, then $\beta \in \mathbb{Q}$ .

Proof. Both clauses are special cases of Baker's theorem for $\mathcal{L}_u$ (DiazModulus.logAlg_adjoin_circle_point_baker_linear_forms). Hermite–Lindemann is the case $n = 1$ : a non-zero algebraic $z \in \mathcal{L}_u$ is $\mathbb{Q}$ -independent on its own, and $-z + 1 \cdot z = 0$ is a vanishing form with algebraic coefficients, not all zero. Gel'fond–Schneider is the case $n = 2$ , $b_0 = 0$ : if $\beta$ is not rational, then $(l_0, \beta l_0)$ is $\mathbb{Q}$ -independent, since $sl_0 + t\beta l_0 = 0$ with $t \neq 0$ would make $\beta = -s/t$ rational, and $\beta \cdot l_0 - 1 \cdot (\beta l_0) = 0$ is again forbidden.

Novelty. With $\mathcal{L}_u$ in place of $\mathcal{L}$ , this is the Hermite–Lindemann theorem together with the Gel'fond–Schneider theorem (1934), both derived here from Baker's theorem for $\mathcal{L}_u$ . Not found in the sources read; routine.

Preamble

import Definitions.Def_DiazModulus

Formal statement

open Complex ComplexConjugate

namespace DiazModulus

theorem logAlg_adjoin_circle_point_hermite_lindemann_gelfond_schneider
    (u : ℂ) (hρ : IsAlgebraic ℚ (u * conj u))
    (hu : Transcendental (Subfield.closure (LogAlgTilde : Set ℂ)) u) :
    (∀ z ∈ (Submodule.span ℚ LogAlg ⊔ Submodule.span ℚ ({u, conj u} : Set ℂ)), IsAlgebraic ℚ z → z = 0) ∧
    (∀ l₀ β : ℂ, l₀ ∈ (Submodule.span ℚ LogAlg ⊔ Submodule.span ℚ ({u, conj u} : Set ℂ)) → β * l₀ ∈ (Submodule.span ℚ LogAlg ⊔ Submodule.span ℚ ({u, conj u} : Set ℂ)) →
      l₀ ≠ 0 → IsAlgebraic ℚ β → ∃ q : ℚ, β = (q : ℂ)) := by
  sorry

end DiazModulus

Source

Restates the Hermite–Lindemann theorem (Ch. Hermite 1873; F. Lindemann 1882) and the Gel'fond–Schneider theorem (A. O. Gel'fond 1934; Th. Schneider 1934) with ℒ replaced by ℒ_u = ℒ + ℚu + ℚū; both are derived from Baker's theorem (A. Baker, Linear forms in the logarithms of algebraic numbers I, Mathematika 13 (1966), 204–216). The ℒ_u form was not found in the sources read. Uses DiazModulus.logAlg_adjoin_circle_point_baker_linear_forms. R19 of the Diaz modulus mission. Formal proof: Diaz modulus mission, 18 October 2026 (C. Perassi).

View graph