Circulant matrices are diagonalized by the discrete Fourier transform

For v : ZMod N → ℂ, Mathlib's Matrix.circulant v satisfies circulant v *ᵥ dftChar k = ZMod.dft v k • dftChar k, where dftChar k j = stdAddChar (j * k). The characters form a basis (N times the inverse transform of the standard basis), so every circulant is diagonal in it. For the cycle graph C₁₂ this gives the spectrum 2 cos (2πk / 12); for a Cayley graph of ℤ/N the eigenvalue is a character sum.

Main results

• circulant_mulVec_dftChar: every circulant has the characters as eigenvectors, with eigenvalue the transform of its first column.
• dftChar_linearIndependent, dftChar_basis: the characters form a basis of ZMod N → ℂ.
• C12_eq_adjMatrix, C12_eigenvalue_cos: the adjacency matrix of SimpleGraph.cycleGraph 12 and its eigenvalues 2 cos (2πk / 12).
• cayleyAdj_eigenvalue, cayleyAdj_eq_adjMatrix: the spectrum of a Cayley graph of ℤ/N.

References

• C. Godsil, G. Royle, Algebraic Graph Theory, Springer (2001).
• L. Babai, Spectra of Cayley graphs, J. Combin. Theory Ser. B 27 (1979).
• C. Marín, The Tonnetz spectrum is the generating triad's Fourier balance profile, Zenodo (2026), doi:10.5281/zenodo.20862821.

T1 — circulants are diagonalized by the DFT characters.

noncomputable def MusicTheory.CycleGraphSpectrum.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) = exp(2πi·jk/N). These are the simultaneous eigenvectors of every circulant operator.

Equations

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

@[simp]

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

theorem MusicTheory.CycleGraphSpectrum.dftChar_ne_zero {N : ℕ} [NeZero N] (k : ZMod N) : dftChar k ≠ 0

The DFT character is nowhere the zero vector: its value at 0 is stdAddChar 0 = 1 ≠ 0.

theorem MusicTheory.CycleGraphSpectrum.circulant_mulVec_dftChar {N : ℕ} [NeZero N] (v : ZMod N → ℂ) (k : ZMod N) : (Matrix.circulant v).mulVec (dftChar k) = ZMod.dft v k • dftChar k

THE DIAGONALIZATION (T1). Every circulant matrix is diagonalized by the DFT characters: circulant v sends the k-th character dftChar k to (dft v k) • dftChar k. The eigenvalue is exactly the k-th discrete Fourier coefficient of the generating vector v.

T2 — the DFT characters are a BASIS: the simultaneous eigenbasis of all circulants.

The 12 characters dftChar k are linearly independent, hence (card = dim = N) a basis of ZMod N → ℂ. This is the classical "characters of a finite abelian group are independent", here in the concrete stdAddChar form. Combined with T1 (circulant_mulVec_dftChar), it makes the DFT the literal diagonalizing eigenbasis of every circulant — in particular of C12.

The load-bearing observation: each dftChar k is N times the inverse-DFT image of the standard basis vector Pi.single k 1. Since Pi.single · 1 is independent (Pi.linearIndependent_single_one), the injective linear equiv 𝓕⁻ = dft.symm preserves independence (LinearIndependent.map'), and scaling by the nonzero constant (N : ℂ) preserves it again (LinearIndependent.units_smul).

theorem MusicTheory.CycleGraphSpectrum.dftChar_eq_smul_invDFT {N : ℕ} [NeZero N] (k : ZMod N) : dftChar k = ↑N • ZMod.dft.symm (Pi.single k 1)

The bridge to the standard basis. The k-th DFT character is N times the inverse-DFT of the standard basis vector Pi.single k 1: dftChar k = (N : ℂ) • 𝓕⁻ (Pi.single k 1). The inverse-DFT of a delta is (up to the N⁻¹ normalization) exactly a character.

theorem MusicTheory.CycleGraphSpectrum.linearIndependent_single_one_map (M' : Type u_1) [AddCommGroup M'] [Module ℂ M'] (n : ℕ) (f : (ZMod n → ℂ) →ₗ[ℂ] M') (hf : Function.Injective ⇑f) : LinearIndependent ℂ fun (k : ZMod n) => f (Pi.single k 1)

Sealed helper. An injective linear map out of ZMod N → ℂ carries the standard basis (Pi.single k 1)_k to a linearly independent family. Stated generically (f opaque) so the elaborator/kernel never unfolds the heavy dft structure — the direct inline map' over ZMod.dft.symm provokes a whnf/isDefEq blow-up; this generic version sidesteps it.

theorem MusicTheory.CycleGraphSpectrum.dftChar_linearIndependent {N : ℕ} [NeZero N] : LinearIndependent ℂ fun (k : ZMod N) => dftChar k

THE EIGENBASIS — LINEAR INDEPENDENCE (T2, load-bearing). The DFT characters (dftChar k)_{k ∈ ZMod N} are linearly independent over ℂ. (Characters of the finite abelian group ZMod N, in stdAddChar form.) Pushed through 𝓕⁻ from the standard basis and scaled.

noncomputable def MusicTheory.CycleGraphSpectrum.dftChar_basis {N : ℕ} [NeZero N] : Module.Basis (ZMod N) ℂ (ZMod N → ℂ)

THE EIGENBASIS — AS A BASIS (T2). The DFT characters form a basis of ZMod N → ℂ (linear independence + card = dim). This is the simultaneous eigenbasis diagonalizing every circulant operator on ZMod N.

Equations

• MusicTheory.CycleGraphSpectrum.dftChar_basis = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

@[simp]

theorem MusicTheory.CycleGraphSpectrum.dftChar_basis_apply {N : ℕ} [NeZero N] (k : ZMod N) : dftChar_basis k = dftChar k

T3 — the pitch-class cycle graph C₁₂ and its spectrum.

The chromatic circle: vertex m ∈ ℤ/12 joined to m ± 1 (its semitone neighbours). The adjacency operator is C12 = circulant cycAdj where cycAdj is the ±1 semitone indicator. By T1 its eigenvalues are dft cycAdj k, which we compute to the textbook 2·cos(2πk/12).

noncomputable def MusicTheory.CycleGraphSpectrum.cycAdj : ZMod 12 → ℂ

The ±1 semitone-neighbour indicator on ℤ/12: cycAdj m = 1 iff m = 1 ∨ m = -1, else 0. This is the first column of the C₁₂ adjacency matrix.

Equations

• MusicTheory.CycleGraphSpectrum.cycAdj m = if m = 1 ∨ m = -1 then 1 else 0

noncomputable def MusicTheory.CycleGraphSpectrum.C12 : Matrix (ZMod 12) (ZMod 12) ℂ

The adjacency operator of the pitch-class cycle graph C₁₂, as a circulant matrix over ℂ.

Equations

• MusicTheory.CycleGraphSpectrum.C12 = Matrix.circulant MusicTheory.CycleGraphSpectrum.cycAdj

theorem MusicTheory.CycleGraphSpectrum.C12_mulVec_dftChar (k : ZMod 12) : C12.mulVec (dftChar k) = ZMod.dft cycAdj k • dftChar k

C₁₂ is diagonalized by the DFT characters: eigenvector dftChar k, eigenvalue dft cycAdj k. (Direct specialization of the general T1 diagonalization.)

theorem MusicTheory.CycleGraphSpectrum.C12_eigenvalue (k : ZMod 12) : ZMod.dft cycAdj k = ZMod.stdAddChar k + ZMod.stdAddChar (-k)

The C₁₂ eigenvalue, as a character sum. Only the two semitone steps m = 1, -1 contribute, giving dft cycAdj k = stdAddChar k + stdAddChar (-k) = ω^k + ω^(-k), ω = exp(2πi/12).

theorem MusicTheory.CycleGraphSpectrum.stdAddChar_eq_exp (k : ZMod 12) : ZMod.stdAddChar k = Complex.exp (2 * ↑Real.pi * Complex.I * ↑k.val / 12)

stdAddChar of a class equals the explicit root of unity exp(2πi·k.val/12).

theorem MusicTheory.CycleGraphSpectrum.C12_eigenvalue_cos (k : ZMod 12) : ZMod.dft cycAdj k = 2 * Complex.cos (2 * ↑Real.pi * ↑k.val / 12)

The C₁₂ eigenvalue in closed form (T3 payload). The k-th eigenvalue of the chromatic cycle graph is the textbook 2·cos(2πk/12) — the cosine spectrum of C₁₂.

T4 — the graph bridge: C12 IS Mathlib's cycle-graph adjacency matrix.

So the eigenvalues C12_eigenvalue_cos are LITERALLY the spectrum of SimpleGraph.cycleGraph 12. The Fin/ZMod subtraction-instance mismatch that defeats a direct rw [cycleGraph_adj] (cycleGraph lives over Fin n, our work over ZMod 12) is sidestepped by proving the adjacency characterization with decide over the 144 vertex pairs — the kernel evaluates both sides to a boolean, no pattern unification needed.

theorem MusicTheory.CycleGraphSpectrum.cycleGraph12_adj_iff (i j : ZMod 12) : (SimpleGraph.cycleGraph 12).Adj i j ↔ i - j = 1 ∨ i - j = -1

The adjacency relation of cycleGraph 12 on ℤ/12 is "differ by a semitone" (i - j = ±1). Checked by decide over the 144 pairs of Fin 12.

theorem MusicTheory.CycleGraphSpectrum.C12_eq_adjMatrix : C12 = SimpleGraph.adjMatrix ℂ (SimpleGraph.cycleGraph 12)

THE GRAPH BRIDGE (T4). The circulant C12 IS the adjacency matrix of the chromatic cycle graph cycleGraph 12 over ℂ. Combined with C12_eigenvalue_cos, this says the eigenvalues 2·cos(2πk/12) are the spectrum of Mathlib's SimpleGraph.cycleGraph 12.

theorem MusicTheory.CycleGraphSpectrum.C12_diagonalized_by_dftChar_basis (k : ZMod 12) : C12.mulVec (dftChar_basis k) = ZMod.dft cycAdj k • dftChar_basis k

THE PAYOFF (T2 ⋈ T1). C12 is diagonalized by the DFT basis: every basis vector dftChar_basis k is an eigenvector of C12 with eigenvalue dft cycAdj k. The eigenvectors range over a genuine basis (dftChar_basis), so the DFT is a full diagonalizing eigenbasis of the chromatic cycle graph's adjacency operator.

The spectrum of every abelian Cayley graph.

C₁₂ is one instance of a general fact: an abelian Cayley graph Cay(ℤ_N, S) — equivalently Mathlib's circulantGraph S over ZMod N — has adjacency operator the circulant of the connection-set indicator 1_S, so by T1 it is diagonalized by the DFT characters with eigenvalue the character sum ∑_{s∈S} stdAddChar(-(s·k)) (Babai's formula for abelian Cayley spectra). The bridge cayleyAdj S = circulantGraph S mirrors T4's C12_eq_adjMatrix, now for an arbitrary SYMMETRIC, 0∉S connection set. Folklore (Babai 1979, Lovász).

noncomputable def MusicTheory.CycleGraphSpectrum.cayleyAdjVec {N : ℕ} (S : Finset (ZMod N)) : ZMod N → ℂ

The connection-set indicator 1_S on ZMod N (first column of the Cayley adjacency matrix).

Equations

• MusicTheory.CycleGraphSpectrum.cayleyAdjVec S m = if m ∈ S then 1 else 0

noncomputable def MusicTheory.CycleGraphSpectrum.cayleyAdj {N : ℕ} (S : Finset (ZMod N)) : Matrix (ZMod N) (ZMod N) ℂ

The adjacency operator of the abelian Cayley graph Cay(ℤ_N, S), as a circulant over ℂ.

Equations

• MusicTheory.CycleGraphSpectrum.cayleyAdj S = Matrix.circulant (MusicTheory.CycleGraphSpectrum.cayleyAdjVec S)

theorem MusicTheory.CycleGraphSpectrum.cayleyAdj_mulVec_dftChar {N : ℕ} [NeZero N] (S : Finset (ZMod N)) (k : ZMod N) : (cayleyAdj S).mulVec (dftChar k) = ZMod.dft (cayleyAdjVec S) k • dftChar k

Abelian Cayley diagonalization (C-2). Every abelian Cayley graph is diagonalized by the DFT characters: cayleyAdj S *ᵥ dftChar k = (dft 1_S k) • dftChar k. Direct specialization of T1.

theorem MusicTheory.CycleGraphSpectrum.cayleyAdj_eigenvalue {N : ℕ} [NeZero N] (S : Finset (ZMod N)) (k : ZMod N) : ZMod.dft (cayleyAdjVec S) k = ∑ s ∈ S, ZMod.stdAddChar (-(s * k))

The abelian Cayley eigenvalue = the character sum (C-2, Babai's formula). The k-th eigenvalue is dft 1_S k = ∑_{s∈S} stdAddChar(-(s·k)) — sum of the k-th character over the connection set.

theorem MusicTheory.CycleGraphSpectrum.cayleyAdj_eq_adjMatrix {N : ℕ} (S : Finset (ZMod N)) (hsymm : ∀ x ∈ S, -x ∈ S) (h0 : 0 ∉ S) : cayleyAdj S = SimpleGraph.adjMatrix ℂ (SimpleGraph.circulantGraph ↑S)

The abelian Cayley graph bridge (C-2, mirrors T4). For a SYMMETRIC connection set S not containing 0, the circulant cayleyAdj S IS the adjacency matrix of Mathlib's circulantGraph S. Combined with cayleyAdj_eigenvalue this gives the spectrum of every such abelian Cayley graph.