Waldschmidt's bound $\mathcal{D}_L(\mathbb{K}) \le r/2$ for unit rank $r \ge 3$

Let $p$ be a prime and $\mathbb{K}$ a number field whose unit group $E = \mathcal{O}(\mathbb{K})^\times$ has Dirichlet rank $r = \mathbb{Z}\text{-rk}(E) \ge 3$. With $U = \prod_{\wp \mid p}\mathcal{O}_\wp^\times$ the semilocal units at $p$, $\iota : E \to U$ the diagonal embedding and $\bar E = \bigcap_{n>0}\iota(E)\cdot U^{p^n}$ the $p$-adic closure of the units, the Leopoldt defect satisfies

This is Waldschmidt's theorem restricted to unit rank at least $3$, which is exactly the range in which it goes beyond the elementary bound $\mathcal{D}_L(\mathbb{K}) \le r - 1$ (a unit of infinite order generates a copy of $\mathbb{Z}_p$ in $\bar E$). Its proof is transcendence theory: a $p$-adic lower bound for the rank of matrices of $p$-adic logarithms of algebraic numbers, applied to the logarithms of the conjugates of a system of fundamental units. Together with the elementary bound it gives Waldschmidt's inequality for every number field.

Formalization Note The right-hand side is $\lfloor r/2 \rfloor$ (division in $\mathbb{N}$), matching the milestone Leopoldt.defect_le_rank_div_two, of which this is the case $r \ge 3$.