A logarithm off the axes lies on no algebraic generalized line, unconditionally

Proved

DiazModulus.no_algebraic_generalized_line_unconditional

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

diaz-modulus-leannumber-theorytranscendence

A logarithm $\lambda$ of an algebraic number lying off both coordinate axes lies on no algebraic generalized line: there are no $B \in \overline{\mathbb{Q}}^{\times}$ and $C \in \overline{\mathbb{Q}}$ with

B\lambda + \overline{B}\,\overline{\lambda} + C = 0 .

This is DiazModulus.no_algebraic_generalized_line with its hypothesis, Baker's theorem for two logarithms, discharged by DiazModulus.baker_two_logs, which this mission proves following Chapter 4 of Waldschmidt's Diophantine Approximation on Linear Algebraic Groups.

Proof. DiazModulus.no_algebraic_generalized_line DiazModulus.baker_two_logs.

Novelty. Nothing beyond the parent node; its page gives the argument and the attribution.

Preamble

import Mathlib

Formal statement

namespace DiazModulus

theorem no_algebraic_generalized_line_unconditional :
    ∀ l : ℂ, IsAlgebraic ℚ (Complex.exp l) → l.re ≠ 0 → l.im ≠ 0 →
      ∀ B C : ℂ, IsAlgebraic ℚ B → B ≠ 0 → IsAlgebraic ℚ C →
        B * l + (starRingEnd ℂ) B * (starRingEnd ℂ) l + C ≠ 0 := by
  sorry

end DiazModulus

Source

The statement and argument of `DiazModulus.no_algebraic_generalized_line` (Theorem 6.1 of the companion note, version 1.9; the first step of Théorème 3 in G. Diaz, J. Théor. Nombres Bordeaux 16 (2004)), with Baker's theorem (A. Baker, Linear forms in the logarithms of algebraic numbers I, Mathematika 13 (1966), 204–216) proved in this mission as `DiazModulus.baker_two_logs`. Formal proof: Diaz modulus mission, 2 October 2026 (C. Perassi).

View graph