[proofplan]
We derive the ramification formula for a finite abelian extension $M/K$ by projecting the global formula $G^t(K^{\mathrm{ab}}/K) = \operatorname{Gal}(K^{\mathrm{ab}} / K^{\mathrm{ur}} L_{\lceil t \rceil})$ from the [Explicit Reciprocity Law](/theorems/???) onto $\operatorname{Gal}(M/K)$. The key step is that the upper numbering is compatible with quotients: $G^t(M/K) = G^t(K^{\mathrm{ab}}/K) \cdot \operatorname{Gal}(K^{\mathrm{ab}}/M) / \operatorname{Gal}(K^{\mathrm{ab}}/M)$. Under the Artin isomorphism $K^\times / N(M/K) \cong \operatorname{Gal}(M/K)$, the preimage of $G^t(M/K)$ is the image of $U_K^{(\lceil t \rceil)}$ in $K^\times / N(M/K)$, giving the stated formula.
[/proofplan]
[step:Establish the Artin isomorphism for $M/K$ and the norm subgroup correspondence]
Let $M/K$ be a finite abelian extension. By the [Local Artin Reciprocity](/theorems/???), the Artin map induces an isomorphism
\begin{align*}
\operatorname{Art}_K \colon K^\times / N(M/K) \xrightarrow{\;\sim\;} \operatorname{Gal}(M/K),
\end{align*}
where $N(M/K) := N_{M/K}(M^\times)$ is the norm subgroup.
The Artin map for $M/K$ is the composition of the global Artin map $\operatorname{Art}_K \colon K^\times \to \operatorname{Gal}(K^{\mathrm{ab}}/K)$ with the restriction $\operatorname{Gal}(K^{\mathrm{ab}}/K) \twoheadrightarrow \operatorname{Gal}(M/K)$. The kernel of this composition is $\operatorname{Art}_K^{-1}(\operatorname{Gal}(K^{\mathrm{ab}}/M)) = N(M/K)$, by the definition of the norm subgroup in class field theory.
[/step]
[step:Project the upper ramification filtration from $K^{\mathrm{ab}}/K$ to $M/K$]
The upper numbering is compatible with quotients (by the [Compatibility of Upper Numbering with Quotients](/theorems/???)): for a closed normal subgroup $H = \operatorname{Gal}(K^{\mathrm{ab}}/M) \trianglelefteq \operatorname{Gal}(K^{\mathrm{ab}}/K)$,
\begin{align*}
G^t(M/K) = G^t(K^{\mathrm{ab}}/K) \cdot H / H = \frac{G^t(K^{\mathrm{ab}}/K) \cdot \operatorname{Gal}(K^{\mathrm{ab}}/M)}{\operatorname{Gal}(K^{\mathrm{ab}}/M)}.
\end{align*}
By the [Explicit Reciprocity Law](/theorems/???), $G^t(K^{\mathrm{ab}}/K) = \operatorname{Gal}(K^{\mathrm{ab}} / K^{\mathrm{ur}} L_{\lceil t \rceil})$ for $t > -1$, and $\operatorname{Art}_K^{-1}(G^t(K^{\mathrm{ab}}/K)) = U_K^{(\lceil t \rceil)}$.
The projection of $G^t(K^{\mathrm{ab}}/K)$ to $\operatorname{Gal}(M/K)$ under the quotient map $\operatorname{Gal}(K^{\mathrm{ab}}/K) \to \operatorname{Gal}(M/K)$ corresponds, via the Artin map, to the image of $U_K^{(\lceil t \rceil)}$ in $K^\times / N(M/K)$.
[guided]
The compatibility of upper numbering with quotients is the fundamental property that makes the upper numbering useful. In the lower numbering, $G_s(M/K)$ is *not* the image of $G_s(K^{\mathrm{ab}}/K)$ under restriction. But in the upper numbering, this compatibility holds by construction (it is the defining property used by Herbrand to introduce the renumbering).
The abstract statement is: if $G = \operatorname{Gal}(L/K)$ and $H \trianglelefteq G$ corresponds to an intermediate field $M = L^H$, then $G^t(M/K) = G^t \cdot H / H$ (the image of $G^t$ in $G/H$). Applied to $G = \operatorname{Gal}(K^{\mathrm{ab}}/K)$ and $H = \operatorname{Gal}(K^{\mathrm{ab}}/M)$, this gives the formula for $G^t(M/K)$ in terms of the already-computed $G^t(K^{\mathrm{ab}}/K)$.
The Artin map translates this group-theoretic projection into an arithmetic statement. The quotient $\operatorname{Gal}(K^{\mathrm{ab}}/K) \to \operatorname{Gal}(M/K)$ corresponds to the quotient $K^\times \to K^\times / N(M/K)$. The image of $G^t(K^{\mathrm{ab}}/K)$ in $\operatorname{Gal}(M/K)$ corresponds to the image of $\operatorname{Art}_K^{-1}(G^t(K^{\mathrm{ab}}/K)) = U_K^{(\lceil t \rceil)}$ in $K^\times / N(M/K)$.
[/guided]
[/step]
[step:Write down the explicit formula for $G^t(M/K)$ via the Artin map]
Combining the results of the previous steps: the Artin map induces
\begin{align*}
\operatorname{Art}_K \colon \frac{U_K^{(\lceil t \rceil)} \cdot N(M/K)}{N(M/K)} \xrightarrow{\;\sim\;} G^t(M/K).
\end{align*}
To verify this: an element $\sigma \in \operatorname{Gal}(M/K)$ lies in $G^t(M/K)$ if and only if $\sigma$ lifts to an element of $G^t(K^{\mathrm{ab}}/K)$ in $\operatorname{Gal}(K^{\mathrm{ab}}/K)$. Under the Artin map, $\sigma = \operatorname{Art}_K(a)$ for some $a \in K^\times$ (well-defined modulo $N(M/K)$). The element $\sigma$ lifts to $G^t(K^{\mathrm{ab}}/K)$ if and only if $a$ can be chosen so that $\operatorname{Art}_K(a) \in G^t(K^{\mathrm{ab}}/K)$. Since $a$ is determined modulo $N(M/K)$, this means $a \in U_K^{(\lceil t \rceil)} \cdot N(M/K)$. Therefore
\begin{align*}
G^t(M/K) = \operatorname{Art}_K\left(\frac{U_K^{(\lceil t \rceil)} \cdot N(M/K)}{N(M/K)}\right).
\end{align*}
This completes the proof. The formula expresses the upper ramification filtration of any finite abelian extension $M/K$ purely in terms of the norm subgroup $N(M/K)$ and the higher unit group filtration $U_K^{(\lceil t \rceil)}$ of $K$.
[guided]
Let us trace the argument carefully. We have three objects in play:
1. **The Artin map** $\operatorname{Art}_K \colon K^\times \to \operatorname{Gal}(K^{\mathrm{ab}}/K)$ with $\ker(\operatorname{Art}_K|_M) = N(M/K)$.
2. **The global upper ramification** $G^t(K^{\mathrm{ab}}/K)$, computed by the [Explicit Reciprocity Law](/theorems/???): $\operatorname{Art}_K^{-1}(G^t(K^{\mathrm{ab}}/K)) = U_K^{(\lceil t \rceil)}$.
3. **The projection** $\operatorname{Gal}(K^{\mathrm{ab}}/K) \twoheadrightarrow \operatorname{Gal}(M/K)$ with kernel $\operatorname{Gal}(K^{\mathrm{ab}}/M)$.
We want $G^t(M/K) = G^t(K^{\mathrm{ab}}/K) \cdot \operatorname{Gal}(K^{\mathrm{ab}}/M) / \operatorname{Gal}(K^{\mathrm{ab}}/M)$ (compatibility of upper numbering). Under $\operatorname{Art}_K$:
- $G^t(K^{\mathrm{ab}}/K)$ corresponds to $U_K^{(\lceil t \rceil)}$ on the $K^\times$ side.
- $\operatorname{Gal}(K^{\mathrm{ab}}/M)$ corresponds to $N(M/K)$ on the $K^\times$ side.
- The product $G^t \cdot \operatorname{Gal}(K^{\mathrm{ab}}/M)$ corresponds to $U_K^{(\lceil t \rceil)} \cdot N(M/K)$ on the $K^\times$ side.
- The quotient by $\operatorname{Gal}(K^{\mathrm{ab}}/M)$ corresponds to the quotient by $N(M/K)$.
Putting it together:
\begin{align*}
G^t(M/K) = \operatorname{Art}_K\left(\frac{U_K^{(\lceil t \rceil)} \cdot N(M/K)}{N(M/K)}\right).
\end{align*}
This formula is powerful because it reduces the computation of ramification groups — a Galois-theoretic object — to the computation of norm groups, which are often accessible via local reciprocity. For example, if $M/K$ is totally ramified of degree $p^n$ (so that $N(M/K) \supset U_K^{(0)}$ fails, but $N(M/K)$ is still computable), the formula tells us exactly which higher ramification groups are nontrivial.
[/guided]
[/step]
