A double-cover polynomial with an odd root multiplicity is irreducible. Applied to the norm-polynomial factorization, this detects the even-index subfield exceptions.

theorem CCDN.signedNormCurvePolynomial_absolute_irreducible_of_odd_subfield_index (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) {ε : ℤ} (hε : ε ≠ 0) (hindex : Odd (Module.finrank (↥ℚ⟮↑β⟯) K)) : AbsolutelyIrreducible (signedNormCurvePolynomial K β ε)

Odd multiplicity of the generated subfield suffices, even when the ambient number-field degree itself is even.