Waldschmidt's bound $\mathcal{D}_L(\mathbb{K}) \le r/2$

Statement. For every natural number $p$ that is assumed prime, and for every field $K$ that is assumed to be a number field (a finite extension of $\mathbb{Q}$), the assertion is the inequality of natural numbers

$$\mathrm{defect}(p, K) \;\le\; \left\lfloor \frac{r(K)}{2} \right\rfloor ,$$

where $r(K)$ is the unit rank of $K$ and $\mathrm{defect}(p,K)$ is the quantity defined below. Both $p$ and $K$ are universally quantified; the only hypotheses are that $p$ is prime and that $K$ is a number field. The division by $2$ is truncated division of natural numbers, i.e. the floor of $r(K)/2$.

The unit rank $r(K)$. This is Mathlib's NumberField.Units.rank K, defined as

$$r(K) \;=\; \#\{\text{infinite places of } K\} - 1 ,$$

a truncated subtraction of natural numbers (so $r(K) = r_1 + r_2 - 1$ in the usual notation).

The primes above $p$. Let

$$S_p \;=\; \{\, v \;:\; v \text{ a nonzero prime ideal of } \mathcal{O}_K \text{ (a point of the height-one spectrum, i.e. a prime ideal that is nonzero) and } p \cdot 1 \in v \,\},$$

the (finite) set of primes of the ring of integers $\mathcal{O}_K$ containing the image of $p$. For each such $v$, let $K_v$ be the completion of $K$ at the $v$-adic valuation and $\mathcal{O}_{K_v} \subseteq K_v$ its valuation subring (the elements of valuation $\le 1$).

The semilocal unit group. Set

$$\mathcal{U} \;=\; \prod_{v \in S_p} \mathcal{O}_{K_v}^{\times},$$

the direct product, over the primes $v$ of $\mathcal{O}_K$ above $p$, of the unit groups of these complete valuation rings, regarded as a commutative topological group with the product of the natural topologies on each $\mathcal{O}_{K_v}^{\times}$.

The diagonal embedding. Let

$$\iota : \mathcal{O}_K^{\times} \longrightarrow \mathcal{U}, \qquad \iota(u) = \big( \text{image of } u \text{ in } \mathcal{O}_{K_v}^{\times} \big)_{v \in S_p},$$

the group homomorphism induced componentwise by the structure maps $\mathcal{O}_K \to \mathcal{O}_{K_v}$.

The "closure" subgroup. Let $E = \iota(\mathcal{O}_K^{\times}) \le \mathcal{U}$ be the image of $\iota$, and for each natural number $n \ge 0$ let $\mathcal{U}^{p^{n+1}} = \{\, x^{p^{n+1}} : x \in \mathcal{U} \,\}$ be the image of the $p^{n+1}$-power endomorphism. Define

$$\overline{E} \;=\; \bigcap_{n \in \mathbb{N}} \Big( E \vee \mathcal{U}^{p^{n+1}} \Big),$$

the infimum, in the lattice of subgroups of $\mathcal{U}$, of the joins $E \vee \mathcal{U}^{p^{n+1}}$; since $\mathcal{U}$ is commutative each join is the subgroup $\{\, \iota(u)\, x^{p^{n+1}} : u \in \mathcal{O}_K^{\times},\ x \in \mathcal{U} \,\}$, and the index $n$ runs over all of $\mathbb{N}$, so the exponents occurring are $p^1, p^2, p^3, \dots$ (never $p^0 = 1$).

The bounded $\mathbb{Z}_p$-rank. For a commutative topological group $G$, a natural number $b$, and a subgroup $H \le G$, define

$$\rho_p(b, H) \;=\; \sup \Big\{\, n \in \mathbb{N} \;:\; n \le b \ \text{ and } \ \exists\, f : \big(\mathbb{Z}_p^{\,n}, +\big) \to G \text{ a group homomorphism that is injective, continuous, and satisfies } f(x) \in H \text{ for all } x \,\Big\},$$

where $\mathbb{Z}_p^{\,n}$ carries the product of the $p$-adic topologies and is written multiplicatively, and the supremum is the supremum of a set of natural numbers. The condition asked of $f$ is exactly: it is a homomorphism, it is injective, it is continuous, and its whole image lies in $H$ — nothing more (in particular $f$ is not required to be a topological embedding, nor to have closed image). The defining set always contains $n = 0$ (the group $\mathbb{Z}_p^{\,0}$ is trivial, and the unique map into $G$ is injective, continuous, and lands on the identity, which belongs to every subgroup), and every element is $\le b$, so the supremum is attained and equals the largest such $n$.

The defect. Finally,

$$\mathrm{defect}(p,K) \;=\; r(K) \;-\; \rho_p\big([K : \mathbb{Q}],\ \overline{E}\big),$$

using the truncated subtraction of natural numbers (the value is $0$ whenever the second term is at least $r(K)$), and with the bound taken to be $[K:\mathbb{Q}] = \dim_{\mathbb{Q}} K$.

Edge cases silently included by the quantifiers. The claim is asserted for every prime $p$ and every number field $K$, including $K = \mathbb{Q}$ and the imaginary quadratic fields, where $r(K) = 0$; in those cases the right-hand side is $\lfloor 0/2 \rfloor = 0$ and the left-hand side is also $0$ because of truncated subtraction. More generally, whenever $\rho_p([K:\mathbb{Q}], \overline{E}) \ge r(K)$ the left-hand side is $0$ by truncation, independently of how large $\rho_p$ is. The set $S_p$ of primes above $p$ is nonempty for a prime $p$, but the statement itself imposes no condition on its size, on ramification, or on the splitting of $p$. Nothing in the statement asserts $\mathrm{defect}(p,K) = 0$; the separately defined proposition "$\mathrm{defect}(p,K) = 0$" is not referenced here.