Maximally even sets minimize every convex all-pairs energy #
For A ⊆ ℤ/12 and a potential V : ℕ → ℝ, the all-pairs energy is
E V A = ∑ k ∈ 1..6, iv A k * V k, with iv the interval vector. A double summation by parts
(abel_bridge) writes E V A - E V R as a combination of the second differences of V and of
V 5 - V 6 with coefficients the double cumulative sums DD of iv A - iv R. A finite
check over all subsets of a given size shows these coefficients are nonnegative, and positive off
the T/I-orbit of R. Hence, for every convex V decreasing at the top, the maximally even set
R minimizes the energy, uniquely up to T/I when the inequalities are strict, for the
pentatonic (k = 5), whole-tone (6), diatonic (7) and octatonic (8) collections.
Main results #
abel_bridge,abel_nonneg,abel_pos: the summation by parts and its sign.groundStateG,uniqueG: the reduction to the finite check.diatonic_ground_state,diatonic_uniqueand the pentatonic, whole-tone and octatonic versions.
Implementation notes #
The finite checks over the k-subsets of ℤ/12 are proved by decide in the kernel on a
bitmask encoding of the subsets (ofBits, exists_ofBits, iv_ofBits, census_iv); no
native_decide is used.
References #
- J. Douthett, R. Krantz, papers in J. Math. Phys. (1996, 1998) on one-dimensional Ising models with arbitrary-range convex interactions.
- 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 #
Interval vector entry at distance k (textbook convention): the number of UNORDERED pairs
{a,b} ⊆ A with circular distance k. Each unordered pair is counted twice in A ×ˢ A
(as (a,b) and (b,a), since cdist is symmetric), so we divide by 2.
Equations
- MusicTheory.AllPairsEvenness.iv A k = {p ∈ A ×ˢ A | MusicTheory.AllPairsEvenness.cdist p.1 p.2 = k}.card / 2
Instances For
Transposition Tₙ : a ↦ a + n.
Equations
- MusicTheory.AllPairsEvenness.tpose n A = Finset.map { toFun := fun (x : ZMod 12) => x + n, inj' := ⋯ } A
Instances For
Inversion I_j : a ↦ j − a (axis j/2).
Equations
- MusicTheory.AllPairsEvenness.inv j A = Finset.map { toFun := fun (x : ZMod 12) => j - x, inj' := ⋯ } A
Instances For
The T/I-orbit of the diatonic: all 12 transposes ∪ all inversions (= 12 distinct sets, the diatonic being inversionally symmetric).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Double-cumulative sum DD_j = Σ_{l≤j} (j+1−l)·d_l = Σ_{l≤j} Σ_{i≤l} d_i (single-sum closed
form of the double Abel cumulative).
Equations
- MusicTheory.AllPairsEvenness.DD d j = ∑ l ∈ Finset.range (j + 1), (↑j + 1 - ↑l) * d l
Instances For
All-pairs energy of A for a real potential V : ℕ → ℝ (distance → energy):
E V A = Σ_{k=1..6} iv A k · V k.
Equations
- MusicTheory.AllPairsEvenness.E V A = ∑ j ∈ Finset.range 6, ↑(MusicTheory.AllPairsEvenness.iv A (j + 1)) * V (j + 1)
Instances For
The Abel bridge (general, V-independent) #
Double summation-by-parts (the engine). For any d : ℕ → ℤ with d₀+⋯+d₅ = 0 and any
V : ℕ → ℝ,
Σ_{j<6} d_j·V(j+1) = Σ_{j<4} DD_j·(V(j+1) − 2V(j+2) + V(j+3)) + DD₄·(V 5 − V 6).
Both boundary terms of the first Abel pass vanish because ∑ d = 0; the residual DD₄·(V5−V6)
is the surviving (decreasing) boundary of the second pass. Pure algebra.
Nonnegativity (V-independent ≥). With DD_j ≥ 0 (j=0..4), the four second differences
≥ 0 (convexity) and V 6 ≤ V 5 (decreasing top), the energy gap is ≥ 0.
Strict positivity (V-independent >). Strictly convex (> 0 second differences), strictly
decreasing top (V 6 < V 5), DD_j ≥ 0, and SOME DD_j > 0 ⟹ strictly positive gap.
The finite censuses #
A census ranges over all k-subsets of ℤ/12. A subset is encoded by a bitmask m < 4096
(ofBits, onto by exists_ofBits); its interval vector is computed on the bits (ivN, equal to
iv (ofBits m) by iv_ofBits), and the resulting statement about the masks is checked by
decide in the kernel. Off the orbit, the masks of the orbit are listed explicitly and shown to
lie in it by decide.
The interval vector of ofBits m, computed on the bits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A statement about the interval vectors of all k-subsets follows from the same statement
about the bitmasks with k set bits.
Off-orbit version of census_iv: the masks for which the statement fails are listed in L,
and they encode members of orb.
dg R A as a function of the interval vector v of A.
Equations
- MusicTheory.AllPairsEvenness.dgv R v j = ↑(v (j + 1)) - ↑(MusicTheory.AllPairsEvenness.iv R (j + 1))
Instances For
E0 as a function of the interval vector.
Equations
- MusicTheory.AllPairsEvenness.E0v v = ∑ j ∈ Finset.range 6, v (j + 1) * (7 - (j + 1)) ^ 2
Instances For
The double-cumulative sums are nonnegative for EVERY 7-subset. (Census — the Abel engine.)
OFF the T/I-orbit of the diatonic, some double-cumulative sum is strictly positive. (Census — this is what makes the diatonic the UNIQUE minimizer.)
Item 1 — single-V uniqueness via finite census (anchor) #
The integer admissible potential V₀(k) = (7−k)² (strictly convex, decreasing: 36,25,16,9,4,1)
and its all-pairs energy over ℕ: E₀ A = Σ_{k=1..6} iv A k · (7−k)².
Equations
- MusicTheory.AllPairsEvenness.E0 A = ∑ j ∈ Finset.range 6, MusicTheory.AllPairsEvenness.iv A (j + 1) * (7 - (j + 1)) ^ 2
Instances For
E0 A = c exactly on an orbit, from the bitmask census off the orbit and a check on it.
Item 1a (anchor). Among all 7-subsets of ℤ/12, the all-pairs energy E₀ is ≥ 313.
(Census.)
Item 1b (anchor). The minimum 313 is attained EXACTLY on the 12 T/I-transposes of the
diatonic: E₀ A = 313 ⟺ A ∈ orbitTI. (Census.)
Item 3 — V-independent uniqueness at (7,12) (capstone) #
Item 3, the ≥ half (V-INDEPENDENT ground state). For EVERY decreasing-convex potential V,
the diatonic minimizes the all-pairs energy: E V D ≤ E V A for every 7-subset A. The single
inequality holds simultaneously for all admissible V — this is the V-independence.
Item 3, the capstone (V-INDEPENDENT UNIQUENESS). For EVERY STRICTLY convex, strictly
decreasing potential V, the diatonic is the UNIQUE all-pairs ground state: E V D = E V A
holds iff A is a transposition or inversion of the diatonic. One statement, all admissible
V at once — the headline of Douthett–Krantz maximal evenness.
Generic reference-set engine (k-independent) #
Integer interval-vector difference from an arbitrary reference set R:
dg R A j = iv A (j+1) − iv R (j+1). (The diatonic-specific dvec is dg D.)
Equations
- MusicTheory.AllPairsEvenness.dg R A j = ↑(MusicTheory.AllPairsEvenness.iv A (j + 1)) - ↑(MusicTheory.AllPairsEvenness.iv R (j + 1))
Instances For
Generic V-independent ground state. Given the ∑dg=0 and DD ≥ 0 censuses over a family
S, the reference R minimizes the all-pairs energy over S for every decreasing-convex V.
Generic V-independent uniqueness. Given the ∑dg=0, DD ≥ 0, off-orbit DD>0 and
on-orbit iv-agreement censuses, R is the unique all-pairs ground state over S for every
strictly convex, strictly decreasing V.
k = 5 — pentatonic {0,2,4,7,9} (orbit size 12) #
Single-V anchor: E₀ P = 132 and E₀ A = 132 ⟺ A ∈ orbit over all 5-subsets.
Pentatonic ground state (V-INDEPENDENT). For every decreasing-convex V, the pentatonic
minimizes the all-pairs energy over all 5-subsets of ℤ/12.
Pentatonic uniqueness (V-INDEPENDENT). For every strictly convex, strictly decreasing V,
the pentatonic is the unique all-pairs ground state up to T/I.
k = 8 — octatonic {0,1,3,4,6,7,9,10} (orbit size 3) #
Single-V anchor: E₀ O = 428 and E₀ A = 428 ⟺ A ∈ orbit over all 8-subsets.
Octatonic ground state (V-INDEPENDENT).
Octatonic uniqueness (V-INDEPENDENT).
k = 6 — whole-tone {0,2,4,6,8,10} (orbit size 2, degenerate IV with zeros) #
Single-V anchor: E₀ W = 207 and E₀ A = 207 ⟺ A ∈ orbit over all 6-subsets.
Whole-tone ground state (V-INDEPENDENT).
Whole-tone uniqueness (V-INDEPENDENT). Despite the degenerate IV (three zero classes), the
off-orbit census still yields a strictly positive double-cumulative, so strict uniqueness holds
for every strictly convex, strictly decreasing V.