Kronecker-Weber, wild step for $p = 2$: an abelian field of degree $2^k$ unramified outside $2$ lies in $\mathbb{Q}(\zeta_{2^N})$

Let $K$ be a finite abelian extension of $\mathbb{Q}$ of degree $2^k$. Assume that each odd prime $\ell$ is unramified in $K$. The statement asserts that there is $N \ge 0$ and an embedding of fields

Proof idea. The quadratic fields unramified outside $2$ are $\mathbb{Q}(i)$, $\mathbb{Q}(\sqrt{2})$ and $\mathbb{Q}(\sqrt{-2})$, by Minkowski's bound or a discriminant computation. If $K$ is real, its Galois group has exactly one subgroup of index $2$ (the only real quadratic field unramified outside $2$ is $\mathbb{Q}(\sqrt 2)$), so it is cyclic, and $K$ is the real subfield of degree $2^k$ of $\mathbb{Q}(\zeta_{2^{k+2}})$ by the compositum argument of the odd case. In general, $K(i)$ is abelian of $2$-power degree and unramified outside $2$, and it is the compositum of $\mathbb{Q}(i)$ and its maximal real subfield, so $K \subseteq K(i) \subseteq \mathbb{Q}(\zeta_{2^N})$.

Use. With the tame step (NumberField.exists_isUnramifiedIn_le_sup_of_prime_ne) this gives the Kronecker-Weber theorem for abelian fields of $2$-power degree. This is a child of Leopoldt.exists_algHom_cyclotomicField_of_isCyclic_primePow.

Formalization Note. "Abelian" is IsAbelianGalois ℚ K; "$\ell$ unramified in $K$" is Algebra.IsUnramifiedIn (𝓞 K) (Ideal.span {(ℓ : ℤ)}); the conclusion is Nonempty (K →ₐ[ℚ] CyclotomicField (2 ^ N) ℚ). For $k = 0$ take $N = 0$. The platform has the quadratic case (NumberField.exists_algHom_cyclotomicField_of_finrank_le_two) and the exponent-two case (NumberField.exists_algHom_cyclotomicField_of_exponent_two), but with an unspecified cyclotomic field; here the conductor must be a power of $2$. Mathlib has ZMod.isCyclic_units_two_pow_iff, ZMod.orderOf_five and IsCyclotomicExtension.Rat.galEquivZMod.