A candidate has a four-point orbit and its rational conjugate-plane meets the modulus condition only on the axes

Let $\bar{\mathbb{Q}}$ denote the algebraic numbers. Following the mission's convention, call a complex number $u$ a candidate when $u\neq 0$, $|u|$ is algebraic, and $\exp(u)$ is algebraic; a candidate is exactly a counterexample to Diaz's modulus conjecture, so the conjecture asserts that none exists.

This theorem collects four rigidity properties that a single candidate $u$ would have to satisfy simultaneously.

1. The orbit is a set of candidates. Each of $u$, $-u$, $\bar{u}$, $-\bar{u}$ is again a candidate.

2. The orbit has exactly four points. The four numbers $u$, $-u$, $\bar{u}$, $-\bar{u}$ are pairwise distinct. In particular a candidate is neither real nor purely imaginary.

3. The conjugate is not an algebraic multiple. For every algebraic $\gamma$ one has $\bar{u}\neq \gamma u$; so $u$ and $\bar{u}$ span a genuinely two-dimensional $\bar{\mathbb{Q}}$-configuration, not a line.

4. The rational plane through $u$ and $\bar{u}$ meets the modulus condition only on the two axes. For rational $a,b$,

Clause 4 is the substantive one. Since $\exp$ is not involved in it, it says that the modulus half of the candidate condition already isolates the two lines $\mathbb{Q}u$ and $\mathbb{Q}\bar{u}$ inside their rational span: no genuinely mixed rational combination of a candidate with its conjugate has algebraic absolute value. Combined with clause 1, the four points of clause 2 are the only points of the rational plane that can meet the candidate locus at all.

The statement is unconditional: no transcendence conjecture is assumed. It packages, in the conjecture's own vocabulary, facts previously available only in the manuscript vocabulary of the $\texttt{Diaz.*}$ family (where the locus is written out as the three hypotheses $u\neq0$, $\exp u$ algebraic, $u\bar{u}$ algebraic) or only over an abstract base subfield.

Formalization Note Complex conjugation is starRingEnd ℂ, written conj after open ComplexConjugate. The modulus clause is stated as IsAlgebraic ℚ ((‖·‖ : ℝ) : ℂ), matching DiazModulus.IsCandidate; passing between it and algebraicity of $u\bar{u}$ is the content of Diaz.normal_form.