Quantisation of the real branch: a candidate with real exponential has $|u|^2 > \pi^2$

Source. This is Carlo Perassi's mathematics, from his unpublished note on Diaz's modulus conjecture, section Polar coordinates and the discreteness of the period, statement Theorem (Quantisation of the real branch). Published on his mission with his permission. No novelty is claimed for it here; the argument is elementary, and it is possibly known — it has not been checked against the literature.

Statement. Let $u \in \mathbb{C}$ lie on neither axis ($\Re u \neq 0$, $\Im u \neq 0$) and suppose $e^{u}$ is real. Then $\Im u \in \pi\mathbb{Z}$, and consequently

What it says in the mission's terms. On the Diaz locus the two axis exclusions are supplied by Diaz.not_on_axes, so every candidate whose exponential is real satisfies them. The conclusion is that the real branch of the locus is quantised: its points are $\ell + i n \pi$ with $n \in \mathbb{Z}\setminus\{0\}$, and their norms are bounded below by $\pi^2$ — they cannot accumulate at $0$.

Why the bound is not formal. It is exactly the place where the mission's Laurent shadow model (Diaz.model_falsifies, Diaz.Exp0_*) parts company with the actual exponential. There $\ker \mathrm{Exp}_0$ is a divisible line, the shadow locus is stable under $\mathbb{Q}^\times$, and its norms $q^2\rho$ accumulate at $0$; here $\ker \exp \cap \mathcal{L} = 2\pi i \mathbb{Z}$ is a rank-one lattice inside the divisible line $2\pi i\mathbb{Q}$, and both conclusions fail in the model. The real branch is also, unlike the full locus, not stable under $\mathbb{Q}^\times$: $qu$ has real exponential only when $qn \in \mathbb{Z}$.

Reading the Lean. (Complex.exp u).im = 0 is "$e^{u}$ is real"; Complex.normSq u is $u \bar u$.

Proof. Complex.exp_im gives $(e^{u})_{\mathrm{im}} = e^{\Re u}\sin(\Im u)$, and $e^{\Re u} \neq 0$, so $\sin(\Im u) = 0$ and $\Im u = n\pi$ for some integer $n$. Since $\Im u \neq 0$ we have $n \neq 0$, hence $|\Im u| \geq \pi$ and $(\Im u)^2 \geq \pi^2$; adding $(\Re u)^2 > 0$ gives the strict inequality.