Auxiliary file: sigma_infinite_iff—the finiteness dichotomy of Remark 1° (p.1031)

sigma K n is infinite exactly when K has equal characteristic p and p divides n ([Serre 1978, Remark 1°, p.1031][Serre1978]). The two directions are separate goals:

• Infinite implies equal characteristic and p ∣ n (eq_and_dvd_of_infinite)—proved, and by the mass formula itself rather than by the tame classification and Krasner's finiteness theorem. Outside the asserted case n survives into 𝒪[K] (eq_and_dvd_of_natCast_eq_zero is the characteristic bookkeeping), so at an Eisenstein generator ξ of any L in sigma K n (exists_eisenstein_generator) the term n * ξ ^ (n - 1) of the derivative of g at ξ has finite valuation n * v + (n - 1), where v is the valuation of n, and orthogonality of the power basis (le_addVal_sum_iff) forbids the other terms from cancelling it: d L ≤ n * v + n - 1 (addVal_derivative_eq_d), a bound uniform in L, that is c L ≤ n * v (c_le_of_mem_sigma). An infinite sigma K n would then feed infinitely many equal nonzero terms into the sum of Theorem 1, forcing it to ⊤ (ENNReal.tsum_const_eq_top_of_ne_zero), while tsum_one_div_q_pow_c evaluates it to n.
• Equal characteristic and p ∣ n implies infinite (infinite_of_eq_of_dvd)—proved by an explicit Eisenstein family rather than by the Artin–Schreier layers the classical argument composes. For each 1 ≤ m the polynomial X ^ n + π ^ m * X + π is Eisenstein, so a root generates a member of sigma K n (isTotallyRamified_adjoin); and because n vanishes in 𝒪[K]—this is where equal characteristic and p ∣ n enter—the term n * X ^ (n - 1) of the derivative dies, leaving the constant π ^ m exactly, so that d L = n * m for the member L it generates (addVal_derivative_eq_d; exists_mem_sigma_d_eq). The discriminant exponent is an invariant of the subfield, so these members are pairwise distinct and m indexes an injection of ℕ into sigma K n.

References

• [Serre1978] J-P. Serre, Une «formule de masse» pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris 286 (1978), Série A, 1031–1036.
• [Serre1979] J-P. Serre, Local fields, Graduate Texts in Mathematics 67, Springer, 1979.

theorem MassFormula.c_le_of_mem_sigma (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] (n t : ℕ) (hn : 0 < n) (ht : (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) ↑n = ↑t) (L : IntermediateField K (SeparableClosure K)) (hL : L ∈ sigma K n) : c L ≤ n * t

The uniform bound behind the finiteness half: when n does not vanish in 𝒪[K], writing v for the valuation of n, every L in sigma K n has c L ≤ n * v. At an Eisenstein generator ξ (exists_eisenstein_generator) the term of index n - 1 of the derivative of g at ξ, the sum of the terms i * a i * ξ ^ (i - 1), is n * ξ ^ (n - 1), of valuation exactly n * v + (n - 1); by orthogonality of the power basis (le_addVal_sum_iff) no other term can cancel it, so that valuation is at most n * v + n - 1—and it is d L (addVal_derivative_eq_d). This is the elementary form of the classical bound d ≤ n - 1 + n * v on the different of a totally ramified extension ([Serre 1979, Chap. III, §6, Prop. 13][Serre1979]), the tame case v = 0 included, with no case split and no different ideal. Public rather than private: at t = 0 it is also the tame half of c_eq_zero_iff.

theorem MassFormula.eq_and_dvd_of_infinite (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) (h : (sigma K n).Infinite) : ringChar K = ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∧ ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n

The finiteness half of Remark 1°, contrapositively: if sigma K n is infinite, then K has equal characteristic and the residue characteristic divides n ([Serre 1978, Remark 1°, p.1031][Serre1978]).

theorem MassFormula.infinite_of_eq_of_dvd (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) (hchar : ringChar K = ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) (hdvd : ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n) : (sigma K n).Infinite

The infinitude half of Remark 1°: in equal characteristic p with p ∣ n, the set sigma K n is infinite ([Serre 1978, Remark 1°, p.1031][Serre1978]).

theorem MassFormula.sigma_infinite_iff (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) : (sigma K n).Infinite ↔ ringChar K = ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∧ ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n

sigma K n is infinite exactly when K has equal characteristic p and p divides n, assembled from the two halves above ([Serre 1978, Remark 1°, p.1031][Serre1978]).