The multiplication transform on the Fourier coefficients

For a unit u of ℤ/12, multiplying a pitch-class set by u permutes its Fourier coefficients: Ahat (u • A) t = Ahat A (u * t); with u = 5 this exchanges the first and fifth coefficients. The power ‖Ahat A 1‖² lies in ½ ℤ[√3]: 2 ‖Ahat A 1‖² = P + Q √3 with integers P, Q read from the interval vector, and the order of these values is decided in ℤ√3.

Main results

• Ahat_mul, Ahat_mul_norm, Ahat_M5, Ahat_M5_norm.
• powerSpec_one_eq: the ℤ[√3] form of the first power coefficient.
• toR3_le_iff, powerSpec_one_re_le_iff: the order of ℤ√3 agrees with the real order.

References

• E. Amiot, David Lewin and maximally even sets, J. Math. Music 1 (2007).
• I. Quinn, General equal-tempered harmony, Perspectives of New Music 44–45 (2006–2007).

noncomputable def MusicTheory.MTransform.ind (A : Finset (ZMod 12)) : ZMod 12 → ℂ

The 0/1 indicator of a pc-set (= Fourier.ind).

Equations

• MusicTheory.MTransform.ind A j = if j ∈ A then 1 else 0

noncomputable def MusicTheory.MTransform.Ahat (A : Finset (ZMod 12)) : ZMod 12 → ℂ

The DFT of a pc-set (= Fourier.Ahat):  A t = Σ_{a ∈ A} exp(−2πi·a·t/12).

Equations

• MusicTheory.MTransform.Ahat A = ZMod.dft (MusicTheory.MTransform.ind A)

theorem MusicTheory.MTransform.Ahat_apply (A : Finset (ZMod 12)) (t : ZMod 12) : Ahat A t = ∑ a ∈ A, ZMod.stdAddChar (-(a * t))

 A t = Σ_{a ∈ A} stdAddChar(−(a·t)) (= Fourier.Ahat_apply).

theorem MusicTheory.MTransform.unit_mul_injOn (u : (ZMod 12)ˣ) {s : Finset (ZMod 12)} (x : ZMod 12) : x ∈ s → ∀ y ∈ s, ↑u * x = ↑u * y → x = y

Left multiplication by a unit is injective on ZMod 12 (no NoZeroDivisors needed: cancel by u⁻¹). The witness fed to Finset.sum_image.

theorem MusicTheory.MTransform.Ahat_mul (u : (ZMod 12)ˣ) (A : Finset (ZMod 12)) (t : ZMod 12) : Ahat (Finset.image (fun (a : ZMod 12) => ↑u * a) A) t = Ahat A (↑u * t)

STAGE A — the M-transform coefficient permutation. For a unit u ∈ (ℤ/12)ˣ, multiplying every pitch class by u permutes the Fourier index: Â(u·A)(t) = Â(A)(u·t). Equivalently a_k(M_u A) = a_{u·k}(A) — Amiot's footnote / Quinn's Multiplication Principle.

theorem MusicTheory.MTransform.Ahat_mul_norm (u : (ZMod 12)ˣ) (A : Finset (ZMod 12)) (t : ZMod 12) : ‖Ahat (Finset.image (fun (a : ZMod 12) => ↑u * a) A) t‖ = ‖Ahat A (↑u * t)‖

Magnitude corollary. The M-transform preserves the spectrum up to the index permutation: ‖Â(u·A)(t)‖ = ‖Â(A)(u·t)‖.

def MusicTheory.MTransform.u5 : (ZMod 12)ˣ

5 is a unit of ℤ/12 (it is its own inverse: 5·5 = 25 ≡ 1). The M₅ "circle-of-fifths" multiplication used in Amiot's corollary.

Equations

• MusicTheory.MTransform.u5 = { val := 5, inv := 5, val_inv := MusicTheory.MTransform.u5._proof_1, inv_val := MusicTheory.MTransform.u5._proof_1 }

@[simp]

theorem MusicTheory.MTransform.u5_coe : ↑u5 = 5

theorem MusicTheory.MTransform.Ahat_M5 (A : Finset (ZMod 12)) : Ahat (Finset.image (fun (a : ZMod 12) => 5 * a) A) 1 = Ahat A 5

M-transform corollary, frequency 1 ↦ 5. With u = 5, the M-transform sends the k = 1 coefficient to the k = 5 coefficient: Â(M₅ A)(1) = Â(A)(5). This is the index map that turns the Huddling Lemma (cluster maximizes ‖a_1‖) into its M-corollary (the fifth-generated set, image of the cluster under M₅, maximizes ‖a_5‖).

theorem MusicTheory.MTransform.Ahat_M5_norm (A : Finset (ZMod 12)) : ‖Ahat (Finset.image (fun (a : ZMod 12) => 5 * a) A) 1‖ = ‖Ahat A 5‖

M-transform corollary (magnitudes), ‖a_1‖ ↦ ‖a_5‖. ‖Â(M₅ A)(1)‖ = ‖Â(A)(5)‖.

STAGE B — Amiot's Huddling Lemma: the ℤ[√3] reformulation and the decidable order.

Amiot 2007 (Huddling Lemma) maximizes ‖Â A 1‖, equivalently powerSpec A 1 = ‖Â A 1‖² ∈ ℝ. The 12th-root cosines cos(π d/6) introduce √3 at the d = ±1, ±5 interval classes, so the value is NOT rational: it lives in ℤ[√3] (scaled by ½). We FORMALIZE that reformulation here. This is a Lean restatement of Amiot's analysis, NOT new mathematics.

powerSpec, autocorr, IVraw live in Fourier.lean; IV k := IVraw A k is the interval vector.

KEYSTONE (powerSpec_one_eq): 2 · powerSpec A 1 = P A + (Q A)·√3 , with the INTEGER coefficients P A = 2·|A| + IV 2 − IV 4 − 2·IV 6 (the ℚ-part, ×2) Q A = IV 1 − IV 5 (the √3-part) The √3 ordering BLOCKS naive decide; mapping P + Q√3 ↦ (⟨P,Q⟩ : Zsqrtd 3) exposes Mathlib's LinearOrder (ℤ√d) (decidable), and toR3_le_iff bridges that order to the real spectrum order (Mathlib has Zsqrtd.toReal as a ring hom and its injectivity, not its monotonicity, which is proved here from SqLe/nonneg_cases).

theorem MusicTheory.MTransform.charZ (n : ℤ) : ZMod.stdAddChar ↑n = ↑(Real.cos (Real.pi * ↑n / 6)) + ↑(Real.sin (Real.pi * ↑n / 6)) * Complex.I

Bridge: stdAddChar of an integer residue as cos + sin·i (real cosines/sines).

def MusicTheory.MTransform.P (A : Finset (ZMod 12)) : ℤ

ℚ-part (×2) of 2·powerSpec A 1: P A = 2·|A| + IV 2 − IV 4 − 2·IV 6.

Equations

• MusicTheory.MTransform.P A = 2 * ↑A.card + ↑(MusicTheory.Fourier.IVraw A 2) - ↑(MusicTheory.Fourier.IVraw A 4) - 2 * ↑(MusicTheory.Fourier.IVraw A 6)

def MusicTheory.MTransform.Q (A : Finset (ZMod 12)) : ℤ

√3-part of 2·powerSpec A 1: Q A = IV 1 − IV 5.

Equations

• MusicTheory.MTransform.Q A = ↑(MusicTheory.Fourier.IVraw A 1) - ↑(MusicTheory.Fourier.IVraw A 5)

theorem MusicTheory.MTransform.powerSpec_one_eq (A : Finset (ZMod 12)) : 2 * Fourier.powerSpec A 1 = ↑(P A) + ↑(Q A) * ↑√3

STAGE B keystone — the ℤ[√3] reformulation of Amiot's Huddling target. 2 · powerSpec A 1 = P A + (Q A)·√3 with P A, Q A : ℤ the interval-vector combinations.

The decidable ℤ[√3] order (Zsqrtd 3) and the bridge to the real spectrum order.

Zsqrtd (3 : ℕ) is used (not Zsqrtd (3 : ℤ)) because Mathlib's LinearOrder (ℤ√d) is stated for d : ℕ. Zsqrtd.toReal is a ring hom but Mathlib does not prove it monotone, so we supply toR3_le_iff from the SqLe/nonneg_cases characterisation of the order.

def MusicTheory.MTransform.psZ (A : Finset (ZMod 12)) : ℤ√↑3

The ℤ[√3] coordinate vector of 2·powerSpec A 1 (= P A + Q A·√3).

Equations

• MusicTheory.MTransform.psZ A = { re := MusicTheory.MTransform.P A, im := MusicTheory.MTransform.Q A }

@[reducible, inline]

noncomputable abbrev MusicTheory.MTransform.toR3 : ℤ√↑3 →+* ℝ

ℤ[√3] ↪ ℝ, the canonical ring hom sending √3 ↦ Real.sqrt 3.

Equations

• MusicTheory.MTransform.toR3 = Zsqrtd.toReal MusicTheory.MTransform.toR3._proof_1

theorem MusicTheory.MTransform.toReal_psZ (A : Finset (ZMod 12)) : toR3 (psZ A) = 2 * (Fourier.powerSpec A 1).re

The image of psZ A in ℝ is exactly 2·Re(powerSpec A 1): the spectrum value lives in ℤ[√3].

theorem MusicTheory.MTransform.three_nonsquare (n : ℤ) : ↑3 ≠ n * n

3 is not a perfect square in ℤ (needed for Zsqrtd.toReal injectivity).

theorem MusicTheory.MTransform.zero_le_iff_toR3 (a : ℤ√↑3) : 0 ≤ a ↔ 0 ≤ toR3 a

0 ≤ a in ℤ[√3] iff 0 ≤ toR3 a in ℝ — monotonicity of Zsqrtd.toReal (not in Mathlib).

theorem MusicTheory.MTransform.toR3_le_iff (a b : ℤ√↑3) : a ≤ b ↔ toR3 a ≤ toR3 b

The ℤ[√3] order IS the real spectrum order. a ≤ b in ℤ[√3] iff toR3 a ≤ toR3 b.

theorem MusicTheory.MTransform.powerSpec_one_re_le_iff (A B : Finset (ZMod 12)) : (Fourier.powerSpec A 1).re ≤ (Fourier.powerSpec B 1).re ↔ psZ A ≤ psZ B

STAGE B bridge — the Huddling comparison reduced to the decidable ℤ[√3] order. Re(powerSpec A 1) ≤ Re(powerSpec B 1) iff psZ A ≤ psZ B in Zsqrtd 3 (a DecidableLE order). So Amiot's "cluster maximizes ‖a₁‖" becomes a finite decidable comparison.