Translation-invariant pair energies

On a finite abelian group G, a pair weight W a b = f (b - a) has constant row sum ∑ x, f x, and it is symmetric iff f is even. So the complement correction of ComplementEnergy is a single scalar. On ℤ/12 with a potential of the circular distance, a hexachord and its complement have the same energy for every potential, and complementation transports minimizers.

Main results

• kernel_symmetric_iff, rowSum_kernel, energy_univ.
• energy_compl, energy_compl_card, energy_gap_compl, minimizer_compl_iff.
• PitchClassEnergy.potential_sum, PitchClassEnergy.energy_compl_card, PitchClassEnergy.complement_difference_bridge, PitchClassEnergy.hexachord_energy_eq, PitchClassEnergy.minimizer_compl_iff.

References

• N. Bushaw, B. Cody, C. Leffler, Sets of vertices with extremal energy, arXiv:2407.18785.

def MusicTheory.TranslationInvariantEnergy.kernel {G : Type u_1} [AddCommGroup G] (f : G → ℝ) (a b : G) : ℝ

A pair potential determined only by the oriented difference of its sites.

Equations

• MusicTheory.TranslationInvariantEnergy.kernel f a b = f (b - a)

theorem MusicTheory.TranslationInvariantEnergy.kernel_symmetric {G : Type u_1} [AddCommGroup G] (f : G → ℝ) (heven : ∀ (x : G), f (-x) = f x) : ComplementEnergy.IsSymmetric (kernel f)

Evenness of the potential makes its pair kernel symmetric.

theorem MusicTheory.TranslationInvariantEnergy.kernel_symmetric_iff {G : Type u_1} [AddCommGroup G] (f : G → ℝ) : ComplementEnergy.IsSymmetric (kernel f) ↔ ∀ (x : G), f (-x) = f x

Symmetry of the pair energy is exactly evenness of its difference potential.

theorem MusicTheory.TranslationInvariantEnergy.rowSum_kernel {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℝ) (a : G) : ComplementEnergy.rowSum (kernel f) a = ∑ x : G, f x

Translation invariance gives the same weighted degree at every site.

theorem MusicTheory.TranslationInvariantEnergy.kernel_regular {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℝ) : ComplementEnergy.IsRegular (kernel f)

theorem MusicTheory.TranslationInvariantEnergy.energy_univ {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℝ) : ComplementEnergy.energy (kernel f) Finset.univ = (↑(Fintype.card G) * ∑ x : G, f x) / 2

The total energy is half the number of sites times their common row sum.

theorem MusicTheory.TranslationInvariantEnergy.energy_compl {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f : G → ℝ) (heven : ∀ (x : G), f (-x) = f x) (A : Finset G) : ComplementEnergy.energy (kernel f) Aᶜ - ComplementEnergy.energy (kernel f) A = ComplementEnergy.energy (kernel f) Finset.univ - ↑A.card * ∑ x : G, f x

The full complement correction is fixed by cardinality and the potential's total sum.

theorem MusicTheory.TranslationInvariantEnergy.energy_compl_card {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f : G → ℝ) (heven : ∀ (x : G), f (-x) = f x) (A : Finset G) : ComplementEnergy.energy (kernel f) Aᶜ - ComplementEnergy.energy (kernel f) A = (↑(Fintype.card G) / 2 - ↑A.card) * ∑ x : G, f x

Normal form: one scalar (the row sum) controls every complement correction.

theorem MusicTheory.TranslationInvariantEnergy.energy_gap_compl {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f : G → ℝ) (heven : ∀ (x : G), f (-x) = f x) (A B : Finset G) (hcard : A.card = B.card) : ComplementEnergy.energy (kernel f) Aᶜ - ComplementEnergy.energy (kernel f) Bᶜ = ComplementEnergy.energy (kernel f) A - ComplementEnergy.energy (kernel f) B

Equal-cardinality energy gaps are unchanged by complementation.

theorem MusicTheory.TranslationInvariantEnergy.minimizer_compl_iff {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f : G → ℝ) (heven : ∀ (x : G), f (-x) = f x) (A : Finset G) : ComplementEnergy.IsMinimizer (kernel f) Aᶜ ↔ ComplementEnergy.IsMinimizer (kernel f) A

Every cardinality-constrained minimizer is transported to its complement.

def MusicTheory.PitchClassEnergy.potential (V : ℕ → ℝ) (x : ZMod 12) : ℝ

The twelve-tone circular-distance potential viewed as a difference kernel.

Equations

• MusicTheory.PitchClassEnergy.potential V x = V (MusicTheory.AllPairsEvenness.cdist 0 x)

theorem MusicTheory.PitchClassEnergy.potential_even (V : ℕ → ℝ) (x : ZMod 12) : potential V (-x) = potential V x

theorem MusicTheory.PitchClassEnergy.kernel_eq_distance (V : ℕ → ℝ) (a b : ZMod 12) : TranslationInvariantEnergy.kernel (potential V) a b = V (AllPairsEvenness.cdist a b)

Every distance-based pair weight in the pitch-class circle is translation invariant.

theorem MusicTheory.PitchClassEnergy.potential_sum (V : ℕ → ℝ) : ∑ x : ZMod 12, potential V x = V 0 + 2 * (V 1 + V 2 + V 3 + V 4 + V 5) + V 6

The twelve sites occur at circular distances 0, 1, ..., 6 with multiplicities 1, 2, ..., 2, 1.

theorem MusicTheory.PitchClassEnergy.energy_compl_card (V : ℕ → ℝ) (A : Finset (ZMod 12)) : ComplementEnergy.energy (fun (a b : ZMod 12) => V (AllPairsEvenness.cdist a b)) Aᶜ - ComplementEnergy.energy (fun (a b : ZMod 12) => V (AllPairsEvenness.cdist a b)) A = (6 - ↑A.card) * ∑ x : ZMod 12, potential V x

Twelve-tone specialization of the general complement identity. The scalar is the sum of all twelve distance weights, including the possible self-weight V(0).

theorem MusicTheory.PitchClassEnergy.complement_difference_bridge (V : ℕ → ℝ) (hzero : V 0 = 0) (A : Finset (ZMod 12)) : AllPairsEvenness.E V Aᶜ - AllPairsEvenness.E V A = ComplementEnergy.energy (fun (a b : ZMod 12) => V (AllPairsEvenness.cdist a b)) Aᶜ - ComplementEnergy.energy (fun (a b : ZMod 12) => V (AllPairsEvenness.cdist a b)) A

The abstract and pitch-class complement differences coincide when the diagonal weight vanishes, which is the convention used by AllPairsEvenness.E.

theorem MusicTheory.PitchClassEnergy.hexachord_energy_eq (V : ℕ → ℝ) (A : Finset (ZMod 12)) (hcard : A.card = 6) : ComplementEnergy.energy (fun (a b : ZMod 12) => V (AllPairsEvenness.cdist a b)) Aᶜ = ComplementEnergy.energy (fun (a b : ZMod 12) => V (AllPairsEvenness.cdist a b)) A

Any six-note set and its complement have equal pair energy for every circular-distance potential. This is the weighted-energy face of the complementary-hexachord interval-vector theorem.

theorem MusicTheory.PitchClassEnergy.minimizer_compl_iff (V : ℕ → ℝ) (A : Finset (ZMod 12)) : ComplementEnergy.IsMinimizer (fun (a b : ZMod 12) => V (AllPairsEvenness.cdist a b)) Aᶜ ↔ ComplementEnergy.IsMinimizer (fun (a b : ZMod 12) => V (AllPairsEvenness.cdist a b)) A

Complementation transports minima for every circular-distance potential, with no convexity assumption. This is the abstract source of the 5↔7 bridge.