Documentation

Formalizations.MusicTheory.CircleOfFifths

The circle of fifths closes in ℤ/12 #

The reduction red : ℤ × ℤ → ℤ/12 sends a 3-limit interval to its pitch class: the octave goes to 0, the fifth to 7 and the Pythagorean comma to 0. So twelve fifths return to the starting pitch class, and the fifths generate all of ℤ/12. In the 5-limit, four fifths reduce to a major third.

Main results #

References #

source
def MusicTheory.CircleOfFifths.red (m : ℤ × ℤ) :
ZMod 12

The 12-EDO reduction. A just-intonation monzo 2^a·3^b ↦ its pitch class in ℤ/12, i.e. the val's step count taken mod 12. Concretely red (a,b) = (12a + 19b : ℤ/12) = 7·b (since 12 ≡ 0, 19 ≡ 7). This is the homomorphism that maps the JI lattice onto the chromatic circle.

Equations
Instances For
    source
    theorem MusicTheory.CircleOfFifths.red_oct :
    red Temperament.oct = 0

    The octave is the pitch-class unison: red oct = 0 (octave equivalence).

    source
    theorem MusicTheory.CircleOfFifths.red_fifth :
    red Temperament.fifth = 7

    The perfect fifth reduces to the generator 7 — exactly the generator stack iterates in DiatonicScale.lean. This is the seam between the two files.

    source
    theorem MusicTheory.CircleOfFifths.red_pc :
    red Temperament.pc = 0

    The Pythagorean comma vanishes in ℤ/12: red pc = 0. The closure defect of the circle of fifths is the pitch-class unison — the comma is "tempered out" literally, not just to a small number.

    source
    theorem MusicTheory.CircleOfFifths.red_kernel_vanishes (m : ℤ × ℤ) (h : m ∈ Temperament.v12.ker) :
    red m = 0

    Any comma tempered by 12-EDO is a pitch-class unison. red factors through v12, so every element of ker v12 reduces to 0 — the formal content of "tempering out a comma".

    source
    theorem MusicTheory.CircleOfFifths.red_closure_defect :
    red (12 • Temperament.fifth - 7 • Temperament.oct) = 0

    The closure defect of the circle of fifths reduces to the unison: red (12•fifth − 7•oct) = 0. (From closure_defect_eq_pc then red_pc.)

    source
    theorem MusicTheory.CircleOfFifths.circle_of_fifths_complete :
    DiatonicScale.stack 0 (red Temperament.fifth) 12 = Finset.univ

    THE BRIDGE THEOREM. Stacking the perfect fifth twelve times on the chromatic circle — with the generator being exactly red fifth from the JI lattice — visits every pitch class: stack 0 (red fifth) 12 = univ. The circle of fifths CLOSES (returns to 0 after twelve steps) and is COMPLETE (hits all twelve notes). This is the cross-file reason ker_v12_eq_span_pc / closure_defect_eq_pc (in ℤ²) force the ℤ/12 circle to close: the comma lands in the kernel ⇒ red collapses the defect to 0.

    Meantone: the ℤ/12 face of the meantone identity: four fifths = a major third #

    The 5-limit analog of the circle-of-fifths bridge. The 12-EDO reduction red5 : ℤ³ → ℤ/12 sends the just major third 5/4 to the pitch class 4 and the perfect fifth to 7; four fifths reduce to 4·7 = 28 ≡ 4 (mod 12), the same 4. So in 12-EDO four perfect fifths (mod octaves) ARE a major third — the harmonic seed of triadic functional harmony, and the ℤ/12 shadow of Temperament.meantone_identity_tempered.

    source
    def MusicTheory.CircleOfFifths.red5 (m : ℤ × ℤ × ℤ) :
    ZMod 12

    The 5-limit 12-EDO reduction. A 5-limit monzo 2^a·3^b·5^c ↦ its pitch class in ℤ/12, i.e. the 5-limit val v12_5 taken mod 12. Mirrors red on the 3-limit lattice.

    Equations
    Instances For
      source
      theorem MusicTheory.CircleOfFifths.red5_fifth5 :
      red5 Temperament.fifth5 = 7

      The perfect fifth reduces to 7.

      source
      theorem MusicTheory.CircleOfFifths.red5_third5 :
      red5 Temperament.third5 = 4

      The just major third 5/4 reduces to the pitch class 4.

      source
      theorem MusicTheory.CircleOfFifths.red5_oct5 :
      red5 Temperament.oct5 = 0

      The octave reduces to the pitch-class unison 0 (octave equivalence).

      source
      theorem MusicTheory.CircleOfFifths.four_fifths_eq_major_third :
      red5 (4 • Temperament.fifth5) = red5 Temperament.third5

      In 12-EDO, four fifths up equal a major third (mod octaves): red5 (4•fifth5) = red5 third5. Both sides are the pitch class 4 (4·7 = 28 ≡ 4). This is the harmonic analog of circle_of_fifths_complete and the ℤ/12 face of meantone_identity_tempered.