A conjugation-stable rational line has a real or imaginary generator

Let $y \in \mathbb{C}$ be irrational (not a rational number), and suppose $\bar y = a + b y$ with $a, b \in \mathbb{Q}$. Then either $b = 1$, $a = 0$ and $y$ is real, or $b = -1$ and $y - a/2$ is purely imaginary.

Where this sits. This is the normalisation step in the proof of Theorem 3.8 (thm:common, Common logarithmic multipliers) of the manuscript: "If $K_u \neq \mathbb{Q}$, write $K_u = \mathbb{Q} \oplus \mathbb{Q}y_1$. From $\bar y_1 = a + b y_1$, conjugation gives $b^{2} = 1$ and $a(1+b) = 0$. For $b = 1$, take the real generator $y_0 = y_1$; for $b = -1$, the generator $y_0 = y_1 - a/2$ is purely imaginary." The hypothesis that $y$ is irrational is what the $\mathbb{Q}$-independence of $1$ and $y_1$ supplies.

Proof. Applying conjugation twice gives $y = a + b(a + by)$, that is $(b+1)\bigl((1-b)y - a\bigr) = 0$. If $b \neq \pm 1$ this makes $y = a/(1-b)$ rational. For $b = 1$ the same relation forces $2a = 0$, so $\bar y = y$. For $b = -1$ it is vacuous, and $\overline{y - a/2} = a - y - a/2 = -(y - a/2)$.

What is deliberately not claimed. The substance of Theorem 3.8 — that $\dim_{\mathbb{Q}} K_u \le 2$, that $K_u \cap \widetilde{\mathcal{L}} = \mathbb{Q}$, and that every $y \in K_u \setminus \mathbb{Q}$ gives $\operatorname{trdeg}_{\mathbb{Q}}\mathbb{Q}(u,y) = 2$ — uses the six exponentials theorem, Diaz's Theorem 3(1) and Waldschmidt's $2 \times 2$ transcendence-degree estimate, none of which is available in Mathlib. Only the shape of the generator is recorded here.

Elementary; possibly known, not checked against the literature.

Source. Carlo Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz (private manuscript, 15 August 2026). The mathematics is his; this node only records one step of it in Lean, and claims no novelty of its own.