The dihedral action on the Fourier basis of ℂ[ℤ/N]

With the characters dftChar k j = stdAddChar (j * k), translation acts diagonally (transl a (dftChar k) = stdAddChar (-(a * k)) • dftChar k) and inversion swaps k and -k (inv (dftChar k) = dftChar (-k)). Hence each block k = span {dftChar k, dftChar (-k)} is invariant under the dihedral group generated by translations and inversion, and it is irreducible when k ≠ -k. Mathlib has the transform-level statement ZMod.dft_comp_neg; here the statements are about the characters themselves. The decomposition into the abstract irreducible representations of the dihedral group is not formalized (Mathlib has no classification of them).

Main results

• inv_dftChar, transl_dftChar: the two operators on the characters.
• block_dihedral_invariant, block_irreducible: the blocks are invariant, and irreducible for k ≠ -k.
• selfPaired_eq, selfPaired_iff, selfPaired_odd, selfPaired_even, tritone_selfPaired: the self-paired frequencies ({0, 6} for N = 12; {0, m} for N = 2m).

References

• C. Marín, The Tonnetz spectrum is the generating triad's Fourier balance profile, Zenodo (2026), doi:10.5281/zenodo.20862821.

noncomputable def MusicTheory.InversionDFT.dftChar {N : ℕ} [NeZero N] (k : ZMod N) : ZMod N → ℂ

The k-th DFT character as a vector on ZMod N: dftChar k j = stdAddChar (j * k). (The same characters as CycleGraphSpectrum.dftChar.)

Equations

• MusicTheory.InversionDFT.dftChar k j = ZMod.stdAddChar (j * k)

@[simp]

theorem MusicTheory.InversionDFT.dftChar_apply {N : ℕ} [NeZero N] (k j : ZMod N) : dftChar k j = ZMod.stdAddChar (j * k)

T1 — the two operator actions on the DFT basis.

noncomputable def MusicTheory.InversionDFT.inv {N : ℕ} (Φ : ZMod N → ℂ) : ZMod N → ℂ

Pitch-class INVERSION operator: inv Φ x = Φ (-x) (flip the chromatic circle).

Equations

• MusicTheory.InversionDFT.inv Φ x = Φ (-x)

noncomputable def MusicTheory.InversionDFT.transl {N : ℕ} (a : ZMod N) (Φ : ZMod N → ℂ) : ZMod N → ℂ

TRANSPOSITION operator by a semitones: transl a Φ x = Φ (x - a).

Equations

• MusicTheory.InversionDFT.transl a Φ x = Φ (x - a)

theorem MusicTheory.InversionDFT.inv_dftChar {N : ℕ} [NeZero N] (k : ZMod N) : inv (dftChar k) = dftChar (-k)

Inversion swaps k ↔ -k (T1). inv (dftChar k) = dftChar (-k): inversion permutes the DFT characters by negating the frequency.

theorem MusicTheory.InversionDFT.transl_dftChar {N : ℕ} [NeZero N] (a k : ZMod N) : transl a (dftChar k) = ZMod.stdAddChar (-(a * k)) • dftChar k

Translation is diagonal (T1). transl a (dftChar k) = stdAddChar (-(a*k)) • dftChar k: each DFT character is an eigenvector of every transposition, with eigenvalue the root of unity stdAddChar(-(a·k)).

T2 — the D₁₂-invariant 2-dimensional block.

noncomputable def MusicTheory.InversionDFT.block {N : ℕ} [NeZero N] (k : ZMod N) : Submodule ℂ (ZMod N → ℂ)

The 2-dim block block k = span{dftChar k, dftChar (-k)} — a D₁₂-invariant subspace.

Equations

• MusicTheory.InversionDFT.block k = Submodule.span ℂ {MusicTheory.InversionDFT.dftChar k, MusicTheory.InversionDFT.dftChar (-k)}

theorem MusicTheory.InversionDFT.dftChar_mem_block {N : ℕ} [NeZero N] (k : ZMod N) : dftChar k ∈ block k

Both generators of block k lie in block k (trivially); recorded for the membership proofs.

theorem MusicTheory.InversionDFT.dftChar_neg_mem_block {N : ℕ} [NeZero N] (k : ZMod N) : dftChar (-k) ∈ block k

theorem MusicTheory.InversionDFT.inv_mem_block {N : ℕ} [NeZero N] (k : ZMod N) {Φ : ZMod N → ℂ} (hΦ : Φ ∈ block k) : inv Φ ∈ block k

Inversion preserves the block (T2). inv maps block k into block k: it swaps the two spanning characters (dftChar k ↦ dftChar (-k) and dftChar (-k) ↦ dftChar k, using -(-k) = k), so the whole span is preserved.

theorem MusicTheory.InversionDFT.transl_mem_block {N : ℕ} [NeZero N] (a k : ZMod N) {Φ : ZMod N → ℂ} (hΦ : Φ ∈ block k) : transl a Φ ∈ block k

Translation preserves the block (T2). Every transposition transl a maps block k into block k: each generator goes to a scalar times itself, hence stays in the span.

theorem MusicTheory.InversionDFT.block_dihedral_invariant {N : ℕ} [NeZero N] (k : ZMod N) {Φ : ZMod N → ℂ} (hΦ : Φ ∈ block k) : inv Φ ∈ block k ∧ ∀ (a : ZMod N), transl a Φ ∈ block k

The block is D₁₂-invariant (T2 corollary). block k is closed under inversion AND under every transposition transl a — i.e. under the whole group ⟨T, I⟩ = D₁₂. This is the block-diagonalization of the dihedral action in the DFT basis.

T3 — the pairing counts over ℤ/12.

The self-paired classes {k | k = -k} are exactly {0, 6}: the two 1-dim blocks. The remaining ten classes split into the five pairs {1,11},{2,10},{3,9},{4,8},{5,7}, each a 2-dim block. The dimension bookkeeping 2·1 + 5·2 = 12 = dim ℂ[ℤ₁₂] is recorded as an example.

theorem MusicTheory.InversionDFT.selfPaired_eq : {k : ZMod 12 | k = -k} = {0, 6}

The self-paired classes over ℤ/12 (T3). {k : ZMod 12 | k = -k} = {0, 6}: exactly the two frequencies fixed by inversion, giving the two 1-dimensional blocks. (decide over ZMod 12.)

The self-paired frequencies for every N.

selfPaired_eq and the 2·1 + 5·2 = 12 bookkeeping above are the EVEN instance of a statement true over every ZMod N. The self-paired frequencies {k | k = -k} — the negation fixed points = the 1-dimensional dihedral blocks — and the rest pair into 2-dimensional blocks: • N ODD : self-paired = {0} (1 one-dim block ; (N−1)/2 two-dim blocks), • N EVEN : self-paired = {0, N/2} (2 one-dim blocks; (N−2)/2 two-dim blocks — the extra self-paired frequency is the TRITONE N/2). The count of 1-dim blocks is gcd(2, N). The structural theorems above (block_dihedral_invariant, block_irreducible) hold for arbitrary N. The key lemma is Mathlib's ZMod.neg_eq_self_iff.

theorem MusicTheory.InversionDFT.selfPaired_iff {N : ℕ} (k : ZMod N) : k = -k ↔ k = 0 ∨ 2 * k.val = N

Self-paired ⟺ negation fixed point. k = -k ↔ k = 0 ∨ 2 * k.val = N: a frequency is its own inverse exactly at the DC term, or where 2·k = N (the tritone, available only for even N).

theorem MusicTheory.InversionDFT.selfPaired_odd {N : ℕ} (hodd : Odd N) : {k : ZMod N | k = -k} = {0}

Odd N — one 1-dim block. {k : ZMod N | k = -k} = {0}: for odd N the equation 2·k.val = N is even = odd, impossible, so inversion fixes only the DC frequency.

theorem MusicTheory.InversionDFT.selfPaired_even {N : ℕ} [NeZero N] (m : ℕ) (hm : N = 2 * m) : {k : ZMod N | k = -k} = {0, ↑m}

Even N — two 1-dim blocks, DC and the TRITONE. {k : ZMod N | k = -k} = {0, (m : ZMod N)} where N = 2m: the only nonzero self-paired frequency is the tritone m = N/2. The n=12 case {0, 6} (selfPaired_eq) is m = 6.

theorem MusicTheory.InversionDFT.tritone_selfPaired {N : ℕ} [NeZero N] (m : ℕ) (hm : N = 2 * m) : ↑m = -↑m

**The tritone is self-paired in every even universe ** (m : ZMod N) = -(m : ZMod N) when N = 2m: the tritone N/2 is fixed by inversion in every even ℤ_N. This is the structural reason the tritone keeps recurring.

theorem MusicTheory.InversionDFT.selfPaired_ncard_odd {N : ℕ} (hodd : Odd N) : {k : ZMod N | k = -k}.ncard = 1

One 1-dim block for odd N. gcd(2,N) = 1: inversion has a single fixed frequency.

theorem MusicTheory.InversionDFT.selfPaired_ncard_even {N : ℕ} [NeZero N] (m : ℕ) (hm : N = 2 * m) : {k : ZMod N | k = -k}.ncard = 2

Two 1-dim blocks for even N. gcd(2,N) = 2: inversion fixes exactly the DC term and the tritone.

The conjugate pair {k, −k}

The orbit conjPair k = {k, −k} of k under negation indexes the dihedral blocks: block k is the span of dftChar '' conjPair k (block_eq_span_conjPair), of dimension (conjPair k).ncard ∈ {1, 2}; it is a singleton exactly at the self-paired frequencies (conjPair_ncard_*), which for even N are 0 and the tritone N/2 (tritone_selfPaired).

def MusicTheory.InversionDFT.conjPair {N : ℕ} (k : ZMod N) : Set (ZMod N)

The conjugate pair / negation orbit conjPair k = {k, −k}, the index of the dihedral blocks.

Equations

• MusicTheory.InversionDFT.conjPair k = {k, -k}

@[simp]

theorem MusicTheory.InversionDFT.mem_conjPair {N : ℕ} {k j : ZMod N} : j ∈ conjPair k ↔ j = k ∨ j = -k

theorem MusicTheory.InversionDFT.conjPair_neg {N : ℕ} (k : ZMod N) : conjPair (-k) = conjPair k

The pair is well defined on the negation quotient. conjPair (-k) = conjPair k: the two ends of a conjugate pair name the same object — conjPair factors through k ~ -k.

theorem MusicTheory.InversionDFT.block_eq_span_conjPair {N : ℕ} [NeZero N] (k : ZMod N) : block k = Submodule.span ℂ (dftChar '' conjPair k)

The block is the span of the conjugate pair. block k = span ℂ (dftChar '' conjPair k): the dihedral block is literally the span of the two characters indexed by the conjugate pair. So conjPair k IS the block index.

theorem MusicTheory.InversionDFT.conjPair_ncard_of_selfPaired {N : ℕ} {k : ZMod N} (h : k = -k) : (conjPair k).ncard = 1

Self-paired ⟹ the block is 1-dimensional. When k = -k the conjugate pair collapses to a singleton, (conjPair k).ncard = 1: the two fixed frequencies {0, N/2} are the 1-dim blocks.

theorem MusicTheory.InversionDFT.conjPair_ncard_of_not {N : ℕ} {k : ZMod N} (h : k ≠ -k) : (conjPair k).ncard = 2

Not self-paired ⟹ the block is 2-dimensional. When k ≠ -k the conjugate pair has two elements, (conjPair k).ncard = 2: the genuine 2-dim irreducible blocks.

theorem MusicTheory.InversionDFT.conjPair_tritone_ncard {N : ℕ} [NeZero N] (m : ℕ) (hm : N = 2 * m) : (conjPair ↑m).ncard = 1

The tritone pair is a singleton in every even universe. conjPair (N/2) collapses to {N/2} for N = 2m: the tritone is its own conjugate, so its block is 1-dimensional.

Irreducibility of the 2-dim blocks (eigenvalue separation).

For k ≠ -k the block block k is an IRREDUCIBLE ⟨T, I⟩ = D₁₂ representation: it has no proper nonzero subspace invariant under both inv and all transl a. The mechanism is eigenvalue separation — at a = 1 the two transl 1 eigenvalues stdAddChar(-k) and stdAddChar k are DISTINCT iff k ≠ -k, so the only transl-invariant lines are the two coordinate axes, which inv swaps. Standard 2-dim-dihedral-irrep representation theory; here for this concrete DFT block.

T-next-1 — eigenvalue apartness.

theorem MusicTheory.InversionDFT.dftChar_apart {N : ℕ} [NeZero N] {k : ZMod N} (hk : k ≠ -k) : ZMod.stdAddChar k ≠ ZMod.stdAddChar (-k)

Eigenvalue apartness (T-next-1). For k ≠ -k the two transl 1 eigenvalues are distinct: stdAddChar k ≠ stdAddChar (-k). Immediate from injectivity of the standard additive character (ZMod.injective_stdAddChar).

theorem MusicTheory.InversionDFT.not_selfPaired {k : ZMod 12} (hk : k ∉ {0, 6}) : k ≠ -k

The non-self-paired ℤ/12 frequencies (T-next-1, ZMod face). Over ℤ/12, k ∉ {0,6} is exactly the apartness hypothesis k ≠ -k (contrapositive of selfPaired_eq).

T-next-2 — pair independence + operator linearity.

theorem MusicTheory.InversionDFT.transl_add {N : ℕ} (a : ZMod N) (Φ Ψ : ZMod N → ℂ) : transl a (Φ + Ψ) = transl a Φ + transl a Ψ

transl a is additive.

theorem MusicTheory.InversionDFT.transl_smul {N : ℕ} (a : ZMod N) (c : ℂ) (Φ : ZMod N → ℂ) : transl a (c • Φ) = c • transl a Φ

transl a is ℂ-homogeneous.

theorem MusicTheory.InversionDFT.inv_add {N : ℕ} (Φ Ψ : ZMod N → ℂ) : inv (Φ + Ψ) = inv Φ + inv Ψ

inv is additive.

theorem MusicTheory.InversionDFT.inv_smul {N : ℕ} (c : ℂ) (Φ : ZMod N → ℂ) : inv (c • Φ) = c • inv Φ

inv is ℂ-homogeneous.

@[simp]

theorem MusicTheory.InversionDFT.dftChar_zero {N : ℕ} [NeZero N] (k : ZMod N) : dftChar k 0 = 1

dftChar k 0 = 1.

@[simp]

theorem MusicTheory.InversionDFT.dftChar_one {N : ℕ} [NeZero N] (k : ZMod N) : dftChar k 1 = ZMod.stdAddChar k

dftChar k 1 = stdAddChar k.

theorem MusicTheory.InversionDFT.dftChar_pair_indep {N : ℕ} [NeZero N] {k : ZMod N} (hk : k ≠ -k) (c d : ℂ) (h : c • dftChar k + d • dftChar (-k) = 0) : c = 0 ∧ d = 0

Pair independence (T-next-2). For k ≠ -k the two DFT characters dftChar k, dftChar (-k) are ℂ-linearly independent: a vanishing combination c • dftChar k + d • dftChar (-k) = 0 forces c = d = 0. Proof: evaluate at x = 0 (gives c + d = 0) and at x = 1 (gives c·stdAddChar k + d·stdAddChar(-k) = 0); the 2×2 system has determinant stdAddChar(-k) − stdAddChar k ≠ 0 by dftChar_apart.

T-next-3 — concrete irreducibility (eigenvalue separation).

theorem MusicTheory.InversionDFT.eigen_sep {N : ℕ} [NeZero N] (k : ZMod N) (c d : ℂ) : transl 1 (c • dftChar k + d • dftChar (-k)) - ZMod.stdAddChar k • (c • dftChar k + d • dftChar (-k)) = (c * (ZMod.stdAddChar (-k) - ZMod.stdAddChar k)) • dftChar k

Helper: the eigenvalue-separation vector. For w₀ = c • dftChar k + d • dftChar (-k), transl 1 w₀ - stdAddChar k • w₀ = (c * (stdAddChar (-k) - stdAddChar k)) • dftChar k. The dftChar (-k) component cancels because transl 1 acts on it by stdAddChar k — the same scalar we subtract. This is the algebra that isolates the k-eigenvector.

theorem MusicTheory.InversionDFT.block_irreducible {N : ℕ} [NeZero N] {k : ZMod N} (hk : k ≠ -k) (W : Submodule ℂ (ZMod N → ℂ)) (hWle : W ≤ block k) (hinv : ∀ w ∈ W, inv w ∈ W) (htransl : ∀ (a : ZMod N), ∀ w ∈ W, transl a w ∈ W) : W = ⊥ ∨ W = block k

Concrete irreducibility of the 2-dim block (T-next-3, THE PRIZE). For k ≠ -k, any subspace W ≤ block k invariant under inversion inv and all transpositions transl a is either ⊥ or all of block k. So block k is an IRREDUCIBLE ⟨T, I⟩ = D₁₂ representation. The proof is eigenvalue separation: a nonzero w₀ ∈ W, written c • dftChar k + d • dftChar (-k), yields via eigen_sep the vector u = c·(stdAddChar(-k) − stdAddChar k) • dftChar k ∈ W; when c ≠ 0 the scalar is nonzero (apartness) so dftChar k ∈ W, when c = 0 then dftChar (-k) ∈ W directly; inv supplies the partner, hence block k ≤ W, and le_antisymm finishes.

Not formalized

The packaging of block k as a simple module over MonoidAlgebra ℂ (DihedralGroup 6), its isomorphism with an abstract irreducible representation, and the isotypic decomposition ℂ[ℤ₁₂] = ⊕ block need a classification of the irreducible representations of the dihedral group, which Mathlib does not have.

Other equal temperaments — the block census for arbitrary N-TET, for free.

Every theorem above is generic over `{N : ℕ} [NeZero N]`, so the dihedral block decomposition holds
in ANY equal temperament, instantiated with no extra proof. For the famous microtonal systems 19-, 31-,
53-TET (all odd) the ONLY self-paired frequency is the DC term — there is NO tritone, and `gcd(2,N)=1`
gives a single 1-dimensional block, the remaining `(N-1)/2` frequencies pairing into 2-dimensional
irreducible blocks (`block_irreducible`, generic in N). For an even temperament such as 24-TET (quarter
tones) the tritone reappears at `N/2 = 12`, giving two 1-dim blocks. The proof assistant supplies each
instance by feeding `N` to the same generic theorem — no per-system work.