In transcendence degree one, a real product of two non-zero logarithms has both factors real, both purely imaginary, or one a rational multiple of the other's conjugate

Proved

DiazModulus.log_mul_real_trichotomy_of_trdeg_one

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

diaz-modulus-leannumber-theorytranscendence

Let $\lambda, \mu$ be non-zero logarithms of algebraic numbers such that $\lambda, \bar\lambda, \mu, \bar\mu$ generate a $\mathbb{Q}$ -algebra of transcendence degree at most $1$ . If $\lambda\mu$ is real, then $\lambda$ and $\mu$ are both real, or both purely imaginary, or $\mu \in \mathbb{Q}\bar\lambda$ .

Each of the three cases makes $\lambda\mu$ real, so this is a classification. The product need not be algebraic: only its argument matters. Under Schanuel's conjecture the hypothesis forces $\lambda$ and $\mu$ onto one axis, as rational multiples of each other. Unconditionally the other configurations are not known to be impossible, and the theorem says which of them can occur. The companion node DiazModulus.log_mul_imaginary_mixed_of_trdeg_one treats a purely imaginary product, and DiazModulus.candidate_log_mul_real_iff_rat_conj applies both to a candidate for Diaz's conjecture.

Proof. The matrix $\begin{pmatrix}\lambda & \bar\lambda\\ \bar\mu & \mu\end{pmatrix}$ has non-zero logarithms of algebraic numbers as entries, since $e^{\bar z} = \overline{e^{z}}$ , and its determinant $\lambda\mu - \overline{\lambda\mu} = 2i\,\mathrm{Im}(\lambda\mu)$ vanishes. By the four exponentials theorem in transcendence degree one (DiazModulus.four_exponentials_trdeg_one), its rows or its columns are linearly dependent over $\mathbb{Q}$ . Dependent rows give $\bar\mu = q\lambda$ , that is $\mu = q\bar\lambda$ . Dependent columns give $a\lambda + b\bar\lambda = 0$ and $b\mu + a\bar\mu = 0$ with $a, b \in \mathbb{Q}$ not both zero; on real and imaginary parts, $a + b \neq 0$ makes both factors purely imaginary, and $a - b \neq 0$ makes both real.

Novelty. Not asserted. The statement is the transcendence-degree-one case of Diaz's conjecture (Qr2) (2007, p. 376), and the proof is Diaz's own argument for (Qr2) from the four exponentials conjecture (p. 377), with that conjecture replaced by the theorem of Waldschmidt (1973) and Brownawell (1974) in transcendence degree one, which Diaz quotes on p. 386. That combination was not found in the sources read.

Preamble

import Mathlib

Formal statement

open Complex ComplexConjugate

namespace DiazModulus

theorem log_mul_real_trichotomy_of_trdeg_one (l m : ℂ) (hl : l ≠ 0) (hm : m ≠ 0)
    (hel : IsAlgebraic ℚ (Complex.exp l)) (hem : IsAlgebraic ℚ (Complex.exp m))
    (htr : Algebra.trdeg ℚ ↥(Algebra.adjoin ℚ ({l, m, conj l, conj m} : Set ℂ)) ≤ 1)
    (hreal : (l * m).im = 0) :
    (l.im = 0 ∧ m.im = 0) ∨ (l.re = 0 ∧ m.re = 0) ∨ ∃ q : ℚ, m = (q : ℂ) * conj l := by
  sorry

end DiazModulus

Source

The transcendence-degree-one case of Diaz's conjecture (Qr2) (G. Diaz, Produits et quotients de combinaisons linéaires de logarithmes de nombres algébriques : conjectures et résultats partiels, J. Théor. Nombres Bordeaux 19 (2007), 373–391, p. 376: for logarithms ℓ₀, ℓ₁ off both axes, ℓ₁/ℓ₀ ∈ ℝ ∪ iℝ implies ℓ₁/ℓ₀ ∈ ℚ). Diaz derives (Qr2) from the four exponentials conjecture with the same 2×2 matrix (p. 377); here the conjecture is replaced by the four exponentials theorem in transcendence degree one (M. Waldschmidt, Solution du huitième problème de Schneider, J. Number Theory 5 (1973), 191–202, Cor. 4; W. D. Brownawell, The algebraic independence of certain numbers related by the exponential function, J. Number Theory 6 (1974), 22–31, Cor. 7; M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Grundlehren 326, Springer, 2000, Cor. 15.28(c)), which Diaz quotes on p. 386 without combining it with (Qr2). His Cor. 6(2) (p. 387) proves (Qr2) under ℓ₁/ℓ₀ ∈ ℒ̃ instead. The transcendence-degree-one form was not found in the sources read. Formal proof: Diaz modulus mission, 2 October 2026 (C. Perassi).

View graph