At most two points of an exponential fibre have algebraic modulus

For $\alpha \in \mathbb{C}$ put

Then $\#E_\alpha \le 2$: three pairwise distinct points of $E_\alpha$ cannot exist.

Where this sits. This is the main clause of Corollary 2.4 (cor:fibre, Two-point algebraic-fibre bound) of the manuscript. It is unconditional — no unproved transcendence input enters.

Proof. Two points of one exponential fibre differ by an integer multiple of $2\pi i$, so with $c = 2\pi i$ the three points are $u$, $u + mc$, $u + nc$ with $m \neq n$ both non-zero. Since $\bar c = -c$,

a quadratic in $k$ whose leading coefficient is $-c^{2} = 4\pi^{2}$. Three algebraic values at distinct integers make that leading coefficient algebraic (Diaz.second_difference_mem), hence $(\pi i)^{2} = -\pi^{2}$ is algebraic, hence $\pi i$ is algebraic. But $\pi i \neq 0$ and $e^{\pi i} = -1$ is algebraic, so Hermite–Lindemann makes $\pi i$ transcendental. Contradiction.

The Lean carries the Lindemann–Weierstrass development inline, since it is not in this Mathlib revision; the form used is the one already on this mission as Diaz.transcendental_of_candidate.

Two remarks on the hypotheses. The statement does not assume $\alpha$ algebraic, nor even $\alpha \neq 0$: the bound holds for every exponential fibre. And only the squared moduli are assumed algebraic, which is the same condition as $|u| \in \bar{\mathbb{Q}}$ but avoids a square root in the formalisation.

The two remaining clauses of Corollary 2.4 — that a real $\alpha$ gives a conjugate pair, and that for non-real $\alpha$ two points have squared-modulus ratio in $\bar{\mathbb{Q}} \setminus \mathbb{Q}$ — depend on Theorem 2.3, whose input (Roy–Waldschmidt) is not formalisable here, and are not published.

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.