Diaz 2007, Corollaire 2 (P)(1), from Roy's strong six exponentials

Source (a cited classical result, ported with attribution). This is Corollaire 2 (P), point 1, of

G. Diaz, Produits et quotients de combinaisons linéaires de logarithmes de nombres algébriques : conjectures et résultats partiels, Journal de Théorie des Nombres de Bordeaux 19 (2007), no. 2, 373–391; Corollaire 2 (P), point 1, p. 381.

The result is not the work of the mission's author. It is ported here as an attributed legacy node because the mission needs it as an input, exactly as a formal library carries a named classical theorem. The statement below was transcribed from the original French text of the article, which is held locally on the mission; it was not reconstructed from any secondary description.

Diaz's statement, verbatim:

Corollaire 2 (P). 1) Soit $(\lambda_1,\lambda_2,\lambda_3)\in(\widetilde{\mathcal L}\setminus\overline{\mathbb Q})^3$ avec $(1,\lambda_2,\lambda_3)$ $\overline{\mathbb Q}$-libre. Alors : $\{\lambda_1\lambda_2,\lambda_1\lambda_3\}\not\subset\widetilde{\mathcal L}$.

Here $\mathcal L=\{\ell\in\mathbb C: \exp\ell\in\overline{\mathbb Q}\}$ and $\widetilde{\mathcal L}$ is the $\overline{\mathbb Q}$-vector space generated in $\mathbb C$ by $1$ and $\mathcal L$ (Diaz, p. 375). "$\overline{\mathbb Q}$-libre" means linearly independent over the algebraic numbers.

What is asserted here, and what is only carried. Diaz derives this corollary from D. Roy's strong six exponentials theorem, in the "Version 3" form he states as Théorème 3, point 3, p. 379:

Soit $(\lambda_0,\lambda_1,\lambda_2,\lambda_3)\in\widetilde{\mathcal L}^4$ tel que les familles $(\lambda_0,\lambda_1)$ et $(\lambda_0,\lambda_2,\lambda_3)$ sont $\overline{\mathbb Q}$-libres ; alors : $\{\lambda_1\lambda_2/\lambda_0,\ \lambda_1\lambda_3/\lambda_0\}\not\subset\widetilde{\mathcal L}$.

Roy's theorem (D. Roy, Matrices whose coefficients are linear forms in logarithms, J. Number Theory 41 (1992), Corollary 2; see also Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Corollary 11.16) has no Mathlib formalisation at this revision. It is therefore carried as the explicit hypothesis hSSE rather than asserted: the node proves the implication "Roy's strong six exponentials (Version 3) $\Rightarrow$ Corollaire 2 (P)(1)", which is Diaz's own one-line derivation, the case $\lambda_0=1$. Nothing unproved is asserted by this node.

Lean shape. The statement is over an arbitrary K : Subfield ℂ, the convention already used on this mission (Diaz.four_nodes, Diaz.not_on_axes, Diaz.indep_of_algebraic_product); at K = $\overline{\mathbb Q}$ (the algebraic numbers) it is exactly Diaz's statement. Since the mission carries no Definition node for $\widetilde{\mathcal L}$, the space is inlined: aLog is required to be Submodule.span ↥K (insert 1 {l | Complex.exp l ∈ K}), which is literally "the K-vector space generated by 1 and the logarithms of elements of K". Membership $\lambda\in\widetilde{\mathcal L}\setminus\overline{\mathbb Q}$ is rendered as l ∈ aLog together with l ∉ K, and $\overline{\mathbb Q}$-freeness of $(1,\lambda_2,\lambda_3)$ as hfree.

Proof. Apply hSSE with $\lambda_0=1$. The family $(1,\lambda_1)$ is $K$-free because $\lambda_1\notin K$: a relation $a+b\lambda_1=0$ with $b\ne0$ would put $\lambda_1=-a/b$ in $K$. The family $(1,\lambda_2,\lambda_3)$ is $K$-free by hypothesis, and $1\in\widetilde{\mathcal L}$ by construction. Division by $\lambda_0=1$ is the identity, so the conclusion of hSSE is the conclusion sought.

No novelty is claimed. #print axioms on the submitted proof: [propext, Classical.choice, Quot.sound].