The step-gap energy and balanced gap configurations

A gap configuration of k parts of n is g : Fin k → ℕ with 1 ≤ g i and ∑ g i = n; it is balanced when its maximum and minimum differ by at most one. For a strictly convex potential V on [0, ∞), the gap energy ∑ V (g i) is minimized exactly by the balanced configurations. This energy depends only on the multiset of gaps, so being balanced is necessary but not sufficient for maximal evenness; the all-pairs energy of AllPairsEvenness singles out the maximally even sets.

Main results

• swap_lt, exists_improve: an unbalanced configuration can be improved.
• balanced_energy_eq: balanced configurations have equal energy.
• isMinimizer_iff_balanced: global minimizer iff balanced.
• diatonic_balanced: the diatonic gap word (2, 2, 1, 2, 2, 2, 1) is balanced.

References

• P. Bak, R. Bruinsma, One-dimensional Ising model and the complete devil's staircase, Phys. Rev. Lett. 49 (1982).
• J. Clough, J. Douthett, Maximally even sets, J. Music Theory 35 (1991).
• J. Douthett, R. Krantz, Maximally even sets and configurations: common threads in mathematics, physics, and music, J. Comb. Optim. 14 (2007).
• C. Marín, One transform and one duality: a machine-checked core of music theory in Lean 4, Zenodo (2026), doi:10.5281/zenodo.20953767.

Definitions

def MusicTheory.MaximalEvenness.Balanced {k : ℕ} (g : Fin k → ℕ) : Prop

A gap configuration is Balanced when max − min ≤ 1: every gap differs from every other by at most one. This is exactly the maximally-even structure (all gaps ⌊n/k⌋ or ⌈n/k⌉).

Equations

• MusicTheory.MaximalEvenness.Balanced g = ∀ (i j : Fin k), g i ≤ g j + 1

noncomputable def MusicTheory.MaximalEvenness.energy {k : ℕ} (V : ℝ → ℝ) (g : Fin k → ℕ) : ℝ

The energy of a configuration for a potential V, casting gaps to ℝ.

Equations

• MusicTheory.MaximalEvenness.energy V g = ∑ i : Fin k, V ↑(g i)

Part 1 — the swap lemma (strict convexity)

theorem MusicTheory.MaximalEvenness.swap_lt {V : ℝ → ℝ} {s : Set ℝ} (hV : StrictConvexOn ℝ s V) {a b : ℝ} (ha : a ∈ s) (hb : b ∈ s) (hab : b + 2 ≤ a) : V (a - 1) + V (b + 1) < V a + V b

Swap lemma. For V strictly convex on s and endpoints a, b ∈ s with b + 2 ≤ a, pulling the two gaps one step together strictly lowers the pair energy: V (a-1) + V (b+1) < V a + V b. Proof: write a-1 and b+1 as strict convex combinations of the endpoints a, b, apply binary strict Jensen to each, and add — the endpoint coefficients each total 1.

Part 2 — minimality (the payoff)

theorem MusicTheory.MaximalEvenness.sum_split_two {k : ℕ} {M : Type u_1} [AddCommMonoid M] (F : Fin k → M) {i j : Fin k} (hij : i ≠ j) : ∑ x : Fin k, F x = F i + F j + ∑ x ∈ (Finset.univ.erase i).erase j, F x

A two-index split of a Finset.univ sum: pull out the values at two distinct indices i, j.

theorem MusicTheory.MaximalEvenness.exists_improve {k n : ℕ} {V : ℝ → ℝ} (hV : StrictConvexOn ℝ (Set.Ici 0) V) (g : Fin k → ℕ) (hpos : ∀ (i : Fin k), 1 ≤ g i) (hsum : ∑ i : Fin k, g i = n) (hnb : ¬Balanced g) : ∃ (g' : Fin k → ℕ), (∀ (i : Fin k), 1 ≤ g' i) ∧ ∑ i : Fin k, g' i = n ∧ energy V g' < energy V g

Improvement step. If a valid configuration is not Balanced, one swap of an unbalanced pair gives another valid configuration with the same sum and strictly smaller energy.

theorem MusicTheory.MaximalEvenness.minimizer_balanced {k n : ℕ} {V : ℝ → ℝ} (hV : StrictConvexOn ℝ (Set.Ici 0) V) (g : Fin k → ℕ) (hpos : ∀ (i : Fin k), 1 ≤ g i) (hsum : ∑ i : Fin k, g i = n) (hmin : ∀ (g' : Fin k → ℕ), (∀ (i : Fin k), 1 ≤ g' i) → ∑ i : Fin k, g' i = n → energy V g ≤ energy V g') : Balanced g

ME characterization. Any configuration that minimizes the (strictly convex) energy over all valid configurations of the same sum is Balanced — i.e. maximally even.

Part 3 — the converse: every Balanced config is a global energy minimizer

theorem MusicTheory.MaximalEvenness.balanced_energy_closed {k n : ℕ} (V : ℝ → ℝ) (g : Fin k → ℕ) (hpos : ∀ (i : Fin k), 1 ≤ g i) (hsum : ∑ i : Fin k, g i = n) (hbal : Balanced g) : energy V g = ↑(n % k) * V (↑(n / k) + 1) + ↑(k - n % k) * V ↑(n / k)

Closed form of the energy of ANY balanced valid config: it depends only on (k, n, V). Writing m = ⌊n/k⌋ and r = n % k, exactly r gaps equal m+1 and k − r equal m, so energy V g = r · V(m+1) + (k−r) · V(m). (Counting identity; no convexity needed.)

theorem MusicTheory.MaximalEvenness.balanced_energy_eq {k n : ℕ} (V : ℝ → ℝ) (g g' : Fin k → ℕ) (hpos : ∀ (i : Fin k), 1 ≤ g i) (hsum : ∑ i : Fin k, g i = n) (hbal : Balanced g) (hpos' : ∀ (i : Fin k), 1 ≤ g' i) (hsum' : ∑ i : Fin k, g' i = n) (hbal' : Balanced g') : energy V g = energy V g'

Balanced configs all have the same energy. Any two balanced valid configs of the same (k, n) have equal energy for any V (they are permutations of each other).

def MusicTheory.MaximalEvenness.phi {k : ℕ} (g : Fin k → ℕ) : ℕ

Termination measure for the swap descent: Φ g = ∑ (g i)², a strictly-decreasing ℕ-valued well-founded measure under any balancing swap (independent of V).

Equations

• MusicTheory.MaximalEvenness.phi g = ∑ i : Fin k, g i ^ 2

theorem MusicTheory.MaximalEvenness.exists_improve_phi {k n : ℕ} {V : ℝ → ℝ} (hV : StrictConvexOn ℝ (Set.Ici 0) V) (g : Fin k → ℕ) (hpos : ∀ (i : Fin k), 1 ≤ g i) (hsum : ∑ i : Fin k, g i = n) (hnb : ¬Balanced g) : ∃ (g' : Fin k → ℕ), (∀ (i : Fin k), 1 ≤ g' i) ∧ ∑ i : Fin k, g' i = n ∧ energy V g' < energy V g ∧ phi g' < phi g

Improvement step with the Φ measure. Same single swap as exists_improve, additionally certifying that the termination measure Φ strictly drops (Δ = 2(b−a)+2 ≤ −2).

theorem MusicTheory.MaximalEvenness.balanced_isMinimizer {k n : ℕ} {V : ℝ → ℝ} (hV : StrictConvexOn ℝ (Set.Ici 0) V) (g : Fin k → ℕ) (hgpos : ∀ (i : Fin k), 1 ≤ g i) (hgsum : ∑ i : Fin k, g i = n) (hgbal : Balanced g) (g' : Fin k → ℕ) : (∀ (i : Fin k), 1 ≤ g' i) → ∑ i : Fin k, g' i = n → energy V g ≤ energy V g'

The converse (target). For strictly convex V, any Balanced valid config is a GLOBAL energy minimizer over all valid configs of the same sum. Proof: well-founded descent on Φ = ∑ (g i)² — a non-balanced config strictly improves (lower energy AND lower Φ) via exists_improve_phi, and a balanced config matches g's energy via balanced_energy_eq.

theorem MusicTheory.MaximalEvenness.isMinimizer_iff_balanced {k n : ℕ} {V : ℝ → ℝ} (hV : StrictConvexOn ℝ (Set.Ici 0) V) (g : Fin k → ℕ) (hpos : ∀ (i : Fin k), 1 ≤ g i) (hsum : ∑ i : Fin k, g i = n) : (∀ (g' : Fin k → ℕ), (∀ (i : Fin k), 1 ≤ g' i) → ∑ i : Fin k, g' i = n → energy V g ≤ energy V g') ↔ Balanced g

Ground-state characterization of maximal evenness (full iff). For strictly convex V, a valid config g is a global energy minimizer over all valid configs of the same sum iff it is Balanced (maximally even). Combines minimizer_balanced (⇒) and balanced_isMinimizer (⇐).

Part 4 — concrete music instance: the diatonic scale

def MusicTheory.MaximalEvenness.diatonicGaps : Fin 7 → ℕ

The circular gap word of the diatonic scale {0,2,4,5,7,9,11} ⊂ ℤ/12: (2,2,1,2,2,2,1) (k = 7 gaps summing to n = 12).

Equations

• MusicTheory.MaximalEvenness.diatonicGaps = ![2, 2, 1, 2, 2, 2, 1]

theorem MusicTheory.MaximalEvenness.diatonic_pos (i : Fin 7) : 1 ≤ diatonicGaps i

Every diatonic gap is positive.

theorem MusicTheory.MaximalEvenness.diatonic_sum : ∑ i : Fin 7, diatonicGaps i = 12

The diatonic gaps sum to the octave, n = 12.

theorem MusicTheory.MaximalEvenness.diatonic_balanced : Balanced diatonicGaps

The diatonic scale is maximally even: its gap word (2,2,1,2,2,2,1) is Balanced (max − min = 2 − 1 = 1).

theorem MusicTheory.MaximalEvenness.strictConvexOn_sq : StrictConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x ^ 2

Strict convexity of x ↦ x² on [0,∞) (the canonical repulsive potential).

theorem MusicTheory.MaximalEvenness.sq_minimizer_balanced {k n : ℕ} (g : Fin k → ℕ) (hpos : ∀ (i : Fin k), 1 ≤ g i) (hsum : ∑ i : Fin k, g i = n) (hmin : ∀ (g' : Fin k → ℕ), (∀ (i : Fin k), 1 ≤ g' i) → ∑ i : Fin k, g' i = n → energy (fun (x : ℝ) => x ^ 2) g ≤ energy (fun (x : ℝ) => x ^ 2) g') : Balanced g

Concrete corollary. For the quadratic energy E g = ∑ (g i)², any minimizer over valid configs of a fixed sum is Balanced (maximally even). Specializing the convex minimizer_balanced.

theorem MusicTheory.MaximalEvenness.diatonic_sq_isMinimizer (g' : Fin 7 → ℕ) : (∀ (i : Fin 7), 1 ≤ g' i) → ∑ i : Fin 7, g' i = 12 → energy (fun (x : ℝ) => x ^ 2) diatonicGaps ≤ energy (fun (x : ℝ) => x ^ 2) g'

The diatonic gap word is a global minimizer of ∑ gaps². Concrete instance of the converse: the diatonic (2,2,1,2,2,2,1) minimizes the quadratic energy over every valid 7-gap config summing to 12 — the full ground-state statement of its maximal evenness.

theorem MusicTheory.MaximalEvenness.diatonic_sq_iff : (∀ (g' : Fin 7 → ℕ), (∀ (i : Fin 7), 1 ≤ g' i) → ∑ i : Fin 7, g' i = 12 → energy (fun (x : ℝ) => x ^ 2) diatonicGaps ≤ energy (fun (x : ℝ) => x ^ 2) g') ↔ Balanced diatonicGaps

Full iff at the diatonic. Specializing the ground-state characterization to V = x², 7-of-12.