The four-point orbit of a candidate on its circle

Let $u \neq 0$ with $e^{u}$ and $u\bar u$ algebraic. Then each of

is again such a point and has the same squared modulus $u\bar u$, and the four are pairwise distinct.

Where this sits. This is the orbit clause of Corollary 2.6 (cor:same-circle-independence, Same-circle independence) of the manuscript: "The four points are distinct because $u$ is off the axes, and all lie in $\mathcal{D} \cap C_r$: the set $\mathcal{D}$ is stable under negation and conjugation, and both preserve the modulus."

Proof. $e^{-u} = (e^{u})^{-1}$ and $e^{\bar u} = \overline{e^{u}}$ are algebraic, the first because the inverse of a non-zero algebraic number is algebraic, the second because complex conjugation is a $\mathbb{Q}$-algebra map of $\mathbb{C}$. The moduli agree by a one-line computation. Distinctness reduces to $u \neq 0$ together with $\bar u \neq u$ and $\bar u \neq -u$; those two are Hermite–Lindemann, since $\bar u = \pm u$ makes $u^{2} = \pm u\bar u$ algebraic and hence $u$ algebraic, while $u \neq 0$ has algebraic exponential.

What is deliberately not claimed. The substance of Corollary 2.6 — that two candidates on one centered algebraic circle are algebraically independent unless they lie in a common orbit, and that $\mathcal{D} \cap C_r \cap \overline{\mathbb{Q}(u)}$ is exactly this orbit — descends from Theorem 2.5 (thm:pair-dichotomy) and through it from Theorem 0.2 of Roy–Waldschmidt. That input is not available in Mathlib and nothing of it is asserted here. This node records only that the orbit exists, is genuinely of size four, and stays inside the locus.

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.