:: deftheorem Def26 defines heptatonic_pythagorean_scale MUSIC_S1:def 79 :
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS
for b₃ being Element of 8 -tuples_on the carrier of HPS holds
( b₃ = heptatonic_pythagorean_scale (HPS,frequency) iff ( b₃ . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & b₃ . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & b₃ . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & b₃ . 4 = Fourth (HPS,frequency) & b₃ . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & b₃ . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & b₃ . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & b₃ . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) ) );