The interval vector of a pitch-class set

For a pitch-class set A ⊆ ℤ/12, IVraw A k counts the ordered pairs (a, b) ∈ A × A whose interval class min (a - b).val (b - a).val is k; the textbook interval vector is IVraw A k / 2. The interval class is written so that invariance under negation is min_comm; invariance is proved once for every embedding of ℤ/12 preserving differences up to sign, and transposition and inversion are special cases.

Main results

• IVraw_map: invariance under a difference-class-preserving embedding.
• IVraw_tpose, IVraw_invert: the interval vector is invariant under transposition and inversion.

References

• 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.

def MusicTheory.IntervalVector.ivc (d : ZMod 12) : ℕ

Interval class of a pitch-class difference: min(d, 12−d), value in 0..6. Written as min d.val (-d).val so that neg-invariance is just min_comm.

Equations

• MusicTheory.IntervalVector.ivc d = min d.val (-d).val

@[simp]

theorem MusicTheory.IntervalVector.ivc_neg (d : ZMod 12) : ivc (-d) = ivc d

def MusicTheory.IntervalVector.IVraw (A : Finset (ZMod 12)) (k : ℕ) : ℕ

Raw interval vector: number of ORDERED pairs (a,b) ∈ A×A with interval class k. The textbook interval vector is IVraw A k / 2 for k = 1..6 (each unordered pair twice).

Equations

• MusicTheory.IntervalVector.IVraw A k = ∑ a ∈ A, ∑ b ∈ A, if MusicTheory.IntervalVector.ivc (a - b) = k then 1 else 0

theorem MusicTheory.IntervalVector.IVraw_map (e : ZMod 12 ↪ ZMod 12) (he : ∀ (a b : ZMod 12), ivc (e a - e b) = ivc (a - b)) (A : Finset (ZMod 12)) (k : ℕ) : IVraw (Finset.map e A) k = IVraw A k

Invariance under any embedding of ℤ/12 that preserves the interval class of differences.

def MusicTheory.IntervalVector.tpose (n : ZMod 12) (A : Finset (ZMod 12)) : Finset (ZMod 12)

Transposition Tₙ : a ↦ a + n.

Equations

• MusicTheory.IntervalVector.tpose n A = Finset.map { toFun := fun (x : ZMod 12) => x + n, inj' := ⋯ } A

def MusicTheory.IntervalVector.invert (A : Finset (ZMod 12)) : Finset (ZMod 12)

Inversion I : a ↦ −a.

Equations

• MusicTheory.IntervalVector.invert A = Finset.map { toFun := fun (x : ZMod 12) => -x, inj' := MusicTheory.IntervalVector.invert._proof_1 } A

theorem MusicTheory.IntervalVector.IVraw_tpose (n : ZMod 12) (A : Finset (ZMod 12)) (k : ℕ) : IVraw (tpose n A) k = IVraw A k

The interval vector is invariant under transposition.

theorem MusicTheory.IntervalVector.IVraw_invert (A : Finset (ZMod 12)) (k : ℕ) : IVraw (invert A) k = IVraw A k

The interval vector is invariant under inversion.