The strong four exponentials conjecture, with Baker's theorem, implies the sharp four and the strong five exponentials conjectures

Here $\mathcal{L}$ is the set of logarithms of algebraic numbers, and $\widetilde{\mathcal{L}}$ is the $\overline{\mathbb{Q}}$-vector space spanned by $1$ and $\mathcal{L}$. The strong four exponentials conjecture (DiazModulus.StrongFourExponentials, Conjecture 11.17 of Waldschmidt's book) is carried as the hypothesis hS: if $x_1, x_2$ are linearly independent over $\overline{\mathbb{Q}}$ and so are $y_1, y_2$, then one of the four products $x_iy_j$ is not in $\widetilde{\mathcal{L}}$. Baker's theorem is carried as the hypothesis hB, in its two-logarithm inhomogeneous form, as in DiazModulus.candidate_one_log_saturation.

1. Sharp four exponentials. If $x_1, x_2$ are linearly independent over $\mathbb{Q}$ and so are $y_1, y_2$, and if $\beta_{ij}$ ($i, j = 1, 2$) are algebraic numbers such that the four numbers $e^{x_iy_j - \beta_{ij}}$ are algebraic, then $x_iy_j = \beta_{ij}$ for all $i, j$.
2. Strong five exponentials. Under the hypotheses of part 1 (with constants $\alpha_{ij}$), if moreover $\eta \neq 0$ and $\beta$ are algebraic and $e^{\eta x_2/x_1 - \beta}$ is algebraic, then also $\eta x_2 = \beta x_1$.

The two parts are stated in the forms of DiazModulus.diaz_of_sharp_four_exponentials and DiazModulus.diaz_of_strong_five_exponentials, so they can be passed to those nodes, to DiazModulus.recip_pi_not_log_of_sharp_four_exponentials and DiazModulus.recip_pi_not_log_of_strong_five_exponentials, and to DiazModulus.exp_log_mul_log_transcendental_of_strong_five.

Proof. The four products lie in $\widetilde{\mathcal{L}}$, so the conjecture makes $(x_1, x_2)$ or $(y_1, y_2)$ linearly dependent over $\overline{\mathbb{Q}}$. Say $x_2 = cx_1$, with $c$ algebraic and, by $\mathbb{Q}$-independence, not rational. For the logarithms $\ell_{ij} = x_iy_j - \beta_{ij}$, the number $\ell_{2j} - c\ell_{1j}$ is algebraic. Baker's theorem makes $\ell_{1j}$ and $\ell_{2j}$ linearly dependent over $\mathbb{Q}$; as $c \notin \mathbb{Q}$, both are then algebraic, hence $0$ by Hermite–Lindemann. The case $y_2 = dy_1$ runs along the rows. For part 2, $x_2/x_1 = \alpha_{21}/\alpha_{11}$ is algebraic, so $\eta x_2/x_1 - \beta$ is an algebraic logarithm of an algebraic number, hence $0$.

Novelty. None claimed. Part 2 from part 1 is Waldschmidt's remark (1988, p. 379) that the strong five exponentials conjecture is clearly weaker than the strong four exponentials conjecture of that paper. That conjecture is his Corollary 2.1 (the sharp six exponentials theorem) with two numbers $y_j$ instead of three (p. 377): part 1 here, called the sharp four exponentials conjecture in his 2005 survey. The strong four exponentials conjecture of his book is stated for products in $\widetilde{\mathcal{L}}$, the $\overline{\mathbb{Q}}$-span of $1$ and $\mathcal{L}$, rather than in $\overline{\mathbb{Q}} + \mathcal{L}$; part 1 derives the sharp form from it with Baker's theorem. The book introduces the strong five exponentials conjecture (p. 437) as a weaker statement than a dimension bound that includes Conjecture 11.17. The contribution of this node is the formal proof.