Baker's theorem for ℒ_u = ℒ + ℚu + ℚū (u transcendental over the field of ℒ̃, uū algebraic): b₀ + Σ bᵢlᵢ ≠ 0 for ℚ-independent lᵢ ∈ ℒ_u and algebraic bᵢ, not all 0

Here $\mathcal{L}$ is the set of logarithms of algebraic numbers (the $z \in \mathbb{C}$ with $e^z$ algebraic), and $\widetilde{\mathcal{L}}$ is the $\overline{\mathbb{Q}}$-vector space spanned by $1$ and $\mathcal{L}$. Let $F$ be the subfield of $\mathbb{C}$ generated by $\widetilde{\mathcal{L}}$, that is, by $\overline{\mathbb{Q}}$ and $\mathcal{L}$. Let $u \in \mathbb{C}$ be transcendental over $F$, with $u\bar u$ algebraic, and put $\mathcal{L}_u = \mathrm{span}_{\mathbb{Q}}(\mathcal{L}) + \mathrm{span}_{\mathbb{Q}}(u, \bar u)$; as $\mathcal{L}$ is a $\mathbb{Q}$-vector space, this is $\mathcal{L} + \mathbb{Q}u + \mathbb{Q}\bar u$. Let $n \geq 0$, let $l_1, \dots, l_n \in \mathcal{L}_u$ be linearly independent over $\mathbb{Q}$, and let $b_0, b_1, \dots, b_n$ be algebraic numbers, not all zero. Then $b_0 + \sum_{i=1}^{n} b_il_i \neq 0$.

Proof. This is the derivation of Baker's Theorem 1.6 from Theorem 4.5 in Waldschmidt's book (§4.2.5), with $\mathcal{L}_u$ in place of $\mathcal{L}$; it uses only that $\mathcal{L}_u$ is a $\mathbb{Q}$-vector space. Suppose $b_0 + \sum_jb_jl_j = 0$, let $K = \mathbb{Q}(b_1, \dots, b_n)$, a number field with a $\mathbb{Q}$-basis $(\beta_i)$, and write $b_j = \sum_ic_{ji}\beta_i$ with $c_{ji} \in \mathbb{Q}$. Then $\ell'_i = \sum_jc_{ji}l_j \in \mathcal{L}_u$ and $\sum_i\beta_i\ell'_i = -b_0$ is algebraic, so DiazModulus.logAlg_adjoin_circle_point_baker_number_field_basis gives $\ell' = 0$. The $\mathbb{Q}$-independence of the $l_j$ gives $c = 0$, so every $b_j = 0$, and then the relation reads $b_0 = 0$.

Novelty. With $\mathcal{L}_u$ in place of $\mathcal{L}$, this is Baker's theorem (1966) on linear forms in logarithms, Theorem 1.6 of Waldschmidt's book (2000), derived from its Theorem 4.5 form (DiazModulus.logAlg_adjoin_circle_point_baker_number_field_basis) as in §4.2.5 of that book. Not found in the sources read; routine.