Theorem D as a barrier: some ℚ-subspace L ⊇ ℒ of ℂ has all the Theorem D properties and contains u ≠ 0 with |u| algebraic

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}$. There is a $\mathbb{Q}$-vector subspace $L$ of $\mathbb{C}$ with $\mathcal{L} \subseteq L$ such that, with $\widetilde L = \mathrm{span}_{\overline{\mathbb{Q}}}(\{1\} \cup L)$, $L$ has the properties

• (conjugation) $\bar z \in L$ for every $z \in L$;
• (Baker) if $n \geq 0$, $l_1, \dots, l_n \in L$ are linearly independent over $\mathbb{Q}$, and $b_0, b_1, \dots, b_n$ are algebraic numbers, not all zero, then $b_0 + \sum_{i=1}^{n} b_il_i \neq 0$;
• (Hermite–Lindemann) every algebraic $z \in L$ is $0$;
• (Gel'fond–Schneider) if $l_0 \neq 0$ and $\beta l_0$ both lie in $L$ and $\beta$ is algebraic, then $\beta \in \mathbb{Q}$;
• (Roy, relative to $\widetilde{\mathcal{L}}$) if no $x_1, x_2$, linearly independent over $\overline{\mathbb{Q}}$, and $y_1, y_2, y_3$, linearly independent over $\overline{\mathbb{Q}}$, have all six products $x_iy_j$ in $\widetilde{\mathcal{L}}$, then no such families have all six products in $\widetilde L$;
• (six exponentials) no $x_1, x_2 \in \mathbb{C}$, linearly independent over $\mathbb{Q}$, and $y_1, y_2, y_3 \in \mathbb{C}$, linearly independent over $\mathbb{Q}$, have all six products $x_iy_j$ in $L$;
• (four exponentials in transcendence degree one) if $\ell_{11}, \ell_{12}, \ell_{21}, \ell_{22} \in L$ are non-zero, $\ell_{11}\ell_{22} = \ell_{12}\ell_{21}$, and the $\mathbb{Q}$-algebra they generate has transcendence degree at most $1$ over $\mathbb{Q}$, then there are $a, b \in \mathbb{Q}$, not both zero, with $a\ell_{11} + b\ell_{21} = a\ell_{12} + b\ell_{22} = 0$ (the rows of the matrix $(\ell_{ij})$ are linearly dependent over $\mathbb{Q}$), or with $a\ell_{11} + b\ell_{12} = a\ell_{21} + b\ell_{22} = 0$ (its columns are),

and some $u \in L$ has $u \neq 0$ and $|u|$ algebraic.

The Roy clause is an implication: Roy's strong six exponentials theorem for $\widetilde{\mathcal{L}}$ (Roy 1992, Cor. 2) is its hypothesis, not a hypothesis of the node, so the statement is unconditional.

What it means. DiazModulus.span_logAlg_theorem_D_properties shows that $\mathcal{L}$ itself has these properties and that Diaz's conjecture says exactly that no non-zero element of $\mathcal{L}$ has algebraic modulus, while DiazModulus.theorem_D_barrier gives a $\mathbb{Q}$-space $L \supseteq \mathcal{L}$ with the same properties that does contain such an element. So the listed properties, as axioms about $(\mathcal{L}, \widetilde{\mathcal{L}})$ (with Roy's theorem for $\widetilde{\mathcal{L}}$ supplying the hypothesis of the Roy clause), do not prove Diaz's conjecture: an argument from them alone would apply to $L$ and its $\overline{\mathbb{Q}}$-span with $1$ as well. Here a candidate for $L$ means a non-zero $u \in L$ with $|u|$ algebraic; it is not DiazModulus.IsCandidate, which asks for $e^u$ to be algebraic. The barrier is a model-existence statement about membership only: the model has no exponential function, so it says nothing about arguments through the values $e^{x_iy_j}$, such as Waldschmidt's theorem of 1973, or through Roy's rank bounds for larger matrices.

Proof. DiazModulus.exists_circle_point_transcendental_over_logAlgTilde_closure at $\rho = 1$ gives $u$ with $u\bar u = 1$ that is transcendental over the field generated by $\widetilde{\mathcal{L}}$; its hypothesis that $u\bar u$ is algebraic holds since $1$ is. Then DiazModulus.logAlg_adjoin_circle_point_theorem_D gives every listed property for $L = \mathcal{L}_u = \mathrm{span}_{\mathbb{Q}}(\mathcal{L}) + \mathrm{span}_{\mathbb{Q}}(u, \bar u)$, together with $\mathcal{L} \subseteq L$, $u \in L$, $u \neq 0$ and $|u|$ algebraic.

Novelty. Not found in the sources read; routine, given Theorem D (DiazModulus.logAlg_adjoin_circle_point_theorem_D) and the generic circle point (DiazModulus.exists_circle_point_transcendental_over_logAlgTilde_closure).