The adjacency spectrum of the Tonnetz

The Tonnetz is the 3-regular graph on the 24 triads ZMod 12 × Bool with t — t' iff t' ∈ {P t, L t, R t}, the Cayley graph of the PLR group. Its adjacency matrix A over ℂ is symmetric, and the graph is bipartite on major/minor, so A v = λ v implies A (sign • v) = -λ (sign • v). Explicit eigenvectors give the eigenvalues ± {3, √5, 2 cos (π/12), √3, 1, 2 cos (5π/12)}, the values |1 + ζ⁴ + ζ⁻³| for ζ a 12th root of unity. That these are all the eigenvalues is proved in TonnetzCompleteness.

Main results

• A_symm, nbhd_card, A_bipartite, bipartite_neg_eigen.
• A_mulVec_ones, A_mulVec_sign: eigenvalues 3 and -3.
• A_mulVec_golden: eigenvalue √5.
• A_mulVec_uG: a generic eigenvector lemma for a 12th root of unity; A_mulVec_j4, A_mulVec_j2, A_mulVec_j1, A_mulVec_j5: eigenvalues √3, 1, √(2 - √3), √(2 + √3).
• A_mulVec_neg3, A_mulVec_negGolden, A_mulVec_negJ4, A_mulVec_negJ2, A_mulVec_negJ1, A_mulVec_negJ5: the negative eigenvalues.

References

• J. Douthett, P. Steinbach, Parsimonious graphs, J. Music Theory 42 (1998).
• A. S. Crans, T. M. Fiore, R. Satyendra, Musical actions of dihedral groups, Amer. Math. Monthly 116 (2009) 479–495.
• V. Lostanlen, Eigentriads and eigenprogressions on the Tonnetz, arXiv:1810.00790.
• 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.

Local re-statement of the triad type and the neo-Riemannian operations.

The same definitions as in NeoRiemannian (Triad, Pf, Lf, Rf). These are plain functions Triad → Triad (involutions); we only need them as the neighbour map of the Cayley graph.

@[reducible, inline]

abbrev MusicTheory.TonnetzSpectrum.Triad : Type

A triad: root pitch-class in ZMod 12, quality bit (true = major). 24 of them.

Equations

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

def MusicTheory.TonnetzSpectrum.Pf : Triad → Triad

Parallel: same root, flip quality.

Equations

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

def MusicTheory.TonnetzSpectrum.Lf : Triad → Triad

Leading-tone exchange.

Equations

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

def MusicTheory.TonnetzSpectrum.Rf : Triad → Triad

Relative.

Equations

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

The Cayley-graph adjacency operator over ℂ.

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

The neighbour relation: t — t' iff t' ∈ {P t, L t, R t}.

Equations

• MusicTheory.TonnetzSpectrum.adj t t' = if t' = MusicTheory.TonnetzSpectrum.Pf t ∨ t' = MusicTheory.TonnetzSpectrum.Lf t ∨ t' = MusicTheory.TonnetzSpectrum.Rf t then 1 else 0

def MusicTheory.TonnetzSpectrum.A : Matrix Triad Triad ℂ

The adjacency matrix of the PLR/Tonnetz Cayley graph, over ℂ.

Equations

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

@[simp]

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

T1a — symmetry. P, L, R are involutions, so the neighbour relation is symmetric.

theorem MusicTheory.TonnetzSpectrum.neighbour_symm (t t' : Triad) : t' = Pf t ∨ t' = Lf t ∨ t' = Rf t ↔ t = Pf t' ∨ t = Lf t' ∨ t = Rf t'

The neighbour relation as a Bool-decidable Prop is symmetric: t' ∈ {Pt,Lt,Rt} ↔ t ∈ {Pt',Lt',Rt'}. A finite check over all 24 × 24 triad pairs by decide.

theorem MusicTheory.TonnetzSpectrum.adj_symm (t t' : Triad) : adj t t' = adj t' t

adj is symmetric (over ℂ): proved via the underlying decidable Prop, NOT decide over ℂ.

theorem MusicTheory.TonnetzSpectrum.A_symm : A.IsSymm

T1a. The Tonnetz adjacency matrix is symmetric.

T1b — 3-regularity. The three neighbours P t, L t, R t are pairwise distinct.

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

The three neighbours are pairwise distinct for every triad (decidable Prop over Triad).

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

The neighbour set {P t, L t, R t} as a Finset Triad.

Equations

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

theorem MusicTheory.TonnetzSpectrum.nbhd_card (t : Triad) : (nbhd t).card = 3

T1b (3-regularity). Every triad has exactly three neighbours.

T1c — the +3 eigenvector (all-ones; row sum = #neighbours = 3).

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

For a fixed t, the matrix row adj t · is the indicator of the neighbour set nbhd t: adj t t' = if t' ∈ nbhd t then 1 else 0.

theorem MusicTheory.TonnetzSpectrum.A_mulVec_ones : (A.mulVec fun (x : Triad) => 1) = 3 • fun (x : Triad) => 1

T1c. The all-ones vector is an eigenvector of A with eigenvalue +3 (row sum = 3 neighbours).

T1d — the −3 eigenvector. P, L, R all FLIP the quality bit, so every edge crosses

major↔minor (the graph is bipartite on Bool); the sign vector s t = ±1 by quality is an eigenvector with eigenvalue −3.

def MusicTheory.TonnetzSpectrum.sign (t : Triad) : ℂ

The maj/min sign vector: +1 on major triads, −1 on minor.

Equations

• MusicTheory.TonnetzSpectrum.sign t = if t.2 = true then 1 else -1

theorem MusicTheory.TonnetzSpectrum.neighbours_flip (t : Triad) : (Pf t).2 = !t.2 ∧ (Lf t).2 = !t.2 ∧ (Rf t).2 = !t.2

P, L, R all flip the quality bit (decidable Prop over Triad).

theorem MusicTheory.TonnetzSpectrum.sign_flip (t : Triad) : sign (Pf t) = -sign t ∧ sign (Lf t) = -sign t ∧ sign (Rf t) = -sign t

The sign of a flipped quality is the negated sign: s on any neighbour is −(s t).

theorem MusicTheory.TonnetzSpectrum.row_sign_sum (t : Triad) : ∑ t' : Triad, adj t t' * sign t' = 3 * -sign t

The row adj t · weighted by sign sums to 3 · (−sign t): rewrite the sum over the explicit 3-element neighbour set, on each of which sign = −sign t.

theorem MusicTheory.TonnetzSpectrum.A_mulVec_sign : A.mulVec sign = -3 • sign

T1d. The maj/min sign vector is an eigenvector of A with eigenvalue −3 — every edge of the Tonnetz graph crosses major↔minor (bipartite on quality).

T1e — bipartiteness, as a named fact. Every neighbour has the opposite quality.

theorem MusicTheory.TonnetzSpectrum.A_bipartite (t t' : Triad) (h : adj t t' = 1) : t'.2 = !t.2

Bipartite on quality. Every Tonnetz edge crosses major↔minor: if t — t' then t'.2 = !t.2. (Immediate from neighbours_flip.)

T1f — bipartite negation. Because every edge crosses major↔minor, multiplying any

eigenvector by the maj/min sign vector negates its eigenvalue. One lemma, and every positive eigenvalue immediately yields its negative (and A_mulVec_sign falls out of A_mulVec_ones).

def MusicTheory.TonnetzSpectrum.signMul (v : Triad → ℂ) : Triad → ℂ

sign-twist of a vector: flip sign on the minor triads.

Equations

• MusicTheory.TonnetzSpectrum.signMul v t = MusicTheory.TonnetzSpectrum.sign t * v t

theorem MusicTheory.TonnetzSpectrum.adj_mul_sign (t t' : Triad) : adj t t' * sign t' = adj t t' * -sign t

On any edge the row weight times sign equals the row weight times −sign t (bipartiteness: adj t t' = 1 ⇒ sign t' = −sign t; otherwise both sides are 0).

theorem MusicTheory.TonnetzSpectrum.bipartite_neg_eigen (v : Triad → ℂ) (lam : ℂ) (h : A.mulVec v = lam • v) : A.mulVec (signMul v) = -lam • signMul v

T1f (bipartite negation). If v is an eigenvector with eigenvalue λ, then its sign-twist signMul v is an eigenvector with eigenvalue −λ. The Tonnetz graph is bipartite on quality, so the spectrum is symmetric about 0.

T2 — the golden eigenvalue √5. (GREEN.)

The j = 3 dihedral irrep. With ω = e^{2πi/12} the j = 3 value is |1 + ω³ + ω⁹| = |1 + i + i| = |1 + 2i| = √5 (since ω³ = i). Concretely, the diagonalizing character on roots is χ x = i^x (I is ω³, of order 4, and 12 is divisible by 4 so χ descends to ZMod 12). The explicit golden eigenvector is

  u (x, major) = χ x · (2 + i),      u (x, minor) = χ x · √5.

Verification, neighbour by neighbour. P, L, R send a major (x,true) to the three minors (x,false), (x+4,false), (x−3,false); using χ(x+4) = χ x and χ(x−3) = χ x · i:

  (A u)(x,major) = √5 · χ x · (1 + 1 + i) = √5 · χ x · (2 + i) = √5 · u(x,major).   ✓ (no √5²)

For a minor (x,false) the neighbours are the majors (x,true), (x−4,true), (x+3,true); with χ(x−4) = χ x, χ(x+3) = χ x · (−i):

  (A u)(x,minor) = (2+i) · χ x · (1 + 1 − i) = (2+i)(2−i) · χ x = 5 · χ x = √5 · u(x,minor),

the only place the identity (√5)² = 5 enters (Real.sq_sqrt). All i^k reduce by i⁴ = 1.

noncomputable def MusicTheory.TonnetzSpectrum.chi (x : ZMod 12) : ℂ

The order-4 character χ x = iˣ on the roots (i = ω³). Well-defined on ZMod 12 because i¹² = 1.

Equations

• MusicTheory.TonnetzSpectrum.chi x = Complex.I ^ x.val

theorem MusicTheory.TonnetzSpectrum.I_per : Complex.I ^ 12 = 1

i¹² = 1 (so χ descends to ZMod 12).

theorem MusicTheory.TonnetzSpectrum.chi_shift (x c : ZMod 12) : chi (x + c) = chi x * Complex.I ^ c.val

Character shift law: χ (x + c) = χ x · i^(c.val). (Exponents agree mod 12, and i¹² = 1.)

noncomputable def MusicTheory.TonnetzSpectrum.u : Triad → ℂ

The golden eigenvector of the Tonnetz adjacency operator (the j = 3 dihedral irrep): χ x · (2 + i) on majors, χ x · √5 on minors.

Equations

• MusicTheory.TonnetzSpectrum.u t = if t.2 = true then MusicTheory.TonnetzSpectrum.chi t.1 * (2 + Complex.I) else MusicTheory.TonnetzSpectrum.chi t.1 * ↑√5

@[simp]

theorem MusicTheory.TonnetzSpectrum.u_maj (x : ZMod 12) : u (x, true) = chi x * (2 + Complex.I)

@[simp]

theorem MusicTheory.TonnetzSpectrum.u_min (x : ZMod 12) : u (x, false) = chi x * ↑√5

theorem MusicTheory.TonnetzSpectrum.sqrt5_sq : ↑√5 ^ 2 = 5

(√5 : ℂ)² = 5 — the single irrational identity the minor case needs.

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

A generic row sum: Σ_{t'} adj t t' · f t' = f (P t) + f (L t) + f (R t) (reduce to the explicit 3-element neighbour set; NOT decide over ℂ).

theorem MusicTheory.TonnetzSpectrum.A_mulVec_golden : A.mulVec u = ↑√5 • u

T2 (the headline). The golden eigenvector u realizes the eigenvalue √5: A *ᵥ u = (√5 : ℂ) • u. This is the j = 3 dihedral-irrep eigenvalue |1 + ω³ + ω⁹| = √5, machine-checked component-wise over the 24 triads.

T3 — the remaining two-dimensional irreps, via a generic character.

For each j the diagonalizing character on roots is χ_ζ x = ζ^x with ζ = ω^j a 12th root of unity (ζ¹² = 1), and the eigenvector is u_ζ(x,maj) = ζ^x · p, u_ζ(x,min) = ζ^x · λ, with p = 1 + ζ⁴ + ζ⁻³ and λ = |p|. The major equation needs only p; the minor equation needs the single irrational identity p · conj p = λ². We package this once and specialize per j.

noncomputable def MusicTheory.TonnetzSpectrum.chiG (z : ℂ) (x : ZMod 12) : ℂ

A generic 12th-root character χ_z x = z^x (well-defined on ZMod 12 exactly when z¹² = 1).

Equations

• MusicTheory.TonnetzSpectrum.chiG z x = z ^ x.val

theorem MusicTheory.TonnetzSpectrum.chiG_shift (z : ℂ) (hz : z ^ 12 = 1) (x c : ZMod 12) : chiG z (x + c) = chiG z x * z ^ c.val

Generic character-shift law: for any z with z¹² = 1, χ_z (x + c) = χ_z x · z^(c.val).

noncomputable def MusicTheory.TonnetzSpectrum.uG (z p lam : ℂ) : Triad → ℂ

Generic eigenvector for parameters (z, p, lam): z^x · p on majors, z^x · lam on minors.

Equations

• MusicTheory.TonnetzSpectrum.uG z p lam t = if t.2 = true then MusicTheory.TonnetzSpectrum.chiG z t.1 * p else MusicTheory.TonnetzSpectrum.chiG z t.1 * lam

@[simp]

theorem MusicTheory.TonnetzSpectrum.uG_maj (z p lam : ℂ) (x : ZMod 12) : uG z p lam (x, true) = chiG z x * p

@[simp]

theorem MusicTheory.TonnetzSpectrum.uG_min (z p lam : ℂ) (x : ZMod 12) : uG z p lam (x, false) = chiG z x * lam

theorem MusicTheory.TonnetzSpectrum.A_mulVec_uG (z p lam : ℂ) (hz : z ^ 12 = 1) (hp : 1 + z ^ ZMod.val 4 + z ^ (-3).val = p) (hlam : p * (1 + z ^ (-4).val + z ^ ZMod.val 3) = lam ^ 2) : A.mulVec (uG z p lam) = lam • uG z p lam

Generic two-dimensional-irrep eigenvector lemma. Given a 12th root of unity z and scalars p, lam satisfying the structural relations p = 1 + z⁴ + z⁻³ (root-walk closes on the major side), lam² = p · (1 + z⁻⁴ + z³) (minor side; the irrational step), and lam · 1 = lam, lam·(z⁴.val…) handled by the shift law, the vector uG z p lam is an A-eigenvector with eigenvalue lam. The two hypotheses are hp : 1 + z^(4) + z^((-3:ZMod 12).val) = p and hlam : p * (1 + z^((-4:ZMod 12).val) + z^3) = lam^2.

j = 4 → eigenvalue √3. ζ = ω⁴ = e^{2πi/3}, a primitive cube root; p = 2 + ζ, |p| = √3.

noncomputable def MusicTheory.TonnetzSpectrum.z4 : ℂ

The primitive cube root ζ = ω⁴ = (−1 + √3·i)/2.

Equations

• MusicTheory.TonnetzSpectrum.z4 = (-1 + ↑√3 * Complex.I) / 2

theorem MusicTheory.TonnetzSpectrum.sqrt3_sq : ↑√3 ^ 2 = 3

(√3 : ℂ)² = 3.

theorem MusicTheory.TonnetzSpectrum.z4_quad : z4 ^ 2 + z4 + 1 = 0

z4² + z4 + 1 = 0 (z4 is a primitive cube root). Irrational inputs: (√3)² = 3, I² = −1.

theorem MusicTheory.TonnetzSpectrum.z4_cube : z4 ^ 3 = 1

z4³ = 1 (primitive cube root), from the quadratic relation.

theorem MusicTheory.TonnetzSpectrum.z4_pow12 : z4 ^ 12 = 1

z4¹² = 1.

theorem MusicTheory.TonnetzSpectrum.A_mulVec_j4 : A.mulVec (uG z4 (2 + z4) ↑√3) = ↑√3 • uG z4 (2 + z4) ↑√3

T3 (j = 4). Eigenvalue √3 = |1 + ω⁴ + ω¹²·ⁱ…|: the eigenvector uG z4 (2+z4) √3 satisfies A *ᵥ u = (√3 : ℂ) • u.

j = 2 → eigenvalue 1. ζ = ω² = e^{2πi/6}, a primitive 6th root; p = ζ⁸ = ω¹⁶, |p| = 1.

noncomputable def MusicTheory.TonnetzSpectrum.z2 : ℂ

The primitive 6th root ζ = ω² = (1 + √3·i)/2.

Equations

• MusicTheory.TonnetzSpectrum.z2 = (1 + ↑√3 * Complex.I) / 2

theorem MusicTheory.TonnetzSpectrum.z2_quad : z2 ^ 2 - z2 + 1 = 0

z2² − z2 + 1 = 0 (z2 is a primitive 6th root). Irrational inputs: (√3)² = 3, I² = −1.

theorem MusicTheory.TonnetzSpectrum.z2_cube : z2 ^ 3 = -1

z2³ = −1 (so z2⁶ = 1), from the quadratic relation.

theorem MusicTheory.TonnetzSpectrum.z2_pow12 : z2 ^ 12 = 1

z2¹² = 1.

theorem MusicTheory.TonnetzSpectrum.A_mulVec_j2 : A.mulVec (uG z2 (-z2) 1) = 1 • uG z2 (-z2) 1

T3 (j = 2). Eigenvalue 1: the eigenvector uG z2 (−z2) 1 satisfies A *ᵥ u = 1 • u. Here p = 1 + ζ⁴ + ζ⁹ = 1 − ζ − 1 = −ζ = −z2 (using ζ⁴ = ζ³·ζ = −ζ, ζ⁹ = ζ³ = −1) and λ = |p| = 1.

j = 1 → eigenvalue 2cos(5π/12) = √(2−√3). ζ = ω = e^{iπ/6} = (√3 + i)/2, a primitive

12th root. p = 1 + ζ⁴ + ζ⁻³ = 1 + ζ⁴ + ζ⁹, |p|² = 2 − √3. (The "hard" 12th-root case; closed via ζ³ = i, so every needed power is an explicit {1, ζ, ζ², i}-combination.)

noncomputable def MusicTheory.TonnetzSpectrum.z1 : ℂ

The primitive 12th root ζ = ω = (√3 + i)/2.

Equations

• MusicTheory.TonnetzSpectrum.z1 = (↑√3 + Complex.I) / 2

theorem MusicTheory.TonnetzSpectrum.z1_cube : z1 ^ 3 = Complex.I

z1³ = i. Irrational inputs (√3)² = 3, I² = −1.

theorem MusicTheory.TonnetzSpectrum.z1_pow12 : z1 ^ 12 = 1

z1¹² = 1 (= (z1³)⁴ = i⁴).

theorem MusicTheory.TonnetzSpectrum.sqrt2m3_sq : ↑√(2 - √3) ^ 2 = 2 - ↑√3

(√(2−√3) : ℂ)² = 2 − √3.

theorem MusicTheory.TonnetzSpectrum.A_mulVec_j1 : A.mulVec (uG z1 (1 + Complex.I * z1 - Complex.I) ↑√(2 - √3)) = ↑√(2 - √3) • uG z1 (1 + Complex.I * z1 - Complex.I) ↑√(2 - √3)

T3 (j = 1). Eigenvalue 2cos(5π/12) = √(2−√3).

j = 5 → eigenvalue 2cos(π/12) = √(2+√3). ζ = ω⁵ = e^{5iπ/6} = (−√3 + i)/2, a primitive

12th root. p = 1 + ζ⁴ + ζ⁹, |p|² = 2 + √3. Same machinery; ζ³ = i.

noncomputable def MusicTheory.TonnetzSpectrum.z5 : ℂ

The primitive 12th root ζ = ω⁵ = (−√3 + i)/2.

Equations

• MusicTheory.TonnetzSpectrum.z5 = (-↑√3 + Complex.I) / 2

theorem MusicTheory.TonnetzSpectrum.z5_cube : z5 ^ 3 = Complex.I

z5³ = i.

theorem MusicTheory.TonnetzSpectrum.z5_pow12 : z5 ^ 12 = 1

z5¹² = 1.

theorem MusicTheory.TonnetzSpectrum.sqrt2p3_sq : ↑√(2 + √3) ^ 2 = 2 + ↑√3

(√(2+√3) : ℂ)² = 2 + √3.

theorem MusicTheory.TonnetzSpectrum.A_mulVec_j5 : A.mulVec (uG z5 (1 + Complex.I * z5 - Complex.I) ↑√(2 + √3)) = ↑√(2 + √3) • uG z5 (1 + Complex.I * z5 - Complex.I) ↑√(2 + √3)

T3 (j = 5). Eigenvalue 2cos(π/12) = √(2+√3).

T3⁻ — the negative half of the spectrum, for free via bipartite negation.

Each positive eigenvector, twisted by sign, gives the matching negative eigenvalue. This realizes the full symmetric multiset ± {3, √5, 2cos(π/12), √3, 1, 2cos(5π/12)} without re-proving anything. (A_mulVec_sign above is the λ = 3 instance of the same fact, kept as a standalone for the header.)

theorem MusicTheory.TonnetzSpectrum.A_mulVec_neg3 : A.mulVec (signMul fun (x : Triad) => 1) = -3 • signMul fun (x : Triad) => 1

−3 (from the all-ones +3 eigenvector).

theorem MusicTheory.TonnetzSpectrum.A_mulVec_negGolden : A.mulVec (signMul u) = -↑√5 • signMul u

−√5 (the golden eigenvalue's reflection).

theorem MusicTheory.TonnetzSpectrum.A_mulVec_negJ4 : A.mulVec (signMul (uG z4 (2 + z4) ↑√3)) = -↑√3 • signMul (uG z4 (2 + z4) ↑√3)

−√3 (j = 4 reflection).

theorem MusicTheory.TonnetzSpectrum.A_mulVec_negJ2 : A.mulVec (signMul (uG z2 (-z2) 1)) = -1 • signMul (uG z2 (-z2) 1)

−1 (j = 2 reflection).

theorem MusicTheory.TonnetzSpectrum.A_mulVec_negJ1 : A.mulVec (signMul (uG z1 (1 + Complex.I * z1 - Complex.I) ↑√(2 - √3))) = -↑√(2 - √3) • signMul (uG z1 (1 + Complex.I * z1 - Complex.I) ↑√(2 - √3))

−2cos(5π/12) = −√(2−√3) (j = 1 reflection).

theorem MusicTheory.TonnetzSpectrum.A_mulVec_negJ5 : A.mulVec (signMul (uG z5 (1 + Complex.I * z5 - Complex.I) ↑√(2 + √3))) = -↑√(2 + √3) • signMul (uG z5 (1 + Complex.I * z5 - Complex.I) ↑√(2 + √3))

−2cos(π/12) = −√(2+√3) (j = 5 reflection).

Ramanujan bound. The PLR/Tonnetz graph is 3-regular (nbhd_card), so its degree is

d = 3 and the Ramanujan threshold for a d-regular graph is 2√(d−1) = 2√2. Among the non-trivial eigenvalues (i.e. excluding the Perron pair ±3) the one of largest modulus is the golden eigenvalue √5 = 2φ−1 (the j = 3 dihedral irrep, A_mulVec_golden). The core arithmetic fact is that √5 lies strictly below the bound 2√2 = √8 (since 5 < 8); hence the PLR graph satisfies the Ramanujan inequality λ_nontrivial ≤ 2√(d−1).

Graph: Douthett–Steinbach 1998 (chicken-wire torus / PLR cycles). Identification PLR ≅ D₂₄ = Cay(D₂₄, {P,L,R}): Crans–Fiore–Satyendra, "Musical actions of dihedral groups", AMM 116 (2009). Ramanujan graphs / the 2√(d−1) bound: Lubotzky–Phillips–Sarnak, "Ramanujan graphs", Combinatorica 8 (1988).

This corollary certifies the controlling inequality √5 < 2√2 and relies on the explicit eigenvectors above for the eigenvalue facts. That ±{3, √5, 2cos(π/12), √3, 1, 2cos(5π/12)} is the complete spectrum — and hence that √5 really is the largest non-trivial modulus — is proved in TonnetzCompleteness.

theorem MusicTheory.TonnetzSpectrum.golden_lt_ramanujan_bound : √5 < 2 * √2

The Ramanujan inequality for the PLR/Tonnetz graph (core). The golden eigenvalue √5 (the largest non-trivial PLR-graph eigenvalue) lies strictly below the 3-regular Ramanujan bound 2√(d−1) = 2√2. Arithmetic core: 2√2 = √8 and 5 < 8.