On either axis, an algebraic modulus forces the point itself to be algebraic

Source. The first step of the proof of Lemma 1.3 (Axis and independence reductions) in Carlo Perassi's manuscript Rigidity of logarithms with algebraic modulus — around a conjecture of Diaz, Section 1, The conjecture and its elementary normal form. The mathematics is Carlo Perassi's, and this step is stated there in one sentence: "If $u \in \mathbb{R} \cup i\mathbb{R}$ and $|u| \in \overline{\mathbb{Q}}$, then $u \in \overline{\mathbb{Q}}$." No novelty is claimed; the statement is elementary and possibly known — it has not been checked against the literature.

Statement. Let $u \in \mathbb{C}$ lie on one of the two axes, that is $\bar u = u$ ($u$ real) or $\bar u = -u$ ($u$ purely imaginary). If $|u|$ is algebraic over $\mathbb{Q}$, then so is $u$.

Proof. On either axis $u^{2} = \pm\, u \bar u = \pm |u|^{2}$, so $u^{2}$ is algebraic, and a complex number whose square is algebraic is algebraic.

What this is not. Lemma 1.3 asserts more: that the candidate locus $\mathcal{D}$ is disjoint from $\mathbb{R} \cup i\mathbb{R}$. Getting there from the statement above needs one further input, Hermite–Lindemann — for $u \neq 0$ algebraic, $e^{u}$ is transcendental — which is not available in the platform's Mathlib at this revision (only the analytic half, NumberTheory.Transcendental.Lindemann.AnalyticalPart, is present). The full axis reduction, conditional on that input, is already on this mission as DiazModulus.diaz_on_axes_of_hermite_lindemann. What is published here is the half of the argument that is unconditional, and it is the half that carries the elementary content: on an axis, an algebraic modulus pins the point itself down to $\overline{\mathbb{Q}}$.