$\mathbb{Z}\text{-rk}(E) = \mathcal{D}_L(K) + \mathbb{Z}_p\text{-rk}(\overline{E})$

Let $p$ be a prime and $K$ a number field, with $E = \mathcal{O}_K^\times$ and $\overline{E}$ the $p$-adic closure of $\iota(E)$ in the semilocal units $U = \prod_{\wp\mid p}\mathcal{O}_{K_\wp}^\times$. Then Dirichlet's unit rank splits as the Leopoldt defect plus the $\mathbb{Z}_p$-rank of the closure:

This is the defining relation $\mathcal{D}_L(K) = \mathbb{Z}\text{-rk}(E) - \mathbb{Z}_p\text{-rk}(\overline{E})$ read as an identity of natural numbers; it holds exactly because $\mathbb{Z}_p\text{-rk}(\overline{E}) \le \mathbb{Z}\text{-rk}(E)$, so that the truncated subtraction used in the Lean definition of defect coincides with the true difference. It lets one move freely between statements about the defect and statements about the rank of $\overline{E}$.

Formalization Note defect p K is Units.rank K - zpRankBelow p (finrank ℚ K) (unitClosure p K) with truncated natural-number subtraction (Definitions.Def_LeopoldtDefect).