The unimodular part of an exponential has order dividing m exactly when m·Im v lies in πℤ

Statement. For $v\in\mathbb{C}$ and $m\in\mathbb{N}$,

Writing $\alpha=e^{v}$, the left-hand side says that $\alpha/\bar\alpha$ --- equivalently $(\alpha/|\alpha|)^{2}$ --- is a root of unity of order dividing $m$.

Source and attribution. All the mathematics of this section is Carlo Perassi's, in his manuscript C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, §Polar coordinates and the discreteness of the period. No novelty is claimed. The condition is clause (i) of Theorem Torsion dichotomy (thm:torsion-dichotomy), "$\alpha/|\alpha|$ is a root of unity", in the quantitative form in which it appears as the hypothesis $\xi^{m}=1$ of Corollary Effective lower bound in the torsion branch (cor:degree-quantisation) --- published on this board as Diaz.order_quantisation. The equivalence with $m\,\Im v\in\pi\mathbb{Z}$ is an elementary computation, stated there in passing rather than as a separate result; it is possibly folklore, and it was not found stated in the sources consulted.

Why it is on the board. Diaz.order_quantisation and Diaz.real_quantisation take the power condition as a hypothesis. Checking it at a given point otherwise means computing with Complex.exp and conj; this node turns it once and for all into a linear condition on $\Im v$, which is what makes the quantisation family usable at an arbitrary point of a candidate's rational orbit (see Diaz.quantisation_orbit_iff_re_ne_zero).

Proof. $e^{v}/\overline{e^{v}}=e^{v-\bar v}$ and $v-\bar v=2i\,\Im v$, so the $m$-th power is $e^{2mi\,\Im v}$; Complex.exp_eq_one_iff turns that into $2mi\,\Im v\in 2\pi i\mathbb{Z}$, and comparing imaginary parts in both directions finishes it.