The neo-Riemannian PLR group and the T/I group on the 24 triads

The 24 major and minor triads Triad = ZMod 12 × Bool carry the transposition/inversion action of DihedralGroup 12, which is simply transitive. The neo-Riemannian involutions P, L, R commute with it, and the group they generate is the full centralizer of the T/I action in Equiv.Perm Triad: the two groups are dual in the sense of Crans, Fiore and Satyendra. The key step is that in a faithful transitive action a centralizing permutation with a fixed point is the identity, so the centralizer has at most 24 elements.

Main results

• Duality.centralizing_fixedPoint_eq_one: a permutation commuting with a transitive action and fixing a point is the identity.
• Duality.card_TIgrp, Duality.card_PLRgrp: both groups have order 24.
• Duality.centralizer_eq_PLR: the centralizer of the T/I group is the PLR group.
• VoiceLeading.P_size_one, L_size_one, R_size_two, P_holds_two: voice-leading sizes and common tones of P, L, R.

References

• A. S. Crans, T. M. Fiore, R. Satyendra, Musical actions of dihedral groups, Amer. Math. Monthly 116 (2009) 479–495.
• L. Aniva, C. Wang, Prismriver: formalization of music theory and algorithmic composition in Lean 4, arXiv:2606.19936.
• 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.

@[reducible, inline]

abbrev MusicTheory.Triad : Type

A triad is a root pitch-class in ZMod 12 with a quality bit (true = major, false = minor). There are exactly 24.

Equations

• MusicTheory.Triad = (ZMod 12 × Bool)

@[reducible, inline]

abbrev MusicTheory.Triad.root (t : Triad) : ZMod 12

The root pitch class.

Equations

• t.root = t.1

@[reducible, inline]

abbrev MusicTheory.Triad.isMajor (t : Triad) : Bool

Quality: true = major, false = minor.

Equations

• t.isMajor = t.2

def MusicTheory.Triad.pcs (t : Triad) : Finset (ZMod 12)

Pitch-class content: major root r = {r, r+4, r+7}; minor root r = {r, r+3, r+7}.

Equations

• t.pcs = if t.2 = true then {t.1, t.1 + 4, t.1 + 7} else {t.1, t.1 + 3, t.1 + 7}

The T/I (transposition/inversion) action of D₁₂

r i acts as transposition up by i; sr j acts as an inversion (flips quality, root ↦ −x−j−7). The constants are forced by the pitch-class content; the reindex makes this a genuine left action matching Mathlib's DihedralGroup multiplication.

def MusicTheory.TI.smul : DihedralGroup 12 → Triad → Triad

The T/I action on triads.

Equations

• MusicTheory.TI.smul (DihedralGroup.r i) (x_2, b) = (x_2 + i, b)
• MusicTheory.TI.smul (DihedralGroup.sr j) (x_2, b) = (-x_2 - j - 7, !b)

@[instance_reducible]

instance MusicTheory.TI.instSMulDihedralGroupOfNatNatTriad : SMul (DihedralGroup 12) Triad

Equations

• MusicTheory.TI.instSMulDihedralGroupOfNatNatTriad = { smul := MusicTheory.TI.smul }

@[simp]

theorem MusicTheory.TI.smul_r (i x : ZMod 12) (b : Bool) : DihedralGroup.r i • (x, b) = (x + i, b)

@[simp]

theorem MusicTheory.TI.smul_sr (j x : ZMod 12) (b : Bool) : DihedralGroup.sr j • (x, b) = (-x - j - 7, !b)

@[instance_reducible]

instance MusicTheory.TI.instMulActionDihedralGroupOfNatNatTriad : MulAction (DihedralGroup 12) Triad

Equations

• MusicTheory.TI.instMulActionDihedralGroupOfNatNatTriad = { toSMul := MusicTheory.TI.instSMulDihedralGroupOfNatNatTriad, mul_smul := ⋯, one_smul := ⋯ }

instance MusicTheory.TI.instIsPretransitiveDihedralGroupOfNatNatTriad : MulAction.IsPretransitive (DihedralGroup 12) Triad

The T/I action is transitive: any triad maps to any other.

The neo-Riemannian operations P, L, R

P (parallel): same root, flip quality. L (leading-tone exchange). R (relative). Each is an involution. The crux of the duality is proved here at generator level: every one of P, L, R commutes with the entire T/I action — i.e. P, L, R lie in the centralizer of the T/I group inside Equiv.Perm Triad.

def MusicTheory.PLR.Pf : Triad → Triad

Parallel: C major ↔ C minor.

Equations

• MusicTheory.PLR.Pf (x_1, b) = (x_1, !b)

def MusicTheory.PLR.Lf : Triad → Triad

Leading-tone exchange: C major ↔ E minor.

Equations

• MusicTheory.PLR.Lf (x_1, true) = (x_1 + 4, false)
• MusicTheory.PLR.Lf (x_1, false) = (x_1 - 4, true)

def MusicTheory.PLR.Rf : Triad → Triad

Relative: C major ↔ A minor.

Equations

• MusicTheory.PLR.Rf (x_1, true) = (x_1 - 3, false)
• MusicTheory.PLR.Rf (x_1, false) = (x_1 + 3, true)

theorem MusicTheory.PLR.Pf_invol : Function.Involutive Pf

theorem MusicTheory.PLR.Lf_invol : Function.Involutive Lf

theorem MusicTheory.PLR.Rf_invol : Function.Involutive Rf

def MusicTheory.PLR.P : Equiv.Perm Triad

The three operations as elements of Equiv.Perm Triad (involutions are their own inverse).

Equations

• MusicTheory.PLR.P = Function.Involutive.toPerm MusicTheory.PLR.Pf MusicTheory.PLR.Pf_invol

def MusicTheory.PLR.L : Equiv.Perm Triad

Equations

• MusicTheory.PLR.L = Function.Involutive.toPerm MusicTheory.PLR.Lf MusicTheory.PLR.Lf_invol

def MusicTheory.PLR.R : Equiv.Perm Triad

Equations

• MusicTheory.PLR.R = Function.Involutive.toPerm MusicTheory.PLR.Rf MusicTheory.PLR.Rf_invol

The duality crux: P, L, R each commute with the whole T/I action.

theorem MusicTheory.PLR.Pf_comm (g : DihedralGroup 12) (t : Triad) : Pf (g • t) = g • Pf t

theorem MusicTheory.PLR.Lf_comm (g : DihedralGroup 12) (t : Triad) : Lf (g • t) = g • Lf t

theorem MusicTheory.PLR.Rf_comm (g : DihedralGroup 12) (t : Triad) : Rf (g • t) = g • Rf t

The duality engine (centralizer of the regular T/I rep)

The headline. Two layers:

• Abstract. For any faithful transitive MulAction G α, the centralizer of the image of G in Equiv.Perm α is semiregular: a centralizing permutation with a fixed point is the identity (centralizing_fixedPoint_eq_one). Consequently, evaluation at any base point embeds the centralizer into α, so |centralizer| ≤ |α| (card_Cgrp_le for the triads). This is the regular-action case of Wielandt's theorem on centralizers of transitive permutation groups, which we did not find in Mathlib.

• Concrete (CFS duality). The T/I action is faithful (decide-level) and transitive, so it is the left regular representation on the 24 triads. The neo-Riemannian P, L, R all lie in its centralizer (the _comm lemmas, repackaged as Subgroup.closure {P,L,R} ≤ centralizer), and the centralizer has at most 24 elements. PLR is thus exactly the centralizer iff |⟨P,L,R⟩| = 24, proved below.

instance MusicTheory.instFaithfulSMulDihedralGroupOfNatNatTriad : FaithfulSMul (DihedralGroup 12) Triad

The T/I action is faithful (two test triads pin down the dihedral element).

theorem MusicTheory.Duality.centralizing_fixedPoint_eq_one {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [MulAction.IsPretransitive G α] (σ : Equiv.Perm α) (hcomm : ∀ (g : G), σ * MulAction.toPerm g = MulAction.toPerm g * σ) (a : α) (hfix : σ a = a) : σ = 1

Wielandt, regular case (abstract, reusable). In a faithful transitive G-action, any permutation σ commuting with the whole image of G and fixing one point is the identity — the centralizer of a transitive group is semiregular.

@[reducible, inline]

abbrev MusicTheory.Duality.TIgrp : Subgroup (Equiv.Perm Triad)

The image of the T/I group inside Equiv.Perm Triad — the left regular representation.

Equations

• MusicTheory.Duality.TIgrp = (MulAction.toPermHom (DihedralGroup 12) MusicTheory.Triad).range

@[reducible, inline]

abbrev MusicTheory.Duality.Cgrp : Subgroup (Equiv.Perm Triad)

Its centralizer in Sym(Triad) — the object we identify with PLR.

Equations

• MusicTheory.Duality.Cgrp = Subgroup.centralizer ↑MusicTheory.Duality.TIgrp

theorem MusicTheory.Duality.Cgrp_comm {σ : Equiv.Perm Triad} (hσ : σ ∈ Cgrp) (g : DihedralGroup 12) : σ * MulAction.toPerm g = MulAction.toPerm g * σ

A centralizer element commutes with every toPerm g.

theorem MusicTheory.Duality.eval_injective : Function.Injective fun (c : ↥Cgrp) => ↑c (0, true)

Evaluation at the base triad (0, true) injects the centralizer into Triad (semiregularity).

theorem MusicTheory.Duality.card_Cgrp_le : Nat.card ↥Cgrp ≤ 24

Wielandt bound (concrete): the centralizer of the T/I image has at most 24 elements.

theorem MusicTheory.Duality.mem_Cgrp_of_comm (σ : Equiv.Perm Triad) (h : ∀ (g : DihedralGroup 12) (t : Triad), σ (g • t) = g • σ t) : σ ∈ Cgrp

A neo-Riemannian generator (as a permutation) commuting with the whole T/I image, packaged from a pointwise commuting law f (g • t) = g • f t.

theorem MusicTheory.Duality.PLR_le_centralizer : Subgroup.closure {PLR.P, PLR.L, PLR.R} ≤ Cgrp

PLR centralizes T/I. The neo-Riemannian group sits inside the centralizer of the regular T/I representation — the substantive direction of the CFS duality.

theorem MusicTheory.Duality.card_TIgrp : Nat.card ↥TIgrp = 24

The Cayley identification: T/I ≅ its image, of order 24 (left regular rep is faithful).

Cgrp = ⟨P, L, R⟩

The remaining numeric obligation |⟨P,L,R⟩| = 24 is discharged by orbit–stabilizer: the PLR subgroup acts on the 24 triads transitively (P, L, R already reach everything: L∘R is the root-translation by −7, a generator of ℤ/12, and P flips quality) and semiregularly (it lies in the semiregular centralizer Cgrp). A transitive + semiregular action is regular, so |⟨P,L,R⟩| = |Triad| = 24. Then ⟨P,L,R⟩ ≤ Cgrp, |Cgrp| ≤ 24 = |⟨P,L,R⟩| force equality.

@[reducible, inline]

abbrev MusicTheory.Duality.PLRgrp : Subgroup (Equiv.Perm Triad)

Abbreviation for the neo-Riemannian subgroup of Sym(Triad).

Equations

• MusicTheory.Duality.PLRgrp = Subgroup.closure {MusicTheory.PLR.P, MusicTheory.PLR.L, MusicTheory.PLR.R}

theorem MusicTheory.Duality.P_mem : PLR.P ∈ PLRgrp

The generators belong to PLRgrp.

theorem MusicTheory.Duality.L_mem : PLR.L ∈ PLRgrp

theorem MusicTheory.Duality.R_mem : PLR.R ∈ PLRgrp

theorem MusicTheory.Duality.LR_smul_major (x : ZMod 12) : (PLR.L * PLR.R) (x, true) = (x - 7, true)

L ∘ R translates a major triad's root by −7; iterating reaches every major triad.

def MusicTheory.Duality.wk (k : ℕ) : ↥PLRgrp

The subgroup element (L*R)^k, packaged in PLRgrp.

Equations

• MusicTheory.Duality.wk k = ⟨(MusicTheory.PLR.L * MusicTheory.PLR.R) ^ k, ⋯⟩

theorem MusicTheory.Duality.wk_smul (k : ℕ) : wk k • (0, true) = (-(7 * ↑k), true)

Acting by (L*R)^k on the base major triad lands on root −7k.

theorem MusicTheory.Duality.reach_major (m : ZMod 12) : ∃ (g : ↥PLRgrp), g • (0, true) = (m, true)

Every major triad is reached from the base by some (L*R)^k.

theorem MusicTheory.Duality.reach_minor (m : ZMod 12) : ∃ (g : ↥PLRgrp), g • (0, true) = (m, false)

Every minor triad is reached from the base (apply P after a major reach).

instance MusicTheory.Duality.instIsPretransitiveSubtypePermTriadMemSubgroupPLRgrp : MulAction.IsPretransitive (↥PLRgrp) Triad

The PLR action on the 24 triads is transitive.

theorem MusicTheory.Duality.PLRgrp_stabilizer_eq_bot : MulAction.stabilizer ↥PLRgrp (0, true) = ⊥

The PLR action is semiregular: the stabilizer of any triad is trivial (it sits inside the semiregular centralizer Cgrp).

theorem MusicTheory.Duality.card_PLRgrp : Nat.card ↥PLRgrp = 24

The numeric crux: the neo-Riemannian group has exactly 24 elements (regular action).

theorem MusicTheory.Duality.centralizer_eq_PLR : Cgrp = PLRgrp

Headline: the centralizer of the regular T/I representation is exactly the neo-Riemannian PLR group — the Crans–Fiore–Satyendra duality, deductively closed.

M.3 — P, L, R as minimal voice-leadings (Cohn, JMT 41 (1997))

The neo-Riemannian moves are the parsimonious triad-to-triad voice-leadings: each holds two common tones and shifts the remaining voice by a single step. The precise sizes (in the L¹ voice-leading metric, distances mod 12) are P = 1, L = 1, R = 2 — NOT all equal: R moves its voice by a whole tone. We verify both facts as finite checks over all 24 triads, decoupled from the orbifold (G.1/M.2).

A voice-leading is a bijection between the two triads' three voices; its size is the sum of the (circular) semitone displacements; vlDist is the minimum over all 6 bijections.

def MusicTheory.VoiceLeading.cdist (a b : ZMod 12) : ℕ

Circular semitone distance on the pitch-class circle: min(d, 12−d).

Equations

• MusicTheory.VoiceLeading.cdist a b = min (a - b).val (b - a).val

def MusicTheory.VoiceLeading.voices (t : Triad) : Fin 3 → ZMod 12

The three voices of a triad in order (root, third, fifth).

Equations

• MusicTheory.VoiceLeading.voices t = if t.2 = true then ![t.1, t.1 + 4, t.1 + 7] else ![t.1, t.1 + 3, t.1 + 7]

def MusicTheory.VoiceLeading.perms3 : List (Fin 3 → Fin 3)

The six bijections of three voices.

Equations

• MusicTheory.VoiceLeading.perms3 = [![0, 1, 2], ![0, 2, 1], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1], ![2, 1, 0]]

def MusicTheory.VoiceLeading.cost (t u : Triad) (σ : Fin 3 → Fin 3) : ℕ

The size of the voice-leading t → u that matches voice i of t to voice σ i of u.

Equations

• One or more equations did not get rendered due to their size.

def MusicTheory.VoiceLeading.vlDist (t u : Triad) : ℕ

The voice-leading distance: minimal size over all bijective matchings of the voices.

Equations

• MusicTheory.VoiceLeading.vlDist t u = List.foldr min 100 (List.map (MusicTheory.VoiceLeading.cost t u) MusicTheory.VoiceLeading.perms3)

theorem MusicTheory.VoiceLeading.P_size_one (t : Triad) : vlDist t (PLR.Pf t) = 1

P is a single-semitone voice-leading (size 1), for every triad.

theorem MusicTheory.VoiceLeading.L_size_one (t : Triad) : vlDist t (PLR.Lf t) = 1

L is a single-semitone voice-leading (size 1), for every triad.

theorem MusicTheory.VoiceLeading.R_size_two (t : Triad) : vlDist t (PLR.Rf t) = 2

R is a whole-tone voice-leading (size 2 — NOT 1), for every triad: the honest correction to "P, L, R are all minimal/equal".

theorem MusicTheory.VoiceLeading.P_holds_two (t : Triad) : (t.pcs ∩ (PLR.Pf t).pcs).card = 2

Each of P, L, R retains exactly two common tones (the parsimony that makes them minimal).

theorem MusicTheory.VoiceLeading.L_holds_two (t : Triad) : (t.pcs ∩ (PLR.Lf t).pcs).card = 2

theorem MusicTheory.VoiceLeading.R_holds_two (t : Triad) : (t.pcs ∩ (PLR.Rf t).pcs).card = 2