$\mathbb{Z}_p\text{-rk}(\overline{E}) \le \mathbb{Z}\text{-rk}(E)$: the Leopoldt defect is non-negative

Let $p$ be a prime and $K$ a number field with unit group $E = \mathcal{O}_K^\times$ and Dirichlet unit rank $r = r_1 + r_2 - 1 = \mathbb{Z}\text{-rk}(E)$. Let $U = \prod_{\wp \mid p} \mathcal{O}_{K_\wp}^\times$ be the semilocal units at $p$, $\iota : E \to U$ the diagonal embedding, and

the $p$-adic closure of the global units. Then the $\mathbb{Z}_p$-rank of $\overline{E}$ never exceeds the $\mathbb{Z}$-rank of $E$:

Equivalently, the Leopoldt defect $\mathcal{D}_L(K) = \mathbb{Z}\text{-rk}(E) - \mathbb{Z}_p\text{-rk}(\overline{E})$ is a genuine non-negative integer: the truncated subtraction in the mission's definition of defect is never triggered. Leopoldt's conjecture asserts that equality holds.

Formalization Note The $\mathbb{Z}_p$-rank is zpRankBelow p (finrank ℚ K) (unitClosure p K), the largest $n \le [K:\mathbb{Q}]$ such that $\mathbb{Z}_p^n$ admits a continuous injective homomorphism into $U$ with image in $\overline{E}$ (from Definitions.Def_LeopoldtDefect); Dirichlet's unit rank is Mathlib's NumberField.Units.rank K.