The logarithmic unit image is discrete

Given: The Axiom of Choice, a number field $K$ of degree $n=[K:\mathbb{Q}]$ with logarithmic embedding $\lambda$ and hyperplane $H$ (Logarithmic embedding of a number field), and a bounded subset $C\subseteq H$.

The map $\lambda$ is given by $\lambda (x)=(\log \mathrm{\mid }{\sigma }_{1}x\mathrm{\mid },\dots ,\log \mathrm{\mid }{\sigma }_{r_1}x\mathrm{\mid },2\log \mathrm{\mid }{\tau }_{1}x\mathrm{\mid },\dots ,2\log \mathrm{\mid }{\tau }_{r_2}x\mathrm{\mid })$, with ${\sigma }_1,\dots ,{\sigma }_{r_1}$ the real embeddings and ${\tau }_1,\dots ,{\tau }_{r_2}$ one embedding from each complex conjugate pair (Logarithmic embedding of a number field, Archimedean embeddings and signature).

For every unit $u\in {\mathcal{O}}_K^{\times }$ one has $\lambda (u)\in H$, so $\lambda ({\mathcal{O}}_K^{\times })$ is a subgroup of the finite-dimensional real vector space $H$ (Unit logarithms lie in the trace-zero hyperplane).

For a subgroup $\mathrm{\Gamma }$ of a finite-dimensional real vector space with the topology induced by a norm, $\mathrm{\Gamma }$ is discrete if and only if every bounded subset of the space meets $\mathrm{\Gamma }$ in a finite set (Discrete subgroups of a real vector space are lattices).

The natural logarithm is strictly increasing with inverse the exponential function on $(0,\mathrm{\infty })$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The exponential function is strictly increasing, The natural logarithm as the inverse of the exponential function); hence for real $a>0$ and real $t$, $a\le e^t$ if and only if $\log a\le t$, and similarly $\log a\ge -t$ if and only if $a\ge e^{-t}$.

For fixed $n\ge 1$ and $R\ge 1$, only finitely many monic integer polynomials of degree at most $n$ have all their complex roots of modulus at most $R$ (Bounded roots give finitely many monic integer polynomials). This batch-2 supplier is authored in this run, and the exact obligation used is the instance for the fixed real $R=e^M\ge 1$ of the argument.

For $u\in {\mathcal{O}}_K^{\times }$ the minimal polynomial $m_u\in \mathbb{Z}[X]$ is monic of degree $[\mathbb{Q}(u):\mathbb{Q}]$, which divides $n$; its complex roots are exactly the numbers $\psi (u)$, where $\psi$ ranges over the $\mathbb{Q}$-embeddings $K\to \mathbb{C}$ (Minimal-polynomial criterion for algebraic integers, The degree of an intermediate field divides the degree of a finite extension, $F$-embeddings of $F(\alpha )$ into an algebraically closed field correspond to the distinct roots of $m_{\alpha }$, Restriction partitions embeddings in a finite tower into extension fibres).

A nonzero polynomial of degree at most $n$ over $\mathbb{C}$ has at most $n$ distinct roots (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

The kernel of $\lambda {\mathrm{\mid }}_{{\mathcal{O}}_K^{\times }}$ is finite (Kernel of the unit logarithm is the roots of unity).

The Axiom of Choice is assumed; it is used only through the AC-qualified hyperplane lemma [F2] (The Axiom of Choice).