Rational rays force algebraic dependence: exclusivity in the pair dichotomy

Let $u \in \mathbb{C}$ be such that $u\bar u$ is algebraic over $\mathbb{Q}$, and let $v$ be a non-zero rational multiple of either $u$ or $\bar u$:

Then $u$ and $v$ are algebraically dependent over $\mathbb{Q}$.

Where this sits. This is the opening paragraph of the proof of Theorem 2.5 (thm:pair-dichotomy, Pair dichotomy: rational proportionality or independence) of the manuscript — the clause that makes the dichotomy exclusive. Theorem 2.5 asserts that for $u,v$ on the Diaz locus with $|v|^2/|u|^2 \in \mathbb{Q}$, exactly one of

• (i) $v \in \mathbb{Q}^\times u \,\dot\cup\, \mathbb{Q}^\times\bar u$,
• (ii) $u$ and $v$ are algebraically independent over $\mathbb{Q}$

holds. The implication (i) $\Rightarrow \neg$(ii) is this node, and it is unconditional: it uses no transcendence input whatever. The opposite direction $\neg$(ii) $\Rightarrow$ (i) is the deep half — it passes through Théorème 0.2 of Roy–Waldschmidt (1997), which is not available in this Mathlib revision, and then through the linear-algebra step already published as Diaz.rational_singular_subspace_classification and Diaz.rational_subspace_quadric_ratios.

Proof. Write $q = u\bar u$.

Case $v = cu$, $c \in \mathbb{Q}^\times$. The non-zero polynomial $X_1 - cX_0 \in \mathbb{Q}[X_0,X_1]$ vanishes at $(u,v)$.

Case $v = c\bar u$, $c \in \mathbb{Q}^\times$. Then $uv = c\,u\bar u = cq$, which is algebraic over $\mathbb{Q}$ because $q$ is and $c$ is rational. Let $f = \operatorname{minpoly}_{\mathbb{Q}}(cq)$, a non-zero polynomial with $f(cq) = 0$, and set $P(X_0,X_1) = f(X_0X_1)$. Then

and $P \neq 0$ because the substitution $T \mapsto X_0X_1$ is an injective $\mathbb{Q}$-algebra map $\mathbb{Q}[T] \to \mathbb{Q}[X_0,X_1]$ — it admits the left inverse $X_0 \mapsto T$, $X_1 \mapsto 1$, under which $T \mapsto X_0X_1 \mapsto T$.

In both cases a non-zero rational polynomial annihilates $(u,v)$, so the pair is not algebraically independent.

Formalisation notes. "Algebraically dependent over $\mathbb{Q}$" is rendered ¬ AlgebraicIndependent ℚ ![u, v]. Two hypotheses of the manuscript's setting are deliberately not assumed, because the argument does not use them: $u \neq 0$ (the statement holds for $u = 0$ too, where $X_0$ itself annihilates the pair), and the algebraicity of $e^u$. Only $u\bar u \in \overline{\mathbb{Q}}$ is used, so the node applies verbatim off the Diaz locus.

Source. Carlo Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz (private manuscript, 15 August 2026), Theorem 2.5, first 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.