Myhill's property and well-formedness of the diatonic scale

A scale has Myhill's property when every nonzero generic interval comes in exactly two specific sizes. The diatonic scale {0, 2, 4, 5, 7, 9, 11} has it; the whole-tone scale is maximally even but every generic interval has one size. The diatonic and pentatonic scales are generated by the fifth and are well formed (two step sizes); the three-gap theorem is checked in ℤ/12.

Main results

• diatonic_hasMyhill, wholeTone_not_hasMyhill.
• diatonic_isMaxEven, wholeTone_isMaxEven.
• diatonic_generated_by_fifth, pentatonic_generated_by_fifth.
• threeGap_chromatic, diatonic_isWellFormed, pentatonic_isWellFormed, sixFifths_not_wellFormed.

The general theorem (Myhill's property iff non-degenerate well-formed) is not formalized.

References

• J. Clough, G. Myerson, Variety and multiplicity in diatonic systems, J. Music Theory 29 (1985).
• N. Carey, D. Clampitt, Aspects of well-formed scales, Music Theory Spectrum 11 (1989).
• F. C. Harasim, S. E. Schmidt, M. Rohrmeier, Axiomatic scale theory, J. Math. Music (2020).
• 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.DiatonicScale.specSize {n : ℕ} (s : Fin n → ZMod 12) (k i : Fin n) : ZMod 12

The specific size of the generic interval k measured at scale degree i: the circular semitone gap s(i+k) − s(i) in ℤ/12 (index i+k taken mod n, the cyclic scale order).

Equations

• MusicTheory.DiatonicScale.specSize s k i = s (i + k) - s i

def MusicTheory.DiatonicScale.genericSpectrum {n : ℕ} (s : Fin n → ZMod 12) (k : Fin n) : Finset (ZMod 12)

The spectrum of a generic interval k: the set of specific sizes it takes across all degrees.

Equations

• MusicTheory.DiatonicScale.genericSpectrum s k = Finset.image (MusicTheory.DiatonicScale.specSize s k) Finset.univ

def MusicTheory.DiatonicScale.HasMyhill {n : ℕ} [NeZero n] (s : Fin n → ZMod 12) : Prop

Myhill's property. Every nonzero generic interval has exactly two distinct specific sizes. (= 2 is MP; ≤ 2 would be maximal evenness — a strictly weaker property.)

Equations

• MusicTheory.DiatonicScale.HasMyhill s = ∀ (k : Fin n), k ≠ 0 → (MusicTheory.DiatonicScale.genericSpectrum s k).card = 2

def MusicTheory.DiatonicScale.diatonic : Fin 7 → ZMod 12

The diatonic scale (C major) as the cyclically ordered 7-tuple of pitch classes.

Equations

• MusicTheory.DiatonicScale.diatonic = ![0, 2, 4, 5, 7, 9, 11]

def MusicTheory.DiatonicScale.wholeTone : Fin 6 → ZMod 12

The whole-tone scale: maximally even but degenerate (generator 2, gcd(2,12)=2).

Equations

• MusicTheory.DiatonicScale.wholeTone = ![0, 2, 4, 6, 8, 10]

theorem MusicTheory.DiatonicScale.diatonic_hasMyhill : HasMyhill diatonic

The diatonic scale has Myhill's property (Carey–Clampitt 1989).

theorem MusicTheory.DiatonicScale.wholeTone_not_hasMyhill : ¬HasMyhill wholeTone

The whole-tone scale does not have MP: every generic interval has a single specific size (it is maximally even but degenerate). This separates MP from ME.

Maximal evenness (Clough–Douthett), and how it differs from Myhill

def MusicTheory.DiatonicScale.specSizesNat {n : ℕ} (s : Fin n → ZMod 12) (k : Fin n) : Finset ℕ

Specific sizes of generic interval k as integers 0…11 (lifted from ZMod 12 by val), so "consecutive" is honest integer adjacency (no modular wrap ambiguity).

Equations

• MusicTheory.DiatonicScale.specSizesNat s k = Finset.image ZMod.val (MusicTheory.DiatonicScale.genericSpectrum s k)

def MusicTheory.DiatonicScale.IsMaxEven {n : ℕ} [NeZero n] (s : Fin n → ZMod 12) : Prop

Maximal evenness. Every nonzero generic interval takes at most two specific sizes, and those are consecutive integers. Strictly weaker than Myhill (which demands exactly two): a maximally even scale may have a generic interval of a single size — that is the ME∖MP gap.

Equations

• One or more equations did not get rendered due to their size.

theorem MusicTheory.DiatonicScale.diatonic_isMaxEven : IsMaxEven diatonic

The diatonic scale is maximally even (Clough–Douthett). It is therefore in the ME ∩ MP intersection (diatonic_hasMyhill + this) — the source of its specialness.

theorem MusicTheory.DiatonicScale.wholeTone_isMaxEven : IsMaxEven wholeTone

The whole-tone scale is maximally even — yet wholeTone_not_hasMyhill shows it is not Myhill. Together they witness ME ⊋ MP as a theorem (whole-tone ∈ ME ∖ MP).

Generated scales: well-formedness's generator side (Carey–Clampitt)

A scale is well-formed when generated by a single interval. We record the canonical generator instances over ℤ/12 as decidable set equalities.

def MusicTheory.DiatonicScale.stack (start g : ZMod 12) (d : ℕ) : Finset (ZMod 12)

The pitch-class set of d consecutive copies of the generator g starting at start: {start, start+g, …, start+(d−1)g}. The starting point selects the KEY/mode; the set is the generated scale. Defined as a filter over univ (not image) so equalities reduce under decide.

Equations

• MusicTheory.DiatonicScale.stack start g d = {x : ZMod 12 | ∃ (k : Fin d), start + g * ↑↑k = x}

theorem MusicTheory.DiatonicScale.diatonic_generated_by_fifth : stack 5 7 7 = {0, 2, 4, 5, 7, 9, 11}

The diatonic scale is generated by the perfect fifth — seven CONSECUTIVE fifths (F C G D A E B, i.e. starting at the subdominant 5) give exactly C major {0,2,4,5,7,9,11}. The generator characterization at the heart of well-formedness (Carey–Clampitt).

theorem MusicTheory.DiatonicScale.diatonic_range_eq_stack : Finset.image diatonic Finset.univ = stack 5 7 7

The pitch-class set of the diatonic tuple is exactly that stack of seven fifths.

theorem MusicTheory.DiatonicScale.stack_fifths_from_zero : stack 0 7 7 = {0, 2, 4, 6, 7, 9, 11}

Stacking fifths from a different start just transposes: from 0 the seven fifths give G major {0,2,4,6,7,9,11} — same set class, different key.

theorem MusicTheory.DiatonicScale.pentatonic_generated_by_fifth : stack 0 7 5 = {0, 2, 4, 7, 9}

The major pentatonic is generated by the fifth too (five stacked fifths from 0): {0,2,4,7,9}.

The three-gap (Steinhaus) theorem, discrete ℤ/12 form

The three-gap theorem (Steinhaus, conjectured 1950s; proved by Sós, Świerczkowski, Surányi): for points {0, g, 2g, …, (d−1)g} on a circle, the gaps between cyclically adjacent points take at most three distinct sizes. We formalize its discrete incarnation on the fixed chromatic circle ℤ/12, where the statement becomes DECIDABLE — no continued-fraction machinery is needed because the universe is finite. A general (continuous) version exists in Coq (Mayero et al.). The music-theoretic reading: a GENERATED scale has ≤ 3 step sizes, and is well-formed exactly when it has 2 step sizes (Carey–Clampitt 1989; Clough–Myerson 1985).

The general equivalence of Myhill's property and well-formedness is not formalized here.

def MusicTheory.DiatonicScale.succGap (S : Finset (ZMod 12)) (x : ZMod 12) : ℕ

The cyclic successor gap of a pitch-class set S at x: the smallest positive δ ∈ 1…12 with x + δ ∈ S (the semitone distance from x to the next note of S going up the circle). Defined by a bounded List.find? search so it reduces under decide. If S is empty above x in 1…12 it returns 12 (a full octave); for nonempty S containing x, δ ≤ 12 always hits.

Equations

• MusicTheory.DiatonicScale.succGap S x = (List.find? (fun (δ : ℕ) => decide (x + ↑(δ + 1) ∈ S)) (List.range 12)).getD 11 + 1

def MusicTheory.DiatonicScale.stepSizes (S : Finset (ZMod 12)) : Finset ℕ

The step sizes (adjacent gaps) of a pitch-class set: the set of successor gaps over its notes. For a scale, these are the semitone sizes of its consecutive steps (e.g. diatonic = whole & half).

Equations

• MusicTheory.DiatonicScale.stepSizes S = Finset.image (MusicTheory.DiatonicScale.succGap S) S

theorem MusicTheory.DiatonicScale.threeGap_chromatic (g : ZMod 12) (d : ℕ) : d ≤ 12 → (stepSizes (stack 0 g d)).card ≤ 3

The three-gap theorem on the chromatic circle. For EVERY generator g : ZMod 12 and EVERY count d ≤ 12, the generated set {0, g, 2g, …, (d−1)g} has at most three distinct step sizes. Proved by exhausting d (interval_cases) and deciding the finite ∀ g. Full ∀-scope: no narrowing — all 12 generators, all 13 values d = 0…12.

def MusicTheory.DiatonicScale.IsWellFormed (S : Finset (ZMod 12)) : Prop

Two-step-size property (MOS), the floor of the three-gap bound. A pitch-class set has exactly two step sizes — Wilson's "moment of symmetry". ⚠ For a single-generator (GENERATED) scale this is exactly Carey–Clampitt well-formedness, which is how we use it below (every witness is a stack). As a bare set predicate it is STRICTLY BROADER than well-formed: e.g. the octatonic {0,1,3,4,6,7,9,10} has two step sizes {1,2} yet is not single-generated (ℤ/12 has no order-8 element) — MOS but not WF. Do not read IsWellFormed S as "S is well-formed" for arbitrary S; read it as "S is MOS".

Equations

• MusicTheory.DiatonicScale.IsWellFormed S = ((MusicTheory.DiatonicScale.stepSizes S).card = 2)

theorem MusicTheory.DiatonicScale.diatonic_isWellFormed : IsWellFormed (stack 5 7 7)

The diatonic scale (seven fifths) is well-formed: exactly two step sizes, {1, 2} — the semitone and the whole tone. (The three-gap bound is attained at its floor: 2 < 3.)

theorem MusicTheory.DiatonicScale.diatonic_stepSizes : stepSizes (stack 5 7 7) = {1, 2}

The diatonic step sizes are precisely {1, 2} (half step and whole step).

theorem MusicTheory.DiatonicScale.pentatonic_isWellFormed : IsWellFormed (stack 0 7 5)

The major pentatonic (five fifths) is well-formed too: two step sizes {2, 3} — the whole tone and the minor third.

theorem MusicTheory.DiatonicScale.pentatonic_stepSizes : stepSizes (stack 0 7 5) = {2, 3}

Pentatonic step sizes are precisely {2, 3}.

theorem MusicTheory.DiatonicScale.sixFifths_stepSizes : stepSizes (stack 0 7 6) = {1, 2, 3}

The load-bearing witness that "3" is achieved. Six stacked fifths {0,2,4,7,9,11} give a scale with exactly three step sizes {1, 2, 3} — the three-gap bound is SATURATED, and the scale is NOT well-formed. This is the proper-third-gap case the theorem's ≤ 3 allows.

theorem MusicTheory.DiatonicScale.sixFifths_not_wellFormed : ¬IsWellFormed (stack 0 7 6)

Six fifths: three step sizes, and therefore NOT well-formed (card = 3 ≠ 2).

theorem MusicTheory.DiatonicScale.sixFourths_stepSizes : stepSizes (stack 0 5 6) = {1, 2, 3}

A second saturating witness via a different generator: six stacked perfect FOURTHS (g = 5) {0,1,3,5,8,10} also hit exactly three step sizes {1, 2, 3}. Confirms the bound's saturation is not an artifact of the fifth.

theorem MusicTheory.DiatonicScale.sixFourths_not_wellFormed : ¬IsWellFormed (stack 0 5 6)

Six fourths: not well-formed either (three step sizes).