Liouville's lower bound for the value of Gelfond's auxiliary function

Let K be a number field of degree h and α, β, γ ∈ K. Gelfond's auxiliary function has coefficients η_{ab} ∈ 𝓞 K, a, b < q, with house η_{ab} ≤ c ^ n n ^ ((n + 1) / 2), where q ^ 2 = 2 m n (TauCeti.exists_gelfond_auxiliary_algebraic). Its first nonvanishing derivative at one of the points t₀ ≤ m (RingHom.exists_iteratedDeriv_gelfond_auxiliary_ne_zero), of order r ≥ n, is λ ^ r σ ρ with

ρ = ∑_{a, b} η_{ab} ((a + 1) + (b + 1) β) ^ r α ^ ((a + 1) t₀) γ ^ ((b + 1) t₀) ∈ K.

This file bounds |σ ρ| from below for nonzero ρ, which is the arithmetic half of the final contradiction in Gelfond's proof of the Gelfond–Schneider theorem. If c₀ α, c₀ β, c₀ γ are algebraic integers, then c₀ ^ (r + 2 q m) ρ is a nonzero algebraic integer, of house at most X ^ r r ^ r for a constant X, so Liouville's inequality (NumberField.one_le_norm_mul_house_pow) gives

1 ≤ c₂ ^ r r ^ ((h - 1) r) |σ ρ|

for a constant c₂ depending only on K, α, β, γ, m and c (TauCeti.exists_one_le_pow_mul_norm_gelfond_value). The analytic upper bound for |σ ρ|, which contradicts this for m > 2 h + 1 and large r, is not part of this file.

Main results

• TauCeti.exists_one_le_pow_mul_norm_gelfond_value: the lower bound above, uniform over the embeddings σ : K →+* ℂ.

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_one_le_pow_mul_norm_gelfond_value {K : Type u_1} [Field K] [NumberField K] (α β γ : K) (m : ℕ) (c : ℝ) : ∃ (c₂ : ℝ), 1 ≤ c₂ ∧ ∀ (σ : K →+* ℂ) (n q r t₀ : ℕ) (η : Fin q → Fin q → NumberField.RingOfIntegers K), q ^ 2 = 2 * m * n → n ≤ r → t₀ ≤ m → (∀ (a b : Fin q), NumberField.house ↑(η a b) ≤ c ^ n * ↑n ^ ((↑n + 1) / 2)) → ∑ a : Fin q, ∑ b : Fin q, ↑(η a b) * (↑(↑a + 1) + ↑(↑b + 1) * β) ^ r * (α ^ ((↑a + 1) * t₀) * γ ^ ((↑b + 1) * t₀)) ≠ 0 → 1 ≤ c₂ ^ r * ↑r ^ ((Module.finrank ℚ K - 1) * r) * ‖σ (∑ a : Fin q, ∑ b : Fin q, ↑(η a b) * (↑(↑a + 1) + ↑(↑b + 1) * β) ^ r * (α ^ ((↑a + 1) * t₀) * γ ^ ((↑b + 1) * t₀)))‖

Liouville's lower bound for Gelfond's values (Karatarakis–Wiedijk, §3). Let K be a number field of degree h, α, β, γ ∈ K, m ∈ ℕ and c ∈ ℝ. There is c₂ ≥ 1 with the following property. Let q ^ 2 = 2 m n, r ≥ n and t₀ ≤ m, and let η_{ab} ∈ 𝓞 K, a, b < q, have house at most c ^ n n ^ ((n + 1) / 2), as for Gelfond's auxiliary function. If ρ = ∑_{a, b} η_{ab} ((a + 1) + (b + 1) β) ^ r α ^ ((a + 1) t₀) γ ^ ((b + 1) t₀) is nonzero, then 1 ≤ c₂ ^ r r ^ ((h - 1) r) |σ ρ| for every embedding σ : K →+* ℂ. In particular |σ ρ| ≥ c₂ ^ (-r) r ^ (-(h - 1) (r + 1)).