Leopoldt's conjecture via $r$ Galois conjugates of a Minkowski unit

Let $K/\mathbb{Q}$ be a finite Galois extension with group $G$, $p$ a prime, and $r$ the unit rank of $K$. Let $\varepsilon\in\mathcal{O}_K^\times$ be a Minkowski unit: its conjugates $\{\sigma\varepsilon\}_{\sigma\in G}$ generate a subgroup of finite index in $\mathcal{O}_K^\times$ (such units exist by NumberField.Units.exists_minkowskiUnit). Assume every conjugate lies in the logarithm ball at every prime $v\mid p$:

Write $\Lambda(x)=(\log_p\iota_v(x))_{v\mid p}\in\prod_{v\mid p}K_v$. Then Leopoldt's conjecture holds for $(K,p)$ if and only if one can pick $r$ automorphisms $\sigma_1,\dots,\sigma_r\in G$ such that

are linearly independent over $\mathbb{Z}_p$.

Since the $|G|=r_1+2r_2$ conjugates of $\varepsilon$ satisfy at least one relation (their product is the norm $\pm1$), one can at most hope for $r$ independent ones; the theorem says Leopoldt's conjecture is exactly the statement that the $p$-adic logarithms of the conjugates of a Minkowski unit have the maximal possible $\mathbb{Z}_p$-rank $r$. This is the starting point of Ax's and Brumer's treatment of the abelian case, where the $\mathbb{Z}_p$-rank is then computed via the group determinant of $G$. The Galois action here is $\sigma\varepsilon$ = image of $\varepsilon$ under the ring automorphism of $\mathcal{O}_K$ induced by $\sigma$.