Four exponentials in transcendence degree one, from the master dichotomy

Source. This is the Corollary Four exponentials in transcendence degree one, statement 33 of C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, the predecessor manuscript of Carlo Perassi's note on Diaz's modulus conjecture. The manuscript states outright that the corollary is not its own: it is Theorem 1 of D. Roy and M. Waldschmidt's 1995 announcement, where it is attributed to Brownawell and Waldschmidt. It is ported here as an attributed legacy node. Neither the statement nor its attribution has been verified against the original; both were transcribed from C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026.

Statement. Let $\lambda_{11},\lambda_{12},\lambda_{21},\lambda_{22}$ be non-zero logarithms of elements of a subfield $K\subset\mathbb C$ (at $K=\overline{\mathbb Q}$, non-zero elements of $\mathcal L$) 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$. Equivalently, the four exponentials conjecture holds for quadruples of logarithms generating a field of transcendence degree at most one.

Provenance of the carried hypothesis. The dichotomy hMaster is the Theorem Master dichotomy for rationally proportional products of C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, the predecessor manuscript of Carlo Perassi's note on Diaz's modulus conjecture. In that manuscript it is derived from Roy and Waldschmidt's Théorème 0.2 (M. Waldschmidt and D. Roy, 1997; the dichotomy form), and the manuscript records that its $m=1$ case is Exercise 1.8 / the worked example of §12.5 of M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups. That statement was transcribed from C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026 and has not been verified against its own source; the sources are not held on this mission. It is therefore carried as the explicit hypothesis hMaster rather than asserted: this node asserts only the implication.

What the node proves. Given hMaster, the corollary follows by applying the dichotomy to $(\mu_1,\nu_1,\mu_2,\nu_2)=(\lambda_{11},\lambda_{22},\lambda_{12},\lambda_{21})$ with $m=1$. Its third alternative is excluded by the transcendence-degree hypothesis. In the first alternative $\lambda_{12}=c\lambda_{11}$ and $\lambda_{21}=c'\lambda_{22}$, and the product relation forces $cc'=1$, so the second column is $c$ times the first; the second alternative is symmetric and gives the rows. That case analysis, including the derivation of $cc'=1$, is the content actually verified here.

Formalization note. Transcendence degree is Algebra.trdeg ℚ of Algebra.adjoin ℚ of the four numbers; membership in $\mathcal L$ is Complex.exp l ∈ K; "$\mu_2\in\mathbb Q^\times\mu_1$" is ∃ c : ℚ, c ≠ 0 ∧ μ₂ = c * μ₁; and "linearly dependent over $\mathbb Q$" is the existence of a non-zero rational pair annihilating the two rows, resp. columns. #print axioms on the submitted proof: [propext, Classical.choice, Quot.sound].