The tritone is the unique normal involution subgroup of D₁₂

In the T/I group DihedralGroup 12 (r i = Tᵢ, sr j an inversion), the tritone T₆ = r 6 is the unique rotation of order 2, the center is {T₀, T₆}, and this center is the unique normal subgroup of order 2. A single inversion generates an order-2 subgroup that is not normal.

Main results

• orderOf_r_eq_two_iff: T₆ is the unique element of order 2 in the rotation group.
• center_eq_zpowers_r_six, mem_center_iff: Z(D₁₂) = ⟨T₆⟩ = {T₀, T₆}.
• le_center_of_normal_of_card_eq_two: in any group, a normal subgroup of order 2 is central.
• normal_card_two_iff: H is normal of order 2 iff H = Z(D₁₂) (the tritone lemma).
• zpowers_sr_not_normal: ⟨I⟩ has order 2 and is not normal, for every inversion I.

The center computation is Mathlib's DihedralGroup.center_eq_closure_of_even_ne_two.

References

• C. Marín, A tritone-centered self-duality: the set class 6-30 and its order-12 neo-Riemannian dual, Zenodo (2026), doi:10.5281/zenodo.20820961, Lemma 1 (lem:tritone).

theorem MusicTheory.TritoneNormal.orderOf_r_eq_two_iff (k : ZMod 12) : orderOf (DihedralGroup.r k) = 2 ↔ k = 6

T₆ is the unique rotation of order 2 in D₁₂.

theorem MusicTheory.TritoneNormal.center_eq_zpowers_r_six : Subgroup.center (DihedralGroup 12) = Subgroup.zpowers (DihedralGroup.r 6)

The center of D₁₂ is generated by the tritone T₆.

theorem MusicTheory.TritoneNormal.mem_center_iff (g : DihedralGroup 12) : g ∈ Subgroup.center (DihedralGroup 12) ↔ g = 1 ∨ g = DihedralGroup.r 6

The center of D₁₂ is {T₀, T₆}.

theorem MusicTheory.TritoneNormal.card_center : Nat.card ↥(Subgroup.center (DihedralGroup 12)) = 2

The center of D₁₂ has order 2.

theorem MusicTheory.TritoneNormal.le_center_of_normal_of_card_eq_two {G : Type u_1} [Group G] (H : Subgroup G) [hN : H.Normal] (h2 : Nat.card ↥H = 2) : H ≤ Subgroup.center G

In any group, a normal subgroup of order 2 is contained in the center.

theorem MusicTheory.TritoneNormal.normal_card_two_iff (H : Subgroup (DihedralGroup 12)) : H.Normal ∧ Nat.card ↥H = 2 ↔ H = Subgroup.center (DihedralGroup 12)

The tritone lemma. A subgroup of D₁₂ is normal of order 2 iff it is the center {T₀, T₆}.

theorem MusicTheory.TritoneNormal.card_zpowers_sr (j : ZMod 12) : Nat.card ↥(Subgroup.zpowers (DihedralGroup.sr j)) = 2

The subgroup generated by a single inversion has order 2 …

theorem MusicTheory.TritoneNormal.zpowers_sr_not_normal (j : ZMod 12) : ¬(Subgroup.zpowers (DihedralGroup.sr j)).Normal

… but it is not normal.