Four exponentials in transcendence degree one (Brownawell; Waldschmidt)

The four exponentials conjecture is a theorem in transcendence degree one. This node states that case, unconditionally.

Let $\lambda_{11},\lambda_{12},\lambda_{21},\lambda_{22}$ be non-zero logarithms of algebraic numbers with

Then the two rows, or the two columns, of $\begin{pmatrix}\lambda_{11}&\lambda_{12}\\ \lambda_{21}&\lambda_{22}\end{pmatrix}$ are linearly dependent over $\mathbb Q$.

Attribution. This is Theorem 1 of D. Roy and M. Waldschmidt, Quadratic relations between logarithms of algebraic numbers, Proc. Japan Acad. Ser. A 71 (1995), 151–153, where it is stated in the equivalent form: if $x_1,x_2$ are linearly independent over $\mathbb Q$, and $y_1,y_2$ likewise, and $\mathbb Q(x_1,x_2,y_1,y_2)$ has transcendence degree $1$ over $\mathbb Q$, then at least one of $e^{x_1y_1}, e^{x_1y_2}, e^{x_2y_1}, e^{x_2y_2}$ is transcendental. The two forms are identified in the paper itself, which states that its Theorem 1 "is the special case of Theorem 2 when $P$ is $X_1X_4-X_2X_3$ with $n=4$".

Roy and Waldschmidt do not claim the result as their own — the paper gives a new proof and refers for the original to W. D. Brownawell, The algebraic independence of certain numbers related to the exponential function, J. Number Theory 6 (1974), 22–31, Cor. 7, and to M. Waldschmidt, Solution du huitième problème de Schneider, J. Number Theory 5 (1973), 191–202, Cor. 4. The paper opens by recording that the four exponentials conjecture "has been solved only in one special case, namely when the transcendence degree of the field which is spanned by the four logarithms is 1".

Statement checked against the source. The 1995 paper states the hypothesis as transcendence degree exactly $1$. This node writes $\le 1$: the degree-zero case is vacuous here, since four non-zero algebraic $\lambda_{ij}$ with $e^{\lambda_{ij}}$ algebraic contradict Hermite–Lindemann, available on this mission as the Proved node DiazModulus.hermite_lindemann_holds.

Relation to Diaz.four_exp_trdeg_one. That node states the same conclusion over an arbitrary subfield $K\subset\mathbb C$ and carries a master dichotomy as the explicit hypothesis hMaster, because no source was held when it was written. This node is the $K=\overline{\mathbb Q}$ case asserted outright on the authority of the paper above, which is now held. Neither supersedes the other: the $K$-general form is not supported by this source.

Formalization note. Transcendence degree is Algebra.trdeg ℚ of Algebra.adjoin ℚ of the four numbers, and "linearly dependent over $\mathbb Q$" is the existence of a non-zero rational pair annihilating the two rows, respectively the two columns. Proving this node means formalizing Brownawell's or Waldschmidt's argument; neither is in Mathlib at this revision.

Formalisation status: this is a citation boundary, not a task. A scoping pass on 2026-09-08, run against the pinned Mathlib and with every declaration name confirmed by a building #check, found that essentially none of the required machinery exists: no Wirsing approximation theorem, no interpolation determinants, no zero estimates on commutative algebraic groups, no height-form Liouville inequality, no Gel'fond criterion, no six exponentials, and of Lindemann–Weierstrass only the analytical part (LindemannWeierstrass.exp_polynomial_approx). The single largest obstacle is Philippon's zero estimate: without it there is no route from "the interpolation determinant vanishes to high order" to "rank drop or algebraic subgroup", and its own prerequisites — intersection multiplicities and degree bounds on algebraic groups — are absent wholesale. Wirsing's theorem is a close second and at least self-contained.

The obvious shortcut does not exist either. The six exponentials theorem does not imply this statement: six exponentials is a $3\times2$ result, this is $2\times2$ together with a transcendence-degree hypothesis, and no deduction of the second from the first is known.

So nobody should open this node expecting to prove it. It is here to be cited: an attributed classical result that downstream nodes may depend on, with the source identified precisely enough that a reader can check what is being assumed. DiazModulus.diaz_of_exp_not_real_irrational_angle_period_aligned_norm_rat_mult already depends on it in exactly that way.

Two things that would be genuine contributions, and are not this node: a height-form Liouville inequality (self-contained, roughly a week from Northcott and the product formula, and it unlocks further arithmetic), and the six exponentials theorem itself (a real milestone, and the natural warm-up, though not a route here).