Huddling in ℤ/12

Among pitch-class sets of a given size, the consecutive collections maximize the first Fourier magnitude, with equality exactly for their transpositions (the twelve-tone case of CyclicHuddlingGeometry). Through the multiplication by 5, the chains of fifths maximize the fifth coefficient.

Main results

• arc_maximizes_power, arc_unique, arc_maximizes_norm.
• fifth_frequency_max, fifth_frequency_unique.

References

• E. Amiot, Discrete Fourier transform and Bach's good temperament, Music Theory Online 15 (2009), Lemma 2.
• C. Marín, Huddling, diatonic and pentatonic scales in Z12: Fourier maxima and convex-energy minima formalized in Lean 4, Zenodo (2026), doi:10.5281/zenodo.23121103.

theorem MusicTheory.Huddling.Ahat_eq_cyclic (A : Finset (ZMod 12)) (k : ZMod 12) : Fourier.Ahat A k = CyclicHuddling.Ahat A k

The twelve-tone Fourier interface agrees with the general set-sum interface.

def MusicTheory.Huddling.arc (k : ℕ) : Finset (ZMod 12)

The consecutive collection C_k = {0,...,k-1} in ZMod 12.

Equations

• MusicTheory.Huddling.arc k = Finset.image (fun (x : ℕ) => ↑x) (Finset.range k)

def MusicTheory.Huddling.orbitT (A : Finset (ZMod 12)) : Finset (Finset (ZMod 12))

The transposition orbit; equality at the Fourier maximum is equality up to transposition.

Equations

• MusicTheory.Huddling.orbitT A = Finset.image (fun (t : ZMod 12) => MusicTheory.Fourier.tpose t A) Finset.univ

def MusicTheory.Huddling.m5 (A : Finset (ZMod 12)) : Finset (ZMod 12)

Multiplication by five, an involution because 5² = 1 in ZMod 12.

Equations

• MusicTheory.Huddling.m5 A = Finset.image (fun (a : ZMod 12) => 5 * a) A

def MusicTheory.Huddling.fifthArc (k : ℕ) : Finset (ZMod 12)

A consecutive chain in the circle-of-fifths coordinates.

Equations

• MusicTheory.Huddling.fifthArc k = MusicTheory.Huddling.m5 (MusicTheory.Huddling.arc k)

@[simp]

theorem MusicTheory.Huddling.m5_card (A : Finset (ZMod 12)) : (m5 A).card = A.card

@[simp]

theorem MusicTheory.Huddling.m5_involutive (A : Finset (ZMod 12)) : m5 (m5 A) = A

theorem MusicTheory.Huddling.m5_tpose (t : ZMod 12) (A : Finset (ZMod 12)) : m5 (Fourier.tpose t A) = Fourier.tpose (5 * t) (m5 A)

theorem MusicTheory.Huddling.m5_mem_orbit_iff (A B : Finset (ZMod 12)) : m5 A ∈ orbitT B ↔ A ∈ orbitT (m5 B)

theorem MusicTheory.Huddling.powerSpec_m5 (A : Finset (ZMod 12)) : Fourier.powerSpec (m5 A) 1 = Fourier.powerSpec A 5

M5 permutes the Fourier power at frequencies 1 and 5, on the shared Fourier definitions.

theorem MusicTheory.Huddling.powerSpec_re_eq_norm_sq (A : Finset (ZMod 12)) (t : ZMod 12) : (Fourier.powerSpec A t).re = ‖Fourier.Ahat A t‖ ^ 2

Real power is the square of the complex magnitude.

theorem MusicTheory.Huddling.norm_tpose (s : ZMod 12) (A : Finset (ZMod 12)) (t : ZMod 12) : ‖Fourier.Ahat (Fourier.tpose s A) t‖ = ‖Fourier.Ahat A t‖

Transposition changes phase and preserves magnitude at every frequency.

theorem MusicTheory.Huddling.powerSpec_tpose_re (s : ZMod 12) (A : Finset (ZMod 12)) (t : ZMod 12) : (Fourier.powerSpec (Fourier.tpose s A) t).re = (Fourier.powerSpec A t).re

theorem MusicTheory.Huddling.powerSpec_one_re_eq_iff (A B : Finset (ZMod 12)) : (Fourier.powerSpec A 1).re = (Fourier.powerSpec B 1).re ↔ MTransform.psZ A = MTransform.psZ B

theorem MusicTheory.Huddling.arc_maximizes_power (A : Finset (ZMod 12)) : (Fourier.powerSpec A 1).re ≤ (Fourier.powerSpec (arc A.card) 1).re

Huddling inequality: the consecutive collection maximizes a1 at fixed cardinality.

theorem MusicTheory.Huddling.arc_unique (A : Finset (ZMod 12)) : (Fourier.powerSpec A 1).re = (Fourier.powerSpec (arc A.card) 1).re ↔ A ∈ orbitT (arc A.card)

Equality in Huddling holds precisely for the transposes of the consecutive collection.

theorem MusicTheory.Huddling.huddling_census (A : Finset (ZMod 12)) : A ∈ Finset.univ.powerset → MTransform.psZ A ≤ MTransform.psZ (arc A.card) ∧ (MTransform.psZ A = MTransform.psZ (arc A.card) → A ∈ orbitT (arc A.card))

Backward-compatible finite certificate, now derived from the structural theorem. Despite its historical name, no census is evaluated.

theorem MusicTheory.Huddling.arc_maximizes_norm (A : Finset (ZMod 12)) : ‖Fourier.Ahat A 1‖ ≤ ‖Fourier.Ahat (arc A.card) 1‖

The same maximum in the magnitude formulation used by Amiot.

theorem MusicTheory.Huddling.fifth_frequency_max (A : Finset (ZMod 12)) : (Fourier.powerSpec A 5).re ≤ (Fourier.powerSpec (fifthArc A.card) 5).re

Huddling transported through M5: a fifth chain maximizes the fifth Fourier magnitude.

theorem MusicTheory.Huddling.fifth_frequency_unique (A : Finset (ZMod 12)) : (Fourier.powerSpec A 5).re = (Fourier.powerSpec (fifthArc A.card) 5).re ↔ A ∈ orbitT (fifthArc A.card)

The fifth-frequency equality class is exactly the transposition orbit of a fifth chain.