Completeness of the Tonnetz spectrum

ℂ^(ZMod 12 × Bool) is ℂ^(ZMod 12) ⊗ ℂ². For each frequency k the Tonnetz adjacency matrix preserves dftChar k ⊗ ℂ² and acts there as a 2 × 2 block with eigenvalues ±λ k, λ k ^ 2 = pp k * pm k. The 24 eigenvectors so obtained are linearly independent (a tensor product of the character basis with an independent pair for each character), hence a basis. So A is diagonalizable with exactly these eigenvalues, without the classification of the irreducible representations of the dihedral group.

Main results

• tensor_linearIndependent: characters tensored with independent pairs are independent.
• eigFam_is_eigenvector, eigFam_linearIndependent, eigenBasis.
• tonnetz_spectrum_complete, tonnetz_spectrum_complete_unconditional: a basis of eigenvectors with eigenvalues ±λ k.

References

• 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.

The triad type, neo-Riemannian ops, and the adjacency operator (re-stated, as in

TonnetzSpectrum.lean).

@[reducible, inline]

abbrev MusicTheory.TonnetzCompleteness.Triad : Type

Equations

• MusicTheory.TonnetzCompleteness.Triad = (ZMod 12 × Bool)

def MusicTheory.TonnetzCompleteness.Pf : Triad → Triad

Equations

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

def MusicTheory.TonnetzCompleteness.Lf : Triad → Triad

Equations

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

def MusicTheory.TonnetzCompleteness.Rf : Triad → Triad

Equations

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

def MusicTheory.TonnetzCompleteness.adj (t t' : Triad) : ℂ

Equations

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

def MusicTheory.TonnetzCompleteness.A : Matrix Triad Triad ℂ

Equations

• MusicTheory.TonnetzCompleteness.A = Matrix.of MusicTheory.TonnetzCompleteness.adj

@[simp]

theorem MusicTheory.TonnetzCompleteness.A_apply (t t' : Triad) : A t t' = adj t t'

theorem MusicTheory.TonnetzCompleteness.neighbours_distinct (t : Triad) : Pf t ≠ Lf t ∧ Pf t ≠ Rf t ∧ Lf t ≠ Rf t

def MusicTheory.TonnetzCompleteness.nbhd (t : Triad) : Finset Triad

Equations

• MusicTheory.TonnetzCompleteness.nbhd t = {MusicTheory.TonnetzCompleteness.Pf t, MusicTheory.TonnetzCompleteness.Lf t, MusicTheory.TonnetzCompleteness.Rf t}

theorem MusicTheory.TonnetzCompleteness.adj_eq_indicator (t t' : Triad) : adj t t' = if t' ∈ nbhd t then 1 else 0

theorem MusicTheory.TonnetzCompleteness.row_sum (f : Triad → ℂ) (t : Triad) : ∑ t' : Triad, adj t t' * f t' = f (Pf t) + f (Lf t) + f (Rf t)

The generic row sum: Σ_{t'} adj t t' · f t' = f (P t) + f (L t) + f (R t).

The DFT character on the root, and its shift law.

noncomputable def MusicTheory.TonnetzCompleteness.dftChar (k : ZMod 12) : ZMod 12 → ℂ

The k-th DFT character on the root: dftChar k x = stdAddChar (x * k).

Equations

• MusicTheory.TonnetzCompleteness.dftChar k x = ZMod.stdAddChar (x * k)

@[simp]

theorem MusicTheory.TonnetzCompleteness.dftChar_apply (k x : ZMod 12) : dftChar k x = ZMod.stdAddChar (x * k)

theorem MusicTheory.TonnetzCompleteness.dftChar_shift (k x c : ZMod 12) : dftChar k (x + c) = dftChar k x * ZMod.stdAddChar (c * k)

Character shift law: dftChar k (x + c) = dftChar k x · stdAddChar (c * k).

The generic eigenvector eig k q (x,b) = dftChar k x · q b.

For the quality 2-vector q : Bool → ℂ, the vector eig k q is an A-eigenvector with eigenvalue lam provided the two structural relations hold: q false · (1 + stdAddChar (4·k) + stdAddChar ((-3)·k)) = lam · q true (major side), q true · (1 + stdAddChar ((-4)·k) + stdAddChar (3·k)) = lam · q false (minor side).

noncomputable def MusicTheory.TonnetzCompleteness.eig (k : ZMod 12) (q : Bool → ℂ) : Triad → ℂ

The eigenvector skeleton: DFT character on the root times a quality 2-vector.

Equations

• MusicTheory.TonnetzCompleteness.eig k q t = MusicTheory.TonnetzCompleteness.dftChar k t.1 * q t.2

@[simp]

theorem MusicTheory.TonnetzCompleteness.eig_maj (k : ZMod 12) (q : Bool → ℂ) (x : ZMod 12) : eig k q (x, true) = dftChar k x * q true

@[simp]

theorem MusicTheory.TonnetzCompleteness.eig_min (k : ZMod 12) (q : Bool → ℂ) (x : ZMod 12) : eig k q (x, false) = dftChar k x * q false

theorem MusicTheory.TonnetzCompleteness.A_mulVec_eig (k : ZMod 12) (q : Bool → ℂ) (lam : ℂ) (hmaj : q false * (1 + ZMod.stdAddChar (4 * k) + ZMod.stdAddChar (-3 * k)) = lam * q true) (hmin : q true * (1 + ZMod.stdAddChar (-4 * k) + ZMod.stdAddChar (3 * k)) = lam * q false) : A.mulVec (eig k q) = lam • eig k q

Generic eigenvector lemma (dftChar form). Given the two structural relations, eig k q is an A-eigenvector with eigenvalue lam.

DFT-character linear independence (as in CycleGraphSpectrum).

theorem MusicTheory.TonnetzCompleteness.dftChar_eq_smul_invDFT (k : ZMod 12) : dftChar k = 12 • ZMod.dft.symm (Pi.single k 1)

The k-th DFT character is N times the inverse-DFT of the standard delta Pi.single k 1.

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

Sealed helper (as in CycleGraphSpectrum): the standard basis pushed through an injective map.

theorem MusicTheory.TonnetzCompleteness.dftChar_linearIndependent : LinearIndependent ℂ fun (k : ZMod 12) => dftChar k

The DFT characters are linearly independent.

Abstract "(character basis) ⊗ (independent quality pair)" independence.

theorem MusicTheory.TonnetzCompleteness.tensor_linearIndependent {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (f : ι → ι → ℂ) (hf : LinearIndependent ℂ f) (q : ι → κ → κ → ℂ) (hq : ∀ (i : ι), LinearIndependent ℂ (q i)) : LinearIndependent ℂ fun (ib xb : ι × κ) => f ib.1 xb.1 * q ib.1 ib.2 xb.2

Abstract product-independence. If (f i)_i is a linearly independent family in ι → ℂ and for each i, (q i b)_{b} is a linearly independent family in κ → ℂ, then the tensor family (x, b') ↦ f i x * q i b b' indexed by (i, b) is linearly independent in (ι × κ) → ℂ.

The unconditional 24-vector BASIS of ℂ^Triad.

The 24 vectors eig j (Pi.single b 1) — DFT character on the root tensored with a STANDARD quality basis vector — are linearly independent (character basis ⊗ standard basis, both manifestly independent), hence (card = 24 = dim) a BASIS of Triad → ℂ. This is the structural backbone of completeness: A preserves each frequency's 2-dim quality block (the eigenvector lemma A_mulVec_eig says so), so in this basis A is block-diagonal with twelve explicit 2×2 blocks.

noncomputable def MusicTheory.TonnetzCompleteness.stdFam : ZMod 12 × Bool → Triad → ℂ

The standard product family: stdFam (j,b) (x,b') = dftChar j x · (Pi.single b 1) b', i.e. dftChar j on the root, the b-th standard quality vector on the quality bit.

Equations

• MusicTheory.TonnetzCompleteness.stdFam jb xb = MusicTheory.TonnetzCompleteness.dftChar jb.1 xb.1 * Pi.single jb.2 1 xb.2

theorem MusicTheory.TonnetzCompleteness.stdFam_linearIndependent : LinearIndependent ℂ stdFam

The 24 standard product vectors are linearly independent.

theorem MusicTheory.TonnetzCompleteness.finrank_triad_fun : Module.finrank ℂ (Triad → ℂ) = Fintype.card (ZMod 12 × Bool)

Triad → ℂ has dimension 24 = card (ZMod 12 × Bool).

noncomputable def MusicTheory.TonnetzCompleteness.tonnetzBasis : Module.Basis (ZMod 12 × Bool) ℂ (Triad → ℂ)

THE COMPLETENESS BASIS. The 24 vectors stdFam (j,b) form a basis of Triad → ℂ. (Linear independence + card = dim.) In this basis A is block-diagonal across the 12 frequencies; combined with A_mulVec_eig this exhibits the full spectrum as the twelve 2×2 quality blocks.

Equations

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

@[simp]

theorem MusicTheory.TonnetzCompleteness.tonnetzBasis_apply (jb : ZMod 12 × Bool) : tonnetzBasis jb = stdFam jb

The completeness ENGINE: a basis of A-eigenvectors ⇒ spectrum complete.

The general, reusable statement. The per-frequency major/minor structure constants are pp k = 1 + stdAddChar (4·k) + stdAddChar ((-3)·k), pm k = 1 + stdAddChar ((-4)·k) + stdAddChar (3·k), and the two quality eigenvectors for frequency k are q⁺ = (pp k, lam), q⁻ = (pp k, -lam) with lam² = pp k · pm k. These are A-eigenvectors with eigenvalues ± lam (lemma A_mulVec_eig), and across the 12 frequencies they form a basis IFF, per frequency, the pair q⁺, q⁻ is independent — equivalently pp k ≠ 0 (then lam ≠ 0 too, since lam² = ‖pp k‖² ≠ 0).

noncomputable def MusicTheory.TonnetzCompleteness.pp (k : ZMod 12) : ℂ

Major-side structure constant pp k = 1 + ω^{4k} + ω^{-3k}.

Equations

• MusicTheory.TonnetzCompleteness.pp k = 1 + ZMod.stdAddChar (4 * k) + ZMod.stdAddChar (-3 * k)

noncomputable def MusicTheory.TonnetzCompleteness.pm (k : ZMod 12) : ℂ

Minor-side structure constant pm k = 1 + ω^{-4k} + ω^{3k}.

Equations

• MusicTheory.TonnetzCompleteness.pm k = 1 + ZMod.stdAddChar (-4 * k) + ZMod.stdAddChar (3 * k)

noncomputable def MusicTheory.TonnetzCompleteness.qPlus (k : ZMod 12) (lam : ℂ) : Bool → ℂ

The + quality eigenvector for frequency k: (pp k, lam).

Equations

• MusicTheory.TonnetzCompleteness.qPlus k lam b = if b = true then MusicTheory.TonnetzCompleteness.pp k else lam

noncomputable def MusicTheory.TonnetzCompleteness.qMinus (k : ZMod 12) (lam : ℂ) : Bool → ℂ

The − quality eigenvector for frequency k: (pp k, −lam).

Equations

• MusicTheory.TonnetzCompleteness.qMinus k lam b = if b = true then MusicTheory.TonnetzCompleteness.pp k else -lam

@[simp]

theorem MusicTheory.TonnetzCompleteness.qPlus_true (k : ZMod 12) (lam : ℂ) : qPlus k lam true = pp k

@[simp]

theorem MusicTheory.TonnetzCompleteness.qPlus_false (k : ZMod 12) (lam : ℂ) : qPlus k lam false = lam

@[simp]

theorem MusicTheory.TonnetzCompleteness.qMinus_true (k : ZMod 12) (lam : ℂ) : qMinus k lam true = pp k

@[simp]

theorem MusicTheory.TonnetzCompleteness.qMinus_false (k : ZMod 12) (lam : ℂ) : qMinus k lam false = -lam

theorem MusicTheory.TonnetzCompleteness.A_mulVec_eig_plus (k : ZMod 12) (lam : ℂ) (hlam : lam ^ 2 = pp k * pm k) : A.mulVec (eig k (qPlus k lam)) = lam • eig k (qPlus k lam)

eig k (qPlus k lam) is an A-eigenvector with eigenvalue lam, when lam² = pp k · pm k.

theorem MusicTheory.TonnetzCompleteness.A_mulVec_eig_minus (k : ZMod 12) (lam : ℂ) (hlam : lam ^ 2 = pp k * pm k) : A.mulVec (eig k (qMinus k lam)) = -lam • eig k (qMinus k lam)

eig k (qMinus k lam) is an A-eigenvector with eigenvalue −lam, when lam² = pp k · pm k.

theorem MusicTheory.TonnetzCompleteness.qPair_linearIndependent (k : ZMod 12) (lam : ℂ) (hpp : pp k ≠ 0) (hlam : lam ≠ 0) : LinearIndependent ℂ fun (s : Bool) => bif s then qPlus k lam else qMinus k lam

For each frequency, the two quality eigenvectors are linearly independent ⟺ pp k ≠ 0 ∧ lam ≠ 0. Here we prove the ⇐ direction (the one we need): nonvanishing ⇒ independence.

The capstone: a BASIS of A-eigenvectors ⇒ the spectrum is complete.

Assemble the 24 vectors. lam : ZMod 12 → ℂ picks, per frequency, a complex square root of pp k · pm k (it exists — ℂ is algebraically closed). The eigenvector family is eigFam (k, s) = eig k (qPlus k (lam k)) for s = true (eigenvalue lam k), eigFam (k, s) = eig k (qMinus k (lam k)) for s = false (eigenvalue −lam k). Given the per-frequency nonvanishing pp k ≠ 0 ∧ lam k ≠ 0, the 24 are linearly independent (tensor_linearIndependent ∘ qPair_linearIndependent), hence a BASIS — a diagonalization of A.

noncomputable def MusicTheory.TonnetzCompleteness.eigFam (lam : ZMod 12 → ℂ) : ZMod 12 × Bool → Triad → ℂ

The 24-vector eigen-family (parametrized by a choice of square roots lam).

Equations

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

theorem MusicTheory.TonnetzCompleteness.eigFam_is_eigenvector (lam : ZMod 12 → ℂ) (hlam : ∀ (k : ZMod 12), lam k ^ 2 = pp k * pm k) (k : ZMod 12) (s : Bool) : A.mulVec (eigFam lam (k, s)) = (bif s then lam k else -lam k) • eigFam lam (k, s)

Each member of eigFam is an A-eigenvector (eigenvalue ± lam k), given lam k² = pp k·pm k.

theorem MusicTheory.TonnetzCompleteness.eigFam_linearIndependent (lam : ZMod 12 → ℂ) (hpp : ∀ (k : ZMod 12), pp k ≠ 0) (hlamne : ∀ (k : ZMod 12), lam k ≠ 0) : LinearIndependent ℂ (eigFam lam)

The eigen-family is linearly independent (given per-frequency nonvanishing). The crux: the "(DFT character basis) ⊗ (per-frequency independent quality pair)" lemma.

noncomputable def MusicTheory.TonnetzCompleteness.eigenBasis (lam : ZMod 12 → ℂ) (hpp : ∀ (k : ZMod 12), pp k ≠ 0) (hlamne : ∀ (k : ZMod 12), lam k ≠ 0) : Module.Basis (ZMod 12 × Bool) ℂ (Triad → ℂ)

THE COMPLETENESS BASIS OF EIGENVECTORS (engine). Given square roots lam k of pp k·pm k with pp k ≠ 0 and lam k ≠ 0 for every frequency, the 24 vectors eigFam lam form a BASIS of Triad → ℂ consisting of A-eigenvectors. This is a full diagonalization of the Tonnetz adjacency operator: the certified eigenvalues ± lam k (k = 0..11) are ALL of the spectrum, with their multiplicities — completeness, without the dihedral-irrep classification.

Equations

• MusicTheory.TonnetzCompleteness.eigenBasis lam hpp hlamne = basisOfLinearIndependentOfCardEqFinrank ⋯ MusicTheory.TonnetzCompleteness.tonnetzBasis._proof_2

@[simp]

theorem MusicTheory.TonnetzCompleteness.eigenBasis_apply (lam : ZMod 12 → ℂ) (hpp : ∀ (k : ZMod 12), pp k ≠ 0) (hlamne : ∀ (k : ZMod 12), lam k ≠ 0) (ks : ZMod 12 × Bool) : (eigenBasis lam hpp hlamne) ks = eigFam lam ks

Reducing the residual hypothesis to the single fact pp k ≠ 0.

pm k = conj (pp k) (the minor-side constant is the complex conjugate of the major-side one, since stdAddChar is unimodular), hence pp k · pm k = ‖pp k‖². So the square root lam k exists (ℂ is algebraically closed) and is nonzero exactly when pp k ≠ 0; the whole eigen-basis is then a basis of A-eigenvectors. The completeness of the Tonnetz spectrum thus rests on the SINGLE concrete algebraic input ∀ k, pp k ≠ 0.

theorem MusicTheory.TonnetzCompleteness.conj_stdAddChar (a : ZMod 12) : (starRingEnd ℂ) (ZMod.stdAddChar a) = ZMod.stdAddChar (-a)

conj (stdAddChar a) = stdAddChar (-a) — stdAddChar is unimodular (factors through Circle).

theorem MusicTheory.TonnetzCompleteness.pm_eq_conj_pp (k : ZMod 12) : pm k = (starRingEnd ℂ) (pp k)

pm k = conj (pp k): the minor-side structure constant is the conjugate of the major-side one.

theorem MusicTheory.TonnetzCompleteness.pp_mul_pm (k : ZMod 12) : pp k * pm k = ↑(Complex.normSq (pp k))

pp k · pm k = ‖pp k‖² (a nonneg real); in particular it is 0 iff pp k = 0.

theorem MusicTheory.TonnetzCompleteness.pp_mul_pm_ne_zero (k : ZMod 12) (hpp : pp k ≠ 0) : pp k * pm k ≠ 0

pp k · pm k ≠ 0 precisely when pp k ≠ 0.

theorem MusicTheory.TonnetzCompleteness.tonnetz_spectrum_complete (hpp : ∀ (k : ZMod 12), pp k ≠ 0) : ∃ (lam : ZMod 12 → ℂ), (∀ (k : ZMod 12), lam k ^ 2 = pp k * pm k) ∧ ∃ (B : Module.Basis (ZMod 12 × Bool) ℂ (Triad → ℂ)), ∀ (ks : ZMod 12 × Bool), A.mulVec (B ks) = (bif ks.2 then lam ks.1 else -lam ks.1) • B ks

THE COMPLETENESS THEOREM (packaged). Assuming only the concrete algebraic nonvanishing ∀ k, pp k ≠ 0, the Tonnetz adjacency operator A has a BASIS of eigenvectors — i.e. it is diagonalizable and the certified eigenvalues ± √(pp k · pm k) (k = 0..11) are its COMPLETE spectrum with multiplicities. The square roots are produced from ℂ being algebraically closed; no dihedral-irrep classification.

Discharging the residual ∀ k, pp k ≠ 0: explicit root-of-unity arithmetic.

pp k = 1 + ω^{4k} + ω^{-3k} only ever involves ω^m for m ∈ {0,3,4,6,8,9}. We evaluate these six stdAddChar values to their closed forms (exp(2πi m/12)), giving pp k = (rational) + (rational)·I whose REAL part is one of {3, 1, 2, 3/2, 1/2, -1/2} for every k — never zero. Hence pp k ≠ 0 for all 12 frequencies, by a decide exponent reduction + Complex.re extraction. Elementary algebraic arithmetic on twelfth roots of unity.

theorem MusicTheory.TonnetzCompleteness.pp_ne_zero (k : ZMod 12) : pp k ≠ 0

THE RESIDUAL NONVANISHING — DISCHARGED. pp k ≠ 0 for every frequency k. The 12 cases use the six explicit twelfth-root values; each pp k has nonzero real part.

The unconditional completeness theorem.

theorem MusicTheory.TonnetzCompleteness.tonnetz_spectrum_complete_unconditional : ∃ (lam : ZMod 12 → ℂ), (∀ (k : ZMod 12), lam k ^ 2 = pp k * pm k) ∧ ∃ (B : Module.Basis (ZMod 12 × Bool) ℂ (Triad → ℂ)), ∀ (ks : ZMod 12 × Bool), A.mulVec (B ks) = (bif ks.2 then lam ks.1 else -lam ks.1) • B ks

THE TONNETZ SPECTRUM IS COMPLETE (unconditional). The adjacency operator A of the PLR/Tonnetz Cayley graph has a BASIS of 24 explicit eigenvectors — it is diagonalizable, and the eigenvalues ± √(pp k · pm k) (k = 0..11), which are exactly ± {3, √5, 2cos(π/12), √3, 1, 2cos(5π/12)} with their multiplicities, are its COMPLETE spectrum, without the dihedral-irrep classification.