Solution (source code)

= Solution

Normalize the <discrete valuation> by $v_L(\pi_L)=1$, and put $v_L(0)=+\infty$. For $\sigma\ne1$, define its ramification number
$$
i_G(\sigma)=\min_{a\in\mathcal O_L}v_L(\sigma(a)-a),
$$
and set $i_G(1)=+\infty$. The minimum exists: all finite values are nonnegative integers, and a nonidentity automorphism moves some integral element. The <lower ramification numbering> is
$$
\boxed{G_s=\{\sigma\in G:i_G(\sigma)\geq s+1\}\quad(s\in\mathbb R_{\geq0}).}
$$
Thus $G_s=G_{\lceil s\rceil}$, $G_0$ is the <inertia group>, and $G_1$ is the <wild inertia group>. This states the convention at integer endpoints as well as between them. Automorphisms preserve $v_L$, so these are normal subgroups of $G$.

Define the <Herbrand function> and its inverse by
$$
\varphi_{L/K}(s)=\int_0^s\frac{dt}{[G_0:G_t]},\qquad
\psi_{L/K}=\varphi_{L/K}^{-1}.
$$
The integrand is positive and piecewise constant. Since $G_t=1$ for sufficiently large $t$, the function is continuous, strictly increasing and unbounded, and its inverse is defined on all nonnegative reals. The <upper ramification numbering> is
$$
\boxed{G^u=G_{\psi_{L/K}(u)}\quad(u\geq0).}
$$
In particular, the denominator in the Herbrand integral involves $G_0$, even when $L/K$ is not totally ramified. These conventions are also given in https://www.jmilne.org/math/CourseNotes/CFT.pdf[Milne's Class Field Theory, Chapter I, §4].

Now use the monogenic hypothesis $\mathcal O_L=\mathcal O_K[\alpha]$. Since $L/K$ is Galois, its minimal polynomial has the distinct conjugates $\sigma(\alpha)$ as roots, so
$$
f'(\alpha)=\prod_{\sigma\ne1}(\alpha-\sigma(\alpha)).
$$
Taking valuations proves the first equality.

For every polynomial $P\in\mathcal O_K[T]$, the difference $P(\sigma(\alpha))-P(\alpha)$ is divisible in $\mathcal O_L$ by $\sigma(\alpha)-\alpha$. Every element of $\mathcal O_L$ is such a polynomial value, and taking the element $\alpha$ attains the resulting lower bound. Hence
$$
i_G(\sigma)=v_L(\sigma(\alpha)-\alpha)\quad(\sigma\ne1).
$$
For an integer $i_G(\sigma)=m\geq0$, the element $\sigma$ lies in exactly the groups $G_0,\ldots,G_{m-1}$; if $m=0$, it lies in none. Summing this count over the nonidentity elements and interchanging the two finite sums gives
$$
\boxed{v_L(f'(\alpha))
=\sum_{\sigma\ne1}v_L(\sigma(\alpha)-\alpha)
=\sum_{s\in\mathbb Z_{\geq0}}(|G_s|-1).}
$$
This proves the <ramification-group sum for a monogenic integer ring>. Equivalently it is the <different exponent from ramification groups>, since the <different ideal> is generated by $f'(\alpha)$ under the same monogenic hypothesis.