A rational combination $au+b\bar u$ lies off both rational rays

Let $u \in \mathbb{C}$ lie off the two axes, that is $\bar u \neq u$ and $\bar u \neq -u$ (equivalently $\operatorname{Im} u \neq 0$ and $\operatorname{Re} u \neq 0$), and let $a,b \in \mathbb{Q}^\times$. Then

In particular $\mu \neq 0$, which is the instance $c = 0$ of either clause.

Where this sits. This is the closing clause of Theorem 3.9 (thm:mixed-rigidity, Mixed-coordinate rigidity at a Diaz point) of the manuscript. Theorem 3.9 takes $u$ on the Diaz locus, puts $\rho = u\bar u$, and for $\mu \in \mathcal{L} \setminus (\mathbb{Q}u \cup \mathbb{Q}\bar u)$ concludes

Its final paragraph verifies that the headline instance $\mu = au + b\bar u$ with $a,b \in \mathbb{Q}^\times$ really does satisfy that hypothesis: a relation $au + b\bar u \in \mathbb{Q}u \cup \mathbb{Q}\bar u$ would force $\bar u/u \in \mathbb{Q}$ and put $u$ on the axes. This node is exactly that verification, and it is unconditional — the deep input of Theorem 3.9 is Théorème 7.1 of Roy–Waldschmidt (1997), which is not available in this Mathlib revision and is not on the mission graph.

Proof. Off the axes, $u$ and $\bar u$ are linearly independent over $\mathbb{Q}$ (Diaz.indep_of_not_axis: from $\operatorname{Re} u \neq 0$ and $\operatorname{Im} u \neq 0$, a relation $xu + y\bar u = 0$ with $x,y \in \mathbb{Q}$ gives $x + y = 0$ on real parts and $x - y = 0$ on imaginary parts, hence $x = y = 0$).

• If $au + b\bar u = cu$ with $c \in \mathbb{Q}$, then $(a-c)u + b\bar u = 0$, so $b = 0$ — contradicting $b \neq 0$.
• If $au + b\bar u = c\bar u$ with $c \in \mathbb{Q}$, then $au + (b-c)\bar u = 0$, so $a = 0$ — contradicting $a \neq 0$.

Formalisation notes. The hypothesis is stated in the off-axes form $\overline u \neq u \wedge \overline u \neq -u$, which is the weakest form and is exactly what Diaz.indep_of_not_axis consumes; a consumer working on the Diaz locus obtains it from Diaz.not_on_axes. The two ray exclusions quantify over all $c \in \mathbb{Q}$ (not merely $\mathbb{Q}^\times$), so the non-vanishing $\mu \neq 0$ that the manuscript notes separately is the case $c = 0$ and is not stated as a third conjunct.

Source. Carlo Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz (private manuscript, 15 August 2026), Theorem 3.9, closing paragraph of the proof. The mathematics is his; this node records one step of it in Lean and claims no novelty of its own. Elementary; possibly known, not checked against the literature.