For a candidate u and a logarithm μ algebraic over ℚ(u): uμ is real exactly when μ ∈ ℚū, and uμ is never purely imaginary

Let $u$ be a candidate for Diaz's conjecture (DiazModulus.IsCandidate: $u \neq 0$ with $|u|$ and $e^u$ algebraic), and let $\mu \neq 0$ be a logarithm of an algebraic number that is algebraic over $\mathbb{Q}[u]$. Then $u\mu$ is real if and only if $\mu = q\bar u$ for some $q \in \mathbb{Q}$, and $u\mu$ is never purely imaginary.

So among the logarithms algebraic over $\mathbb{Q}(u)$, the conjugate $\bar u$ is, up to a rational factor, the only one whose product with $u$ lies on an axis, whether or not that product is algebraic. Compare DiazModulus.candidate_norm_div_log_not_log, which concerns the factorisations of $|u|^2$ itself.

Proof. A candidate lies on neither axis: there $\bar u = \pm u$, so $u^2 = \pm|u|^2$ would be algebraic, against Hermite–Lindemann (DiazModulus.hermite_lindemann_holds). Since $\bar u = |u|^2/u$ with $|u|^2$ algebraic, $\bar u$ is algebraic over $\mathbb{Q}[u]$, and so is $\bar\mu$, which is algebraic over $\mathbb{Q}[\bar u]$. Hence $u, \mu, \bar u, \bar\mu$ generate an algebra of transcendence degree at most one (Transcendence.trdeg_adjoin_le_one_of_isAlgebraic_adjoin). If $u\mu$ is real, DiazModulus.log_mul_real_trichotomy_of_trdeg_one leaves only $\mu \in \mathbb{Q}\bar u$; conversely $u \cdot q\bar u = q|u|^2$ is real. If $u\mu$ were purely imaginary, DiazModulus.log_mul_imaginary_mixed_of_trdeg_one would put $u$ on an axis.

Novelty. Not asserted. In Diaz's reading of (Qr2) (2007, p. 377), $\mathbb{R}\ell \cap \mathcal{L} = \mathbb{Q}\ell$ and $i\mathbb{R}\ell \cap \mathcal{L} = \{0\}$; this node is that reading at $\ell = \bar u$, proved for the logarithms algebraic over $\mathbb{Q}(u)$. It concerns a candidate, so it is vacuous if Diaz's conjecture holds. Not found in the sources read.