Gelfond's auxiliary function and its first nonvanishing derivative

Let K be a field of characteristic zero with an embedding σ : K →+* ℂ, let λ ∈ ℂ and let α, β, γ ∈ K with σ α = exp λ, σ γ = exp (σ β λ) and β irrational. In Gelfond's proof of the Gelfond–Schneider theorem the auxiliary function is the exponential sum

R(z) = ∑_{a, b = 1}^{q} η_{ab} exp ((a + b σ β) λ z)

with coefficients η_{ab} ∈ K (written σ η_{ab} once embedded in ℂ). Its derivatives at the natural numbers lie in σ(K) after factoring out a power of λ: since exp ((a + b σ β) λ t) is σ (α ^ (a t) γ ^ (b t)),

R⁽ᵏ⁾(t) = λ ^ k σ (y_k(t)), where y_k(t) = ∑_{a, b} η_{ab} (a + b β) ^ k α ^ (a t) γ ^ (b t).

In the application, K is a number field containing the algebraic numbers α, β, γ, and the coefficients η are algebraic integers chosen by Siegel's lemma so that R vanishes to a high order n at the points t = 1, …, m. Gelfond's argument then uses the first derivative order r at which R fails to vanish at one of these points, say at t₀: the number ρ = y_r(t₀) ∈ K is nonzero, so in that number-field setting (after clearing the denominators of α, β, γ) it satisfies Liouville's lower bound, while the vanishing of all lower derivatives gives an analytic upper bound for |R⁽ʳ⁾(t₀)| = |λ| ^ r |σ ρ|.

Construction. For a number field K and m ≥ 1, the conditions y_k(t) = 0 for k < n and 1 ≤ t ≤ m are m n linear equations in the q ^ 2 unknowns η_{ab}. When q ^ 2 = 2 m n, Mathlib's Siegel lemma over 𝓞 K (NumberField.house.exists_ne_zero_int_vec_house_le), whose exponent m n / (q ^ 2 - m n) is then 1, solves them with algebraic integers of house at most c ^ n n ^ ((n + 1) / 2), for a constant c depending only on K, α, β, γ and m. To apply it, each equation is multiplied by c₀ ^ (n - 1 + 2 q m) for a nonzero integer c₀ such that c₀ α, c₀ β and c₀ γ are algebraic integers; the entries of the resulting system have house at most q ^ (n - 1) H ^ (n - 1 + 2 q m).

First nonvanishing derivative. This part makes no arithmetic assumption on K: it proves that such r and t₀ exist, with n ≤ r < q ^ 2, as soon as λ ≠ 0 and η ≠ 0. For each fixed t, the values y_k(t) are the power sums ∑ w_{ab} θ_{ab} ^ k with weights w_{ab} = η_{ab} α ^ (a t) γ ^ (b t) and nodes θ_{ab} = a + b β. The nodes are pairwise distinct because β is irrational, so the Vandermonde matrix of the nodes is invertible and one of the first q ^ 2 power sums is nonzero. In Lean the indices a, b run over Fin q, and the frequencies are written (a + 1) + (b + 1) β.

Main results

• TauCeti.exists_gelfond_auxiliary_algebraic: algebraic integers η_{ab}, not all zero, with house η_{ab} ≤ c ^ n n ^ ((n + 1) / 2), such that y_k(t) = 0 for k < n and 1 ≤ t ≤ m.
• RingHom.exists_gelfond_auxiliary: the same coefficients make R vanish to order n at 1, …, m.
• TauCeti.exists_gelfond_value_ne_zero: for η ≠ 0 and a nonempty finite set T ⊆ ℕ, there are r < q ^ 2 and t₀ ∈ T with y_k(t) = 0 for all k < r and t ∈ T, and y_r(t₀) ≠ 0.
• RingHom.iteratedDeriv_gelfond_auxiliary_natCast: R⁽ᵏ⁾(t) = λ ^ k σ (y_k(t)).
• RingHom.exists_iteratedDeriv_gelfond_auxiliary_ne_zero: if λ ≠ 0, η ≠ 0 and R vanishes to order n on T, then there are r with n ≤ r < q ^ 2 and t₀ ∈ T such that R vanishes to order r on T and R⁽ʳ⁾(t₀) ≠ 0.

References

• M. Karatarakis and F. Wiedijk, A formalization of the Gelfond–Schneider theorem, arXiv:2603.24823 (2026), §3.
• K. Soundararajan (notes by I. Petrow), Transcendental number theory, Stanford Math 249A course notes (2011).

theorem TauCeti.exists_gelfond_value_ne_zero {K : Type u_1} [Field K] [CharZero K] {α β γ : K} (hα : α ≠ 0) (hγ : γ ≠ 0) (hβ : ∀ (r : ℚ), ↑r ≠ β) {q : ℕ} {η : Fin q → Fin q → K} (hη : η ≠ 0) {T : Finset ℕ} (hT : T.Nonempty) : ∃ r < q ^ 2, ∃ t₀ ∈ T, (∀ k < r, ∀ t ∈ T, ∑ a : Fin q, ∑ b : Fin q, η a b * (↑(↑a + 1) + ↑(↑b + 1) * β) ^ k * (α ^ ((↑a + 1) * t) * γ ^ ((↑b + 1) * t)) = 0) ∧ ∑ a : Fin q, ∑ b : Fin q, η a b * (↑(↑a + 1) + ↑(↑b + 1) * β) ^ r * (α ^ ((↑a + 1) * t₀) * γ ^ ((↑b + 1) * t₀)) ≠ 0

The first nonvanishing derivative of Gelfond's auxiliary function, algebraic form. Let K be a field of characteristic zero, let α, γ ∈ K be nonzero and β ∈ K irrational, and let η : Fin q → Fin q → K be nonzero. Put y_k(t) = ∑_{a, b} η_{ab} ((a + 1) + (b + 1) β) ^ k α ^ ((a + 1) t) γ ^ ((b + 1) t). Then for every nonempty finite set T of natural numbers there are r < q ^ 2 and t₀ ∈ T such that y_k(t) = 0 for all k < r and t ∈ T, and y_r(t₀) ≠ 0.

theorem TauCeti.gelfond_two_mul_mul_le {m n q r : ℕ} (hq : q * q = 2 * m * n) (hnr : n ≤ r) : 2 * q * m ≤ 4 * m ^ 2 * r

The exponent bound behind Gelfond's constants: if q ^ 2 = 2 m n and n ≤ r, then 2 q m ≤ 4 m ^ 2 r, because q ≤ q ^ 2 = 2 m n.

theorem TauCeti.gelfond_natCast_pow_le {m n q k j : ℕ} (hm : 1 ≤ m) (hq : q * q = 2 * m * n) (hkj : k ≤ 2 * j) : ↑q ^ k ≤ (2 * ↑m) ^ j * ↑n ^ (↑k / 2)

The power bound behind Gelfond's constants: if q ^ 2 = 2 m n with m ≥ 1 and k ≤ 2 j, then q ^ k = (2 m n) ^ (k / 2) ≤ (2 m) ^ j n ^ (k / 2).

theorem TauCeti.gelfond_index_le {q m t k K₀ : ℕ} (a b : Fin q) (ht : t ≤ m) (hk : k ≤ K₀) : k + (↑a + 1) * t + (↑b + 1) * t ≤ K₀ + 2 * q * m

The index bound for the terms of Gelfond's values: for a, b < q, t ≤ m and k ≤ K₀, the exponent k + (a + 1) t + (b + 1) t is at most K₀ + 2 q m.

theorem TauCeti.exists_gelfond_auxiliary_algebraic {K : Type u_2} [Field K] [NumberField K] (α β γ : K) {m : ℕ} (hm : 1 ≤ m) : ∃ (c : ℝ), 1 ≤ c ∧ ∀ (n q : ℕ), 1 ≤ n → q ^ 2 = 2 * m * n → ∃ (η : Fin q → Fin q → NumberField.RingOfIntegers K), η ≠ 0 ∧ (∀ (a b : Fin q), NumberField.house ↑(η a b) ≤ c ^ n * ↑n ^ ((↑n + 1) / 2)) ∧ ∀ k < n, ∀ t ∈ Finset.Icc 1 m, ∑ a : Fin q, ∑ b : Fin q, ↑(η a b) * (↑(↑a + 1) + ↑(↑b + 1) * β) ^ k * (α ^ ((↑a + 1) * t) * γ ^ ((↑b + 1) * t)) = 0

Gelfond's auxiliary function, algebraic form (Karatarakis–Wiedijk, §3). Let K be a number field, α, β, γ ∈ K and m ≥ 1. There is c ≥ 1 such that for all positive integers n and q with q ^ 2 = 2 m n there are algebraic integers η_{ab} ∈ 𝓞 K, a, b < q, not all zero, with house η_{ab} ≤ c ^ n n ^ ((n + 1) / 2), such that y_k(t) = ∑_{a, b} η_{ab} ((a + 1) + (b + 1) β) ^ k α ^ ((a + 1) t) γ ^ ((b + 1) t) vanishes for all k < n and 1 ≤ t ≤ m.

theorem RingHom.iteratedDeriv_gelfond_auxiliary_natCast {R : Type u_1} [Ring R] (σ : R →+* ℂ) {l : ℂ} {α β γ : R} (hα : σ α = Complex.exp l) (hγ : σ γ = Complex.exp (σ β * l)) {q : ℕ} (η : Fin q → Fin q → R) (k t : ℕ) : iteratedDeriv k (fun (z : ℂ) => ∑ a : Fin q, ∑ b : Fin q, σ (η a b) * Complex.exp ((↑(↑a + 1) + ↑(↑b + 1) * σ β) * l * z)) ↑t = l ^ k * σ (∑ a : Fin q, ∑ b : Fin q, η a b * (↑(↑a + 1) + ↑(↑b + 1) * β) ^ k * (α ^ ((↑a + 1) * t) * γ ^ ((↑b + 1) * t)))

If σ α = exp λ and σ γ = exp (σ β λ), then the k-th derivative of Gelfond's auxiliary function R(z) = ∑_{a, b} σ η_{ab} exp (((a + 1) + (b + 1) σ β) λ z) at a natural number t is λ ^ k times the image under σ of y_k(t) = ∑_{a, b} η_{ab} ((a + 1) + (b + 1) β) ^ k α ^ ((a + 1) t) γ ^ ((b + 1) t).

theorem RingHom.exists_iteratedDeriv_gelfond_auxiliary_ne_zero {K : Type u_1} [Field K] (σ : K →+* ℂ) {l : ℂ} (hl : l ≠ 0) {α β γ : K} (hα : σ α = Complex.exp l) (hγ : σ γ = Complex.exp (σ β * l)) (hβ : ∀ (r : ℚ), ↑r ≠ β) {q : ℕ} {η : Fin q → Fin q → K} (hη : η ≠ 0) {T : Finset ℕ} (hT : T.Nonempty) {n : ℕ} (hn : ∀ k < n, ∀ t ∈ T, iteratedDeriv k (fun (z : ℂ) => ∑ a : Fin q, ∑ b : Fin q, σ (η a b) * Complex.exp ((↑(↑a + 1) + ↑(↑b + 1) * σ β) * l * z)) ↑t = 0) : ∃ (r : ℕ), n ≤ r ∧ r < q ^ 2 ∧ ∃ t₀ ∈ T, (∀ k < r, ∀ t ∈ T, iteratedDeriv k (fun (z : ℂ) => ∑ a : Fin q, ∑ b : Fin q, σ (η a b) * Complex.exp ((↑(↑a + 1) + ↑(↑b + 1) * σ β) * l * z)) ↑t = 0) ∧ iteratedDeriv r (fun (z : ℂ) => ∑ a : Fin q, ∑ b : Fin q, σ (η a b) * Complex.exp ((↑(↑a + 1) + ↑(↑b + 1) * σ β) * l * z)) ↑t₀ ≠ 0

The first nonvanishing derivative of Gelfond's auxiliary function. Let K be a field with an embedding σ : K →+* ℂ, let λ ≠ 0, and let α, β, γ ∈ K with β irrational, σ α = exp λ and σ γ = exp (σ β λ). Let η : Fin q → Fin q → K be nonzero, and suppose that R(z) = ∑_{a, b} σ η_{ab} exp (((a + 1) + (b + 1) σ β) λ z) vanishes to order n at every point of a nonempty finite set T of natural numbers. Then there are r with n ≤ r < q ^ 2 and t₀ ∈ T such that R vanishes to order r at every point of T and R⁽ʳ⁾(t₀) ≠ 0.

theorem RingHom.exists_gelfond_auxiliary {K : Type u_1} [Field K] [NumberField K] (σ : K →+* ℂ) {l : ℂ} {α β γ : K} (hα : σ α = Complex.exp l) (hγ : σ γ = Complex.exp (σ β * l)) {m : ℕ} (hm : 1 ≤ m) : ∃ (c : ℝ), 1 ≤ c ∧ ∀ (n q : ℕ), 1 ≤ n → q ^ 2 = 2 * m * n → ∃ (η : Fin q → Fin q → NumberField.RingOfIntegers K), η ≠ 0 ∧ (∀ (a b : Fin q), NumberField.house ↑(η a b) ≤ c ^ n * ↑n ^ ((↑n + 1) / 2)) ∧ ∀ k < n, ∀ t ∈ Finset.Icc 1 m, iteratedDeriv k (fun (z : ℂ) => ∑ a : Fin q, ∑ b : Fin q, σ ↑(η a b) * Complex.exp ((↑(↑a + 1) + ↑(↑b + 1) * σ β) * l * z)) ↑t = 0

Gelfond's auxiliary function (Karatarakis–Wiedijk, §3). Let K be a number field with an embedding σ : K →+* ℂ, let λ ∈ ℂ and α, β, γ ∈ K with σ α = exp λ and σ γ = exp (σ β λ), and let m ≥ 1. There is c ≥ 1 such that for all positive integers n and q with q ^ 2 = 2 m n there are algebraic integers η_{ab} ∈ 𝓞 K, a, b < q, not all zero, with house η_{ab} ≤ c ^ n n ^ ((n + 1) / 2), such that R(z) = ∑_{a, b} σ η_{ab} exp (((a + 1) + (b + 1) σ β) λ z) vanishes to order n at each of the points 1, …, m.