Homometry, complementation and the pentatonic extremality

Homometric sets have the same interval vector, hence the same all-pairs energy for every potential; homometry is preserved by complementation; the diatonic has no homometric partner outside its orbit. Complementation changes the energy by a constant depending only on the size, which transfers the diatonic results to the pentatonic.

Main results

• energy_eq_of_homometric, homometric_compl, energy_compl_eq_of_homometric.
• diatonic_homometric_iff.
• m5_preserves_a6, m5_commutes_tritone.
• energy_compl.
• pentatonic_norm_max, pentatonic_norm_unique, pentatonic_energy_min, pentatonic_spectral_energy_equivalence.

References

• N. Bushaw, B. Cody, C. Leffler, Sets of vertices with extremal energy, arXiv:2407.18785, Theorem 3.5.
• 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.ExtremalityConnections.iv_eq_raw_div_two (A : Finset (ZMod 12)) (k : ℕ) : AllPairsEvenness.iv A k = Fourier.IVraw A k / 2

Bridge the unordered energy convention to the earlier ordered Fourier convention. At distance zero this is merely an identity between the definitions; energies use 1..6.

theorem MusicTheory.ExtremalityConnections.homometric_iv_eq (A B : Finset (ZMod 12)) (h : Fourier.Homometric A B) (k : ℕ) : AllPairsEvenness.iv A k = AllPairsEvenness.iv B k

Homometry fixes every unordered interval-vector entry.

theorem MusicTheory.ExtremalityConnections.energy_eq_of_homometric (V : ℕ → ℝ) (A B : Finset (ZMod 12)) (h : Fourier.Homometric A B) : AllPairsEvenness.E V A = AllPairsEvenness.E V B

Every all-pairs distance potential is blind to homometric differences. No convexity needed.

theorem MusicTheory.ExtremalityConnections.homometric_tpose (s : ZMod 12) (A : Finset (ZMod 12)) : Fourier.Homometric (Fourier.tpose s A) A

theorem MusicTheory.ExtremalityConnections.energy_tpose (V : ℕ → ℝ) (s : ZMod 12) (A : Finset (ZMod 12)) : AllPairsEvenness.E V (Fourier.tpose s A) = AllPairsEvenness.E V A

theorem MusicTheory.ExtremalityConnections.diatonic_orbit_eq_transpositions : AllPairsEvenness.orbitTI = Huddling.orbitT AllPairsEvenness.D

theorem MusicTheory.ExtremalityConnections.diatonic_homometric_iff (A : Finset (ZMod 12)) : Fourier.Homometric A AllPairsEvenness.D ↔ A ∈ AllPairsEvenness.orbitTI

Extremal spectral rigidity: the diatonic has no nontrivial homometric partner.

theorem MusicTheory.ExtremalityConnections.m5_preserves_a6 (A : Finset (ZMod 12)) : Fourier.Ahat (Huddling.m5 A) 6 = Fourier.Ahat A 6

M5 preserves the full sixth coefficient, hence the parity observable a₆.

theorem MusicTheory.ExtremalityConnections.m5_commutes_tritone (A : Finset (ZMod 12)) : Huddling.m5 (Fourier.tpose 6 A) = Fourier.tpose 6 (Huddling.m5 A)

The coordinate change commutes with the tritone transposition T₆.

theorem MusicTheory.ExtremalityConnections.tpose_compl (s : ZMod 12) (A : Finset (ZMod 12)) : (Fourier.tpose s A)ᶜ = Fourier.tpose s Aᶜ

theorem MusicTheory.ExtremalityConnections.norm_compl (A : Finset (ZMod 12)) (t : ZMod 12) (ht : t ≠ 0) : ‖Fourier.Ahat Aᶜ t‖ = ‖Fourier.Ahat A t‖

Complementing a set preserves every nonzero-frequency magnitude.

theorem MusicTheory.ExtremalityConnections.commonTones_compl (A : Finset (ZMod 12)) (t : ZMod 12) : Fourier.commonTones Aᶜ t + 2 * A.card = 12 + Fourier.commonTones A t

Complement interval identity in autocorrelation form, including the zero difference.

theorem MusicTheory.ExtremalityConnections.homometric_compl (A B : Finset (ZMod 12)) (h : Fourier.Homometric A B) : Fourier.Homometric Aᶜ Bᶜ

Homometry survives complementation: the zero autocorrelation fixes cardinality, and every other autocorrelation receives the same complement correction.

theorem MusicTheory.ExtremalityConnections.energy_compl_eq_of_homometric (V : ℕ → ℝ) (A B : Finset (ZMod 12)) (h : Fourier.Homometric A B) : AllPairsEvenness.E V Aᶜ = AllPairsEvenness.E V Bᶜ

The homometry/complement square commutes for every all-pairs potential.

theorem MusicTheory.ExtremalityConnections.iv_eq_commonTones (A : Finset (ZMod 12)) (k : ℕ) (h1 : 1 ≤ k) (h5 : k ≤ 5) : AllPairsEvenness.iv A k = Fourier.commonTones A ↑k

theorem MusicTheory.ExtremalityConnections.iv_compl_add (A : Finset (ZMod 12)) (k : ℕ) (h1 : 1 ≤ k) (h5 : k ≤ 5) : AllPairsEvenness.iv Aᶜ k + 2 * A.card = 12 + AllPairsEvenness.iv A k

The complement theorem in unordered-pair convention, away from the tritone.

theorem MusicTheory.ExtremalityConnections.iv_compl_tritone_add (A : Finset (ZMod 12)) : AllPairsEvenness.iv Aᶜ 6 + A.card = 6 + AllPairsEvenness.iv A 6

At the tritone the complement correction is half as large.

theorem MusicTheory.ExtremalityConnections.energy_compl (V : ℕ → ℝ) (A : Finset (ZMod 12)) : AllPairsEvenness.E V Aᶜ - AllPairsEvenness.E V A = (6 - ↑A.card) * (2 * (V 1 + V 2 + V 3 + V 4 + V 5) + V 6)

Complementation changes energy by a cardinality-dependent constant. This is the C12 instance of Bushaw--Cody--Leffler, Theorem 3.5 (2025 version).

theorem MusicTheory.ExtremalityConnections.diatonic_compl : AllPairsEvenness.Dᶜ = Fourier.tpose 6 AllPairsEvenness.P

theorem MusicTheory.ExtremalityConnections.pentatonic_orbit : Huddling.orbitT AllPairsEvenness.Dᶜ = AllPairsEvenness.orbitOf AllPairsEvenness.P

theorem MusicTheory.ExtremalityConnections.compl_mem_orbit_iff (A B : Finset (ZMod 12)) : Aᶜ ∈ Huddling.orbitT B ↔ A ∈ Huddling.orbitT Bᶜ

theorem MusicTheory.ExtremalityConnections.five_compl_card (A : Finset (ZMod 12)) (hA : A.card = 5) : Aᶜ.card = 7

theorem MusicTheory.ExtremalityConnections.pentatonic_norm_max (A : Finset (ZMod 12)) (hA : A.card = 5) : ‖Fourier.Ahat A 5‖ ≤ 2 + √3

The five-note spectral bound follows from the seven-note one without another census.

theorem MusicTheory.ExtremalityConnections.pentatonic_norm_unique (A : Finset (ZMod 12)) (hA : A.card = 5) : ‖Fourier.Ahat A 5‖ = 2 + √3 ↔ A ∈ AllPairsEvenness.orbitOf AllPairsEvenness.P

theorem MusicTheory.ExtremalityConnections.pentatonic_energy_gap (V : ℕ → ℝ) (A : Finset (ZMod 12)) (hA : A.card = 5) : AllPairsEvenness.E V A - AllPairsEvenness.E V AllPairsEvenness.P = AllPairsEvenness.E V Aᶜ - AllPairsEvenness.E V AllPairsEvenness.D

The five/seven-note energy gaps coincide, for every real potential.

theorem MusicTheory.ExtremalityConnections.pentatonic_energy_min (V : ℕ → ℝ) (hV : DiatonicExtremality.Admissible V) (A : Finset (ZMod 12)) (hA : A.card = 5) : AllPairsEvenness.E V AllPairsEvenness.P ≤ AllPairsEvenness.E V A

theorem MusicTheory.ExtremalityConnections.pentatonic_spectral_energy_equivalence (V : ℕ → ℝ) (hV : DiatonicExtremality.StrictAdmissible V) (A : Finset (ZMod 12)) (hA : A.card = 5) : ‖Fourier.Ahat A 5‖ = 2 + √3 ↔ AllPairsEvenness.E V AllPairsEvenness.P = AllPairsEvenness.E V A