Babbitt's common-tone theorem and the generalised hexachord theorem over ℤ_n

For S ⊆ ℤ_n, the tones common to S and its transposition S + k number the k-th entry of the interval class vector for 2k < n, and twice it at the tritone 2k = n (Babbitt). For every n and every S with |S| = s, the interval class vectors of S and its complement differ by exactly n − 2s in every entry 2i < n and by n/2 − s at the tritone (the generalised hexachord theorem, with signs and for odd n too). Proof: the n ordered pairs (a, a + d) split into pairs inside S, inside the complement and across.

Main results

• Hexachord.card_inter_image_add: Babbitt: |S ∩ (S + k)| = icv_k (2k < n), = 2 icv_k (2k = n)
• Hexachord.icv_compl: generalised hexachord theorem with signs, every n
• Hexachord.babbitt_and_hexachord: both (Theorem of the Day)

References

• R. Whitty, Theorem of the Day, «Milton Babbitt's Theorem» (MusicAndArt/Babbitt) and «The Generalised Hexachord Theorem» (MusicAndArt/Hexachord).
• M. Babbitt, D. Lewin (1950s); E. Amiot, A. Fourier-proof of the hexachord theorem (2006).

def Hexachord.icv {n : ℕ} (S : Finset (ZMod n)) (i : ℕ) : ℕ

The i-th entry of the interval class vector of S ⊆ ℤ_n: the number of pairs a < b in S (by value in {0, …, n−1}) with min (b − a) (n − (b − a)) = i.

Equations

• Hexachord.icv S i = {p ∈ S ×ˢ S | p.1.val < p.2.val ∧ min (p.2.val - p.1.val) (n - (p.2.val - p.1.val)) = i}.card

def Hexachord.N {n : ℕ} [NeZero n] (S : Finset (ZMod n)) (d : ZMod n) : ℕ

Number of ordered pairs (a, a + d) with both entries in S.

Equations

• Hexachord.N S d = {a : ZMod n | a ∈ S ∧ a + d ∈ S}.card

theorem Hexachord.card_inter_image_eq_N {n : ℕ} [NeZero n] (S : Finset (ZMod n)) (d : ZMod n) : (S ∩ Finset.image (fun (x : ZMod n) => x + d) S).card = N S d

theorem Hexachord.N_compl {n : ℕ} [NeZero n] (S : Finset (ZMod n)) (d : ZMod n) : ↑(N Sᶜ d) = ↑(N S d) + ↑n - 2 * ↑S.card

theorem Hexachord.val_add_lt {n : ℕ} [NeZero n] (a : ZMod n) {k : ℕ} (hk : k < n) (h : a.val + k < n) : (a + ↑k).val = a.val + k

theorem Hexachord.val_add_ge {n : ℕ} [NeZero n] (a : ZMod n) {k : ℕ} (hk : k < n) (h : n ≤ a.val + k) : (a + ↑k).val = a.val + k - n

theorem Hexachord.icv_eq_N {n : ℕ} [NeZero n] (S : Finset (ZMod n)) {k : ℕ} (hk1 : 1 ≤ k) (hk : 2 * k < n) : icv S k = N S ↑k

Non-tritone case: icv S k counts the ordered pairs (a, a + k) in S.

theorem Hexachord.N_eq_two_icv {n : ℕ} [NeZero n] (S : Finset (ZMod n)) {k : ℕ} (hk1 : 1 ≤ k) (hk : 2 * k = n) : N S ↑k = 2 * icv S k

Tritone case: every unordered pair gives two ordered pairs.

theorem Hexachord.card_inter_image_add {n : ℕ} [NeZero n] (S : Finset (ZMod n)) : (∀ (k : ℕ), 1 ≤ k → 2 * k < n → (S ∩ Finset.image (fun (x : ZMod n) => x + ↑k) S).card = icv S k) ∧ ∀ (k : ℕ), 1 ≤ k → 2 * k = n → (S ∩ Finset.image (fun (x : ZMod n) => x + ↑k) S).card = 2 * icv S k

Babbitt's common-tone theorem, both parts.

theorem Hexachord.icv_compl {n : ℕ} [NeZero n] (S : Finset (ZMod n)) : (∀ (i : ℕ), 1 ≤ i → 2 * i < n → ↑(icv Sᶜ i) = ↑(icv S i) + (↑n - 2 * ↑S.card)) ∧ ∀ (i : ℕ), 1 ≤ i → 2 * i = n → ↑(icv Sᶜ i) = ↑(icv S i) + (↑i - ↑S.card)

Generalised hexachord theorem (with signs, every n), both parts.

theorem Hexachord.babbitt_and_hexachord (n : ℕ) [NeZero n] (S : Finset (ZMod n)) : (∀ (k : ℕ), 1 ≤ k → 2 * k < n → (S ∩ Finset.image (fun (x : ZMod n) => x + ↑k) S).card = icv S k) ∧ (∀ (k : ℕ), 1 ≤ k → 2 * k = n → (S ∩ Finset.image (fun (x : ZMod n) => x + ↑k) S).card = 2 * icv S k) ∧ (∀ (i : ℕ), 1 ≤ i → 2 * i < n → ↑(icv Sᶜ i) = ↑(icv S i) + (↑n - 2 * ↑S.card)) ∧ ∀ (i : ℕ), 1 ≤ i → 2 * i = n → ↑(icv Sᶜ i) = ↑(icv S i) + (↑i - ↑S.card)