Diaz 2007, Théorème 4: x₂/x₁ ∈ ℒ̃ keeps the four products out of ℒ̃ (strong six exponentials) and out of ℒ (with Baker)

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}$. Roy's strong six exponentials theorem is carried as the hypothesis hSSE: if $x_1, x_2$ are $\overline{\mathbb{Q}}$-linearly independent and so are $y_1, y_2, y_3$, then one of the six 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. Let $x_1, x_2$ be linearly independent over $\overline{\mathbb{Q}}$ and $(y_1, y_2, 1/x_1)$ linearly independent over $\overline{\mathbb{Q}}$. If $x_2/x_1 \in \widetilde{\mathcal{L}}$, the four numbers $x_1y_1, x_1y_2, x_2y_1, x_2y_2$ are not all in $\widetilde{\mathcal{L}}$.
2. Let $x_1, x_2$ be linearly independent over $\mathbb{Q}$ and $y_1, y_2$ linearly independent over $\mathbb{Q}$. If $x_2/x_1 \in \widetilde{\mathcal{L}}$, the four numbers are not all in $\mathcal{L}$.

Proof. Part 1 is the theorem applied to $(x_1, x_2)$ and $(y_1, y_2, 1/x_1)$, whose two extra products are $1$ and $x_2/x_1$. For part 2, if the four numbers are logarithms, Baker's theorem makes $(x_1, x_2)$ and $(1/x_1, y_1, y_2)$ independent over $\overline{\mathbb{Q}}$, and part 1 applies.

Novelty. None: this is Théorème 4 of Diaz (2007), p. 385, with his proof (p. 386). Diaz presents it as a corollary of the strong six exponentials theorem that generalises Waldschmidt's five exponentials theorem. The contribution of this node is the formal proof.