The order-12 dual of the set class 6-30

The Forte hexachord 6-30 = {0, 1, 3, 6, 7, 9} has a T/I-orbit of 12 sets, no inversional symmetry, and stabilizer {T₀, T₆}. The induced action of DihedralGroup 12 on the orbit has kernel {1, r 6}, and its centralizer in Equiv.Perm of the orbit (the dual group) has order 12. The dual is built as the opposite regular representation, acts simply transitively, and has a dihedral presentation: an element of order 6 inverted by an involution.

Main results

• stab_T, stab_I_empty, not_inversionally_symmetric, orbit_card: the decidable facts.
• Action.Ker_eq, Action.card_TIgrpO: the kernel {1, r 6} and the image of order 12.
• Action.card_Cgrp, Action.Cgrp_transitive: the dual has order 12 and acts transitively.
• Action.dihedral_fingerprint: order 12, orderOf s = 6, t ^ 2 = 1, t * s * t = s⁻¹.

The isomorphism of the dual with DihedralGroup 6 is not constructed.

References

• A. S. Crans, T. M. Fiore, R. Satyendra, Musical actions of dihedral groups, Amer. Math. Monthly 116 (2009) 479–495.
• 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.

def MusicTheory.SixThirty.A : Finset (ZMod 12)

Forte 6-30 = (013679), the Petrushka / octatonic-subset hexachord.

Equations

• MusicTheory.SixThirty.A = {0, 1, 3, 6, 7, 9}

def MusicTheory.SixThirty.tpose (k : ZMod 12) (S : Finset (ZMod 12)) : Finset (ZMod 12)

Transposition of a pc-set: Tₖ A = A + k.

Equations

• MusicTheory.SixThirty.tpose k S = Finset.image (fun (x : ZMod 12) => x + k) S

def MusicTheory.SixThirty.inv (j : ZMod 12) (S : Finset (ZMod 12)) : Finset (ZMod 12)

Inversion of a pc-set: Iⱼ A = j − A.

Equations

• MusicTheory.SixThirty.inv j S = Finset.image (fun (x : ZMod 12) => j - x) S

TIER 1 — decidable facts about 6-30

theorem MusicTheory.SixThirty.stab_T : {k : ZMod 12 | tpose k A = A} = {0, 6}

The transposition stabilizer of 6-30 is exactly the center {T0, T6}.

theorem MusicTheory.SixThirty.stab_I_empty : {j : ZMod 12 | inv j A = A} = ∅

6-30 has no inversional symmetry: no Iⱼ fixes it.

theorem MusicTheory.SixThirty.not_inversionally_symmetric (j : ZMod 12) : inv j A ≠ A

Equivalent statement: A is not inversionally symmetric.

theorem MusicTheory.SixThirty.T6_invariant : tpose 6 A = A

A is T6-invariant (the central transposition symmetry).

def MusicTheory.SixThirty.orbit : Finset (Finset (ZMod 12))

The full T/I-orbit of 6-30 as a finset of pc-sets.

Equations

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

theorem MusicTheory.SixThirty.orbit_card : orbit.card = 12

The T/I-orbit of 6-30 has exactly 12 elements.

TIER 2 — the T/I action on pc-sets, restricted to the orbit, is regular

We make DihedralGroup 12 act on Finset (ZMod 12) by r i ↦ Tᵢ, sr j ↦ I₋ⱼ (the reindex sr j ↦ inv (-j) is forced to make this a genuine left action matching DihedralGroup multiplication). This action restricts to the 12-element orbit O of 6-30; the restricted action is transitive, so by the abstract Wielandt lemma its centralizer in Sym(O) is semiregular, bounding the dual by 12. The 12-element image is itself regular, and an explicit opposite-regular family of 12 commuting permutations witnesses the dual has order exactly 12.

def MusicTheory.SixThirty.Action.smul : DihedralGroup 12 → Finset (ZMod 12) → Finset (ZMod 12)

The T/I action on pitch-class sets.

Equations

• MusicTheory.SixThirty.Action.smul (DihedralGroup.r i) x✝ = MusicTheory.SixThirty.tpose i x✝
• MusicTheory.SixThirty.Action.smul (DihedralGroup.sr j) x✝ = MusicTheory.SixThirty.inv (-j) x✝

@[instance_reducible]

instance MusicTheory.SixThirty.Action.instSMulDihedralGroupOfNatNatFinsetZMod_formalizations : SMul (DihedralGroup 12) (Finset (ZMod 12))

Equations

• MusicTheory.SixThirty.Action.instSMulDihedralGroupOfNatNatFinsetZMod_formalizations = { smul := MusicTheory.SixThirty.Action.smul }

@[simp]

theorem MusicTheory.SixThirty.Action.smul_r (i : ZMod 12) (S : Finset (ZMod 12)) : DihedralGroup.r i • S = tpose i S

@[simp]

theorem MusicTheory.SixThirty.Action.smul_sr (j : ZMod 12) (S : Finset (ZMod 12)) : DihedralGroup.sr j • S = inv (-j) S

@[simp]

theorem MusicTheory.SixThirty.Action.tpose_tpose (i j : ZMod 12) (S : Finset (ZMod 12)) : tpose i (tpose j S) = tpose (i + j) S

@[simp]

theorem MusicTheory.SixThirty.Action.inv_tpose (i j : ZMod 12) (S : Finset (ZMod 12)) : inv i (tpose j S) = inv (i - j) S

@[simp]

theorem MusicTheory.SixThirty.Action.tpose_inv (i j : ZMod 12) (S : Finset (ZMod 12)) : tpose i (inv j S) = inv (j + i) S

@[simp]

theorem MusicTheory.SixThirty.Action.inv_inv (i j : ZMod 12) (S : Finset (ZMod 12)) : inv i (inv j S) = tpose (i - j) S

@[simp]

theorem MusicTheory.SixThirty.Action.tpose_zero (S : Finset (ZMod 12)) : tpose 0 S = S

@[instance_reducible]

instance MusicTheory.SixThirty.Action.instMulActionDihedralGroupOfNatNatFinsetZMod_formalizations : MulAction (DihedralGroup 12) (Finset (ZMod 12))

Equations

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

@[reducible, inline]

abbrev MusicTheory.SixThirty.Action.O : Set (Finset (ZMod 12))

The orbit of 6-30 as a set of pc-sets (the Mathlib MulAction.orbit).

Equations

• MusicTheory.SixThirty.Action.O = MulAction.orbit (DihedralGroup 12) MusicTheory.SixThirty.A

theorem MusicTheory.SixThirty.Action.A_mem_O : A ∈ O

6-30 itself is in its orbit.

theorem MusicTheory.SixThirty.Action.smul_mem_O {B : Finset (ZMod 12)} (hB : B ∈ O) (g : DihedralGroup 12) : g • B ∈ O

g • B stays in O when B ∈ O.

The orbit as a set of cardinality 12

theorem MusicTheory.SixThirty.Action.O_eq_orbit : O = ↑orbit

The Mathlib MulAction.orbit set coincides with the explicit Tier-1 orbit finset.

theorem MusicTheory.SixThirty.Action.card_O : Nat.card ↑O = 12

The induced action on the orbit has 12 elements.

The dual group: centralizer of the induced T/I action on the orbit

The induced action of DihedralGroup 12 on ↥O is transitive (Mathlib's IsPretransitive on orbits). By the abstract Wielandt lemma NeoRiemannian.Duality.centralizing_fixedPoint_eq_one, the centralizer of its image in Sym(O) is semiregular, so it embeds into O and has at most 12 elements. This is the dual group of 6-30.

@[reducible, inline]

abbrev MusicTheory.SixThirty.Action.TIgrpO : Subgroup (Equiv.Perm ↑O)

The image of the T/I group inside Sym(O) — the induced permutation representation.

Equations

• MusicTheory.SixThirty.Action.TIgrpO = (MulAction.toPermHom (DihedralGroup 12) ↑MusicTheory.SixThirty.Action.O).range

@[reducible, inline]

abbrev MusicTheory.SixThirty.Action.Cgrp : Subgroup (Equiv.Perm ↑O)

The dual group: the centralizer of the T/I image in Sym(O).

Equations

• MusicTheory.SixThirty.Action.Cgrp = Subgroup.centralizer ↑MusicTheory.SixThirty.Action.TIgrpO

theorem MusicTheory.SixThirty.Action.Cgrp_comm {σ : Equiv.Perm ↑O} (hσ : σ ∈ Cgrp) (g : DihedralGroup 12) : σ * MulAction.toPerm g = MulAction.toPerm g * σ

A centralizer element commutes with every toPerm g.

def MusicTheory.SixThirty.Action.base : ↑O

The base point of the orbit: 6-30 itself.

Equations

• MusicTheory.SixThirty.Action.base = ⟨MusicTheory.SixThirty.A, MusicTheory.SixThirty.Action.A_mem_O⟩

theorem MusicTheory.SixThirty.Action.eval_injective : Function.Injective fun (c : ↥Cgrp) => ↑c base

Evaluation at base injects the dual group into O (semiregularity, via Wielandt).

theorem MusicTheory.SixThirty.Action.card_Cgrp_le : Nat.card ↥Cgrp ≤ 12

Wielandt bound: the dual group of 6-30 has at most 12 elements.

The kernel of the T/I action on the orbit is the center Z = {1, r 6}

The induced action of DihedralGroup 12 on O is not faithful: T6 (the central transposition, r 6) acts trivially on every orbit element. We show the kernel is exactly {1, r 6} — the center of D₁₂ for n = 6 even — so the induced action factors through D₁₂/Z, which has order 24/2 = 12 = |O| and acts faithfully + transitively, i.e. regularly.

@[reducible, inline]

abbrev MusicTheory.SixThirty.Action.Ker : Subgroup (DihedralGroup 12)

The kernel of the permutation representation on O.

Equations

• MusicTheory.SixThirty.Action.Ker = (MulAction.toPermHom (DihedralGroup 12) ↑MusicTheory.SixThirty.Action.O).ker

theorem MusicTheory.SixThirty.Action.r_smul_A_iff (i : ZMod 12) : DihedralGroup.r i • A = A ↔ i = 0 ∨ i = 6

The stabilizer of A (as a pc-set) under r i is exactly i ∈ {0, 6}.

theorem MusicTheory.SixThirty.Action.sr_smul_A_ne (j : ZMod 12) : DihedralGroup.sr j • A ≠ A

No inversion sr j fixes A.

theorem MusicTheory.SixThirty.Action.r6_central (g : DihedralGroup 12) : DihedralGroup.r 6 * g = g * DihedralGroup.r 6

r 6 is central in DihedralGroup 12: it commutes with everything.

theorem MusicTheory.SixThirty.Action.r6_smul_A : DihedralGroup.r 6 • A = A

r 6 fixes A.

theorem MusicTheory.SixThirty.Action.r6_mem_Ker : DihedralGroup.r 6 ∈ Ker

r 6 acts trivially on the whole orbit (central + fixes A).

theorem MusicTheory.SixThirty.Action.mem_Ker_iff (g : DihedralGroup 12) : g ∈ Ker ↔ g = 1 ∨ g = DihedralGroup.r 6

An element of the kernel fixes A, hence is r 0 or r 6.

theorem MusicTheory.SixThirty.Action.Ker_eq : ↑Ker = {1, DihedralGroup.r 6}

The kernel of the action on O is exactly the center {1, r 6}.

theorem MusicTheory.SixThirty.Action.card_Ker : Nat.card ↥Ker = 2

The kernel has exactly 2 elements (1 ≠ r 6).

Regularity of the induced (quotient) action

The image TIgrpO ≅ D₁₂/Ker has order 24/2 = 12 = |O|, and acts transitively on O. A transitive action of a group whose order equals the size of the set is regular (simply transitive). This is the precise sense in which the T/I action on the 6-30 orbit is the regular representation of D₁₂/Z ≅ D₆.

theorem MusicTheory.SixThirty.Action.card_TIgrpO : Nat.card ↥TIgrpO = 12

The induced T/I image on O has exactly 12 elements (= |D₁₂| / |Ker| = 24/2).

The lower bound |C| ≥ 12 — the opposite regular representation

For each B ∈ O, transitivity gives some h with h • base = B; the choice of h is unique only mod Ker, but since Ker fixes every orbit point, B ↦ h • (g • base) is well-defined. This is the opposite regular representation opp g: it commutes with the whole left T/I action (so lies in Cgrp), and opp g base = g • base, so g ↦ opp g separates the 12 cosets of Ker. Hence the dual has at least 12 elements, and with the Wielandt bound, exactly 12 — it acts regularly.

noncomputable def MusicTheory.SixThirty.Action.carrier (B : ↑O) : DihedralGroup 12

A chosen group element carrying base to B (transitivity witness).

Equations

• MusicTheory.SixThirty.Action.carrier B = ⋯.choose

theorem MusicTheory.SixThirty.Action.carrier_smul (B : ↑O) : carrier B • base = B

theorem MusicTheory.SixThirty.Action.carrier_indep (g : DihedralGroup 12) {h : DihedralGroup 12} {B : ↑O} (hh : h • base = B) : h • g • base = carrier B • g • base

Two carriers of the same point differ by an element of Ker, which fixes g • base; hence the opposite-rep value is independent of the chosen carrier.

noncomputable def MusicTheory.SixThirty.Action.oppFun (g : DihedralGroup 12) (B : ↑O) : ↑O

The opposite-rep underlying function: B ↦ (a carrier of B) • (g • base).

Equations

• MusicTheory.SixThirty.Action.oppFun g B = MusicTheory.SixThirty.Action.carrier B • g • MusicTheory.SixThirty.Action.base

theorem MusicTheory.SixThirty.Action.oppFun_left_inv (g : DihedralGroup 12) (B : ↑O) : oppFun g⁻¹ (oppFun g B) = B

oppFun g⁻¹ is a two-sided inverse of oppFun g.

theorem MusicTheory.SixThirty.Action.oppFun_right_inv (g : DihedralGroup 12) (B : ↑O) : oppFun g (oppFun g⁻¹ B) = B

oppFun g is also a left inverse of oppFun g⁻¹ (the symmetric direction).

noncomputable def MusicTheory.SixThirty.Action.oppPerm (g : DihedralGroup 12) : Equiv.Perm ↑O

The opposite-rep permutation opp g ∈ Sym(O).

Equations

• MusicTheory.SixThirty.Action.oppPerm g = { toFun := MusicTheory.SixThirty.Action.oppFun g, invFun := MusicTheory.SixThirty.Action.oppFun g⁻¹, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MusicTheory.SixThirty.Action.oppPerm_apply (g : DihedralGroup 12) (B : ↑O) : (oppPerm g) B = carrier B • g • base

theorem MusicTheory.SixThirty.Action.oppPerm_base (g : DihedralGroup 12) : (oppPerm g) base = g • base

opp g fixes base ↦ g • base.

theorem MusicTheory.SixThirty.Action.oppPerm_mem_Cgrp (g : DihedralGroup 12) : oppPerm g ∈ Cgrp

Each opp g lies in the dual group Cgrp (commutes with the whole left T/I action).

theorem MusicTheory.SixThirty.Action.oppPerm_carrier_base (B : ↑O) : (oppPerm (carrier B)) base = B

The opposite rep, evaluated at base, recovers the carrier: opp (carrier B) base = B.

theorem MusicTheory.SixThirty.Action.oppInj : Function.Injective fun (B : ↑O) => ⟨oppPerm (carrier B), ⋯⟩

B ↦ opp (carrier B) injects O into the dual group Cgrp (12 distinct elements).

theorem MusicTheory.SixThirty.Action.card_Cgrp_ge : 12 ≤ Nat.card ↥Cgrp

Lower bound: the dual group has at least 12 elements.

theorem MusicTheory.SixThirty.Action.card_Cgrp : Nat.card ↥Cgrp = 12

Tier 2, headline: the dual group of 6-30 has exactly 12 elements.

The dual acts regularly

Cgrp is semiregular (eval_injective) and has 12 elements on a 12-point set; together with transitivity it acts simply transitively (regularly). We record transitivity: every point of O is opp (carrier B) • base, witnessing that Cgrp reaches every orbit element from base.

theorem MusicTheory.SixThirty.Action.Cgrp_transitive (B : ↑O) : ∃ (c : ↥Cgrp), ↑c base = B

The dual group acts transitively on O.

TIER 3 — the dihedral fingerprint of the dual

The opposite representation opp is a group anti-homomorphism D₁₂ → Sym(O) with image Cgrp and kernel Ker = Z, so Cgrp ≅ (D₁₂/Z)ᵒᵖ ≅ D₁₂/Z. Mathlib has no D₁₂/Z ≃* D₆, so we land the dihedral fingerprint that pins Cgrp ≅ D₆ among the five groups of order 12: Cgrp is

• order 12 (Tier 2),
• non-abelian, with
• an element s of order 6 and
• an involution t ≠ 1 that inverts it: t * s * t = s⁻¹ and s * t ≠ t * s.

These four facts identify Cgrp ≅ DihedralGroup 6; the named ≃* is the remaining (Mathlib-gap) step D₁₂/Z ≃* D₆.

theorem MusicTheory.SixThirty.Action.oppPerm_one : oppPerm 1 = 1

opp sends 1 to 1.

theorem MusicTheory.SixThirty.Action.oppPerm_mul (g h : DihedralGroup 12) : oppPerm (g * h) = oppPerm h * oppPerm g

opp is a group anti-homomorphism: opp (g * h) = opp h * opp g.

theorem MusicTheory.SixThirty.Action.oppPerm_pow (g : DihedralGroup 12) (n : ℕ) : oppPerm (g ^ n) = oppPerm g ^ n

Powers go through the anti-hom: opp (g ^ n) = (opp g) ^ n.

noncomputable def MusicTheory.SixThirty.Action.oppC (g : DihedralGroup 12) : ↥Cgrp

The opposite rep as a map into the dual subgroup Cgrp.

Equations

• MusicTheory.SixThirty.Action.oppC g = ⟨MusicTheory.SixThirty.Action.oppPerm g, ⋯⟩

theorem MusicTheory.SixThirty.Action.oppC_mul (g h : DihedralGroup 12) : oppC (g * h) = oppC h * oppC g

oppC is an anti-homomorphism into Cgrp.

theorem MusicTheory.SixThirty.Action.oppC_one : oppC 1 = 1

noncomputable def MusicTheory.SixThirty.Action.s : ↥Cgrp

The chosen order-6 element of the dual: s = opp (r 1).

Equations

• MusicTheory.SixThirty.Action.s = MusicTheory.SixThirty.Action.oppC (DihedralGroup.r 1)

noncomputable def MusicTheory.SixThirty.Action.t : ↥Cgrp

The chosen involution of the dual: t = opp (sr 0).

Equations

• MusicTheory.SixThirty.Action.t = MusicTheory.SixThirty.Action.oppC (DihedralGroup.sr 0)

theorem MusicTheory.SixThirty.Action.s_pow_six : s ^ 6 = 1

s has order 6: s^6 = 1 and s^k ≠ 1 for 0 < k < 6 (checked via opp (r k) base = r k • base which are 6 distinct points).

theorem MusicTheory.SixThirty.Action.s_ne_one : s ≠ 1

s ≠ 1: order strictly bigger than 1 (opp (r 1) base = r 1 • base ≠ base).

theorem MusicTheory.SixThirty.Action.t_sq : t ^ 2 = 1

t is an involution: t^2 = 1.

theorem MusicTheory.SixThirty.Action.t_ne_one : t ≠ 1

t ≠ 1.

theorem MusicTheory.SixThirty.Action.oppC_r_eq_one_iff (k : ZMod 12) : oppC (DihedralGroup.r k) = 1 ↔ k = 0 ∨ k = 6

opp (r k) fixes base iff r k ∈ Ker, i.e. k = 0 or k = 6.

theorem MusicTheory.SixThirty.Action.oppC_pow (g : DihedralGroup 12) (n : ℕ) : oppC (g ^ n) = oppC g ^ n

oppC powers: oppC (g ^ n) = (oppC g) ^ n.

theorem MusicTheory.SixThirty.Action.s_pow (k : ℕ) : s ^ k = oppC (DihedralGroup.r ↑k)

s ^ k = oppC (r k) (since (r 1) ^ k = r k).

theorem MusicTheory.SixThirty.Action.s_pow_eq_one_iff (k : ℕ) : s ^ k = 1 ↔ ↑k = 0 ∨ ↑k = 6

s ^ k = 1 iff k ≡ 0 or k ≡ 6 (mod 12).

theorem MusicTheory.SixThirty.Action.orderOf_s : orderOf s = 6

s has order exactly 6.

theorem MusicTheory.SixThirty.Action.oppC_inv (g : DihedralGroup 12) : oppC g⁻¹ = (oppC g)⁻¹

oppC g⁻¹ = (oppC g)⁻¹ (anti-hom sends inverse to inverse).

theorem MusicTheory.SixThirty.Action.t_mul_s_mul_t : t * s * t = s⁻¹

t inverts s: t * s * t = s⁻¹ (the dihedral reflection relation).

theorem MusicTheory.SixThirty.Action.st_base : ↑(s * t) base = DihedralGroup.sr 1 • base

The two products s * t and t * s, evaluated at base.

theorem MusicTheory.SixThirty.Action.ts_base : ↑(t * s) base = DihedralGroup.sr (-1) • base

theorem MusicTheory.SixThirty.Action.s_t_not_commute : s * t ≠ t * s

Cgrp is non-abelian: s * t ≠ t * s.

theorem MusicTheory.SixThirty.Action.Cgrp_nonabelian : ∃ (a : ↥Cgrp) (b : ↥Cgrp), a * b ≠ b * a

Cgrp is non-abelian.

Tier-3 summary — the dihedral fingerprint of the dual

Bundled: Cgrp has order 12, is non-abelian, contains an element s of order 6 and a non-trivial involution t that inverts it (t s t = s⁻¹). These pin Cgrp ≅ DihedralGroup 6 among the order-12 groups. The named Cgrp ≃* DihedralGroup 6 requires D₁₂/Z ≃* D₆, absent from Mathlib.

theorem MusicTheory.SixThirty.Action.dihedral_fingerprint : Nat.card ↥Cgrp = 12 ∧ orderOf s = 6 ∧ t ^ 2 = 1 ∧ t ≠ 1 ∧ t * s * t = s⁻¹ ∧ s * t ≠ t * s