Leopoldt's conjecture holds in CM fields for odd $p$

Read-back. Fix a natural number $p$ carrying the instance-level assumption that $p$ is prime, together with an explicit hypothesis $\mathrm{Odd}\,p$ (so $p$ is an odd prime; $p = 2$ is excluded, and no further condition on $p$ is imposed). Fix a type $K$ in an arbitrary universe, equipped with a field structure and with the assumption that $K$ is a number field (a finite-dimensional extension of $\mathbb{Q}$, in particular of characteristic zero), and with the further class assumption that $K$ is a CM field, which unfolds to: every infinite place of $K$ is complex, and $K$ is a degree-$2$ extension of its maximal real subfield

$$K^{+} \;=\; \{x \in K \;:\; \overline{\varphi(x)} = \varphi(x)\ \text{ for every ring homomorphism } \varphi : K \to \mathbb{C}\}.$$

Under these hypotheses the theorem asserts a single equation between natural numbers, spelled out below.

The objects involved, unfolded. Let $\mathcal{O}_K$ be the ring of integers of $K$. Let

$$S_p \;=\; \{\, v \;:\; v \text{ a height-one prime of } \mathcal{O}_K \text{ (i.e. a nonzero prime ideal) with } p \cdot 1_{\mathcal{O}_K} \in v \,\}$$

be the set of nonzero primes of $\mathcal{O}_K$ whose ideal contains the image of the integer $p$ — i.e. the primes above $p$ — regarded as a subtype; the bundle also supplies a proof that $S_p$ is finite. Nothing in the definitions requires $S_p$ to be nonempty: if it were empty, all the groups below would be trivial groups. For each $v \in S_p$, let $K_v$ be the $v$-adic completion of $K$ and $\mathcal{O}_v \subseteq K_v$ its valuation subring (the elements of valuation $\le 1$), and put

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

the (dependent) product of the unit groups of these local integer rings, an abelian group carrying the product topology, where each $\mathcal{O}_v^{\times}$ is topologised as a subspace of $\mathcal{O}_v \times \mathcal{O}_v$ via $u \mapsto (u, u^{-1})$ and $\mathcal{O}_v$ carries the subspace topology from $K_v$.

Let

$$\iota : \mathcal{O}_K^{\times} \longrightarrow U, \qquad \iota(\varepsilon) \;=\; \big(\text{image of } \varepsilon \text{ under } \mathcal{O}_K \to \mathcal{O}_v\big)_{v \in S_p}$$

be the diagonal group homomorphism induced componentwise by the canonical algebra maps, and let $E = \iota(\mathcal{O}_K^{\times})$ be its image subgroup (the image of the whole unit group, torsion included). For each natural number $n \ge 0$ let $U^{p^{n+1}} = \{\,u^{p^{n+1}} : u \in U\,\}$ be the image subgroup of the $p^{n+1}$-st power map on $U$. Define

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

the intersection, over all $n = 0, 1, 2, \dots$ (so over exponents $p, p^2, p^3, \dots$), of the subgroups of $U$ generated by $E$ together with the $p^{n+1}$-st powers; since $U$ is abelian, each such join is the set of products $\varepsilon \cdot u^{p^{n+1}}$ with $\varepsilon \in E$, $u \in U$.

Next, for a natural number $b$ and a subgroup $H$ of an abelian topological group $G$, define

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

where $\mathbb{Z}_p$ denotes the $p$-adic integers, $\mathbb{Z}_p^{\,n}$ means functions from an $n$-element index set to $\mathbb{Z}_p$ with the product topology and its additive group structure (written multiplicatively in the code), and $f$ is required only to be a continuous injective homomorphism of abstract groups landing inside $H$ — no $\mathbb{Z}_p$-linearity, no closed image, no topological embedding onto its image is demanded. The supremum is taken in $\mathbb{N}$; the defining set always contains $n = 0$ (the trivial homomorphism from the trivial group qualifies) and is bounded above by $b$, so $\rho_p(b,H)$ is the largest such $n$, and in particular $\rho_p(b,H) \le b$ always.

The assertion. Writing $r = \mathrm{card}\,\{\text{infinite places of } K\} - 1$ for the unit rank of $K$ (Dirichlet's rank, with truncated natural-number subtraction) and $d = [K : \mathbb{Q}] = \dim_{\mathbb{Q}} K$, define the defect

$$\delta_p(K) \;=\; r \; \dot- \; \rho_p\big(d, \overline{E}\big),$$

where $\dot-$ is truncated subtraction on $\mathbb{N}$ (it yields $0$ whenever $\rho_p(d,\overline{E}) \ge r$). The theorem states

$$\delta_p(K) \;=\; 0,$$

which, because of the truncation, is exactly the inequality

$$r \;\le\; \rho_p\big(d, \overline{E}\big):$$

there exists a natural number $n$ with $r \le n \le d$ and an injective continuous group homomorphism from $\mathbb{Z}_p^{\,n}$ into $\prod_{v \mid p} \mathcal{O}_v^{\times}$ whose image lies inside $\bigcap_{n} \big(E \vee U^{p^{n+1}}\big)$ — or else $r = 0$, in which case the equation holds automatically. No lower bound on $\rho_p(d,\overline{E})$ beyond this is asserted, and no claim of equality between $\rho_p(d,\overline{E})$ and $r$ is made.