MUSIC_S1: {P}ythagorean Tuning: Pentatonic and Heptatonic Scale

proof end;

end;

definition

func RATPLUS -> non empty Subset of REAL+ equals :: MUSIC_S1:def 1
{ r where r is positive Rational : verum } ;

proof end;

end;

:: deftheorem defines RATPLUS MUSIC_S1:def 1 :

theorem Th2: :: MUSIC_S1:2

for r being object holds
( r is Element of RATPLUS iff r is positive Rational )

proof end;

theorem :: MUSIC_S1:3

RAT+ c= RAT

proof end;

definition

func REALPLUS -> non empty Subset of REAL+ equals :: MUSIC_S1:def 2
REAL+ \ {0};

proof end;

end;

:: deftheorem defines REALPLUS MUSIC_S1:def 2 :

theorem Th3: :: MUSIC_S1:4

NATPLUS c= RATPLUS

proof end;

theorem Th4: :: MUSIC_S1:5

NATPLUS c= REALPLUS

proof end;

theorem Th5: :: MUSIC_S1:6

RATPLUS c= REALPLUS

proof end;

definition

attr c₁ is strict ;
struct MusicStruct -> 1-sorted ;
aggr MusicStruct(# carrier, Equidistance, Ratio #) -> MusicStruct ;
sel Equidistance c₁ -> Relation of [: the carrier of c₁, the carrier of c₁:],[: the carrier of c₁, the carrier of c₁:];
sel Ratio c₁ -> Function of [: the carrier of c₁, the carrier of c₁:], the carrier of c₁;

end;

definition

let S be MusicStruct ;
let a, b, c, d be Element of S;

pred a,b equiv c,d means :: MUSIC_S1:def 3
[[a,b],[c,d]] in the Equidistance of S;

end;

:: deftheorem defines equiv MUSIC_S1:def 3 :

definition

let x, y be Element of REALPLUS ;

func REAL_ratio (x,y) -> Element of REALPLUS means :Def01: :: MUSIC_S1:def 4
ex r, s being positive Real st
( x = r & s = y & it = s / r );

proof end;

uniqueness ;

end;

:: deftheorem Def01 defines REAL_ratio MUSIC_S1:def 4 :

theorem Th6: :: MUSIC_S1:7

for a, b, c, d being Element of REALPLUS holds
( REAL_ratio (a,b) = REAL_ratio (c,d) iff REAL_ratio (b,a) = REAL_ratio (d,c) )

proof end;

definition

func REAL_ratio -> Function of [:REALPLUS,REALPLUS:],REALPLUS means :Def02: :: MUSIC_S1:def 5
for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st
( x = [y,z] & it . x = REAL_ratio (y,z) );

proof end;

proof end;

end;

:: deftheorem Def02 defines REAL_ratio MUSIC_S1:def 5 :

definition

func EQUIV_REAL_ratio -> Relation of [:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:] means :Def03: :: MUSIC_S1:def 6
for x, y being Element of [:REALPLUS,REALPLUS:] holds
( [x,y] in it iff ex a, b, c, d being Element of REALPLUS st
( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) );

proof end;

proof end;

end;

:: deftheorem Def03 defines EQUIV_REAL_ratio MUSIC_S1:def 6 :

definition

func REAL_Music -> MusicStruct equals :: MUSIC_S1:def 7
MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #);

end;

:: deftheorem defines REAL_Music MUSIC_S1:def 7 :

theorem Th7: :: MUSIC_S1:8

( not REAL_Music is empty & the carrier of REAL_Music c= REALPLUS & ( for f1, f2, f3, f4 being Element of REAL_Music holds
( f1,f2 equiv f3,f4 iff the Ratio of REAL_Music . (f1,f2) = the Ratio of REAL_Music . (f3,f4) ) ) )

proof end;

theorem Th8: :: MUSIC_S1:9

for f1, f2, f3 being Element of REAL_Music st the Ratio of REAL_Music . (f1,f2) = the Ratio of REAL_Music . (f1,f3) holds
f2 = f3

proof end;

theorem :: MUSIC_S1:10

NATPLUS c= the carrier of REAL_Music by Th4;

theorem Th9: :: MUSIC_S1:11

for frequency being Element of REAL_Music
for n being non zero Nat ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])

proof end;

theorem Th10: :: MUSIC_S1:12

for f1, f2, f3 being Element of REAL_Music st the Ratio of REAL_Music . (f1,f1) = the Ratio of REAL_Music . (f2,f3) holds
f2 = f3

proof end;

theorem Th11: :: MUSIC_S1:13

for f1, f2, fn1, fm1, fn2, fm2 being Element of REAL_Music
for r1, r2 being positive Real
for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2

proof end;

theorem Th12: :: MUSIC_S1:14

for f1, f2, f3, f4 being Element of REAL_Music holds
( the Ratio of REAL_Music . (f1,f2) = the Ratio of REAL_Music . (f3,f4) iff the Ratio of REAL_Music . (f2,f1) = the Ratio of REAL_Music . (f4,f3) )

proof end;

definition

let x, y be Element of RATPLUS ;

func RAT_ratio (x,y) -> Element of RATPLUS means :Def04: :: MUSIC_S1:def 8
ex r, s being positive Rational st
( x = r & s = y & it = s / r );

proof end;

uniqueness ;

end;

:: deftheorem Def04 defines RAT_ratio MUSIC_S1:def 8 :

theorem Th13: :: MUSIC_S1:15

for a, b, c, d being Element of RATPLUS holds
( RAT_ratio (a,b) = RAT_ratio (c,d) iff RAT_ratio (b,a) = RAT_ratio (d,c) )

proof end;

definition

func RAT_ratio -> Function of [:RATPLUS,RATPLUS:],RATPLUS means :Def05: :: MUSIC_S1:def 9
for x being Element of [:RATPLUS,RATPLUS:] ex y, z being Element of RATPLUS st
( x = [y,z] & it . x = RAT_ratio (y,z) );

proof end;

proof end;

end;

:: deftheorem Def05 defines RAT_ratio MUSIC_S1:def 9 :

definition

func EQUIV_RAT_ratio -> Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] means :Def06: :: MUSIC_S1:def 10
for x, y being Element of [:RATPLUS,RATPLUS:] holds
( [x,y] in it iff ex a, b, c, d being Element of RATPLUS st
( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) );

proof end;

proof end;

end;

:: deftheorem Def06 defines EQUIV_RAT_ratio MUSIC_S1:def 10 :

definition

func RAT_Music -> MusicStruct equals :: MUSIC_S1:def 11
MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #);

end;

:: deftheorem defines RAT_Music MUSIC_S1:def 11 :

theorem Th14: :: MUSIC_S1:16

( not RAT_Music is empty & the carrier of RAT_Music c= REALPLUS & ( for f1, f2, f3, f4 being Element of RAT_Music holds
( f1,f2 equiv f3,f4 iff the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) ) ) )

proof end;

theorem Th15: :: MUSIC_S1:17

for f1, f2, f3 being Element of RAT_Music st the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f1,f3) holds
f2 = f3

proof end;

theorem :: MUSIC_S1:18

NATPLUS c= the carrier of RAT_Music by Th3;

theorem Th16: :: MUSIC_S1:19

for frequency being Element of RAT_Music
for n being non zero Nat ex harmonique being Element of RAT_Music st [frequency,harmonique] in Class ( the Equidistance of RAT_Music,[1,n])

proof end;

theorem Th17: :: MUSIC_S1:20

for f1, f2, f3 being Element of RAT_Music st the Ratio of RAT_Music . (f1,f1) = the Ratio of RAT_Music . (f2,f3) holds
f2 = f3

proof end;

theorem :: MUSIC_S1:21

for frequency being Element of RAT_Music ex r being positive Real st
( frequency = r & ( for n being non zero Nat holds n * r is Element of RAT_Music ) )

proof end;

theorem Th18: :: MUSIC_S1:22

for f1, f2, fn1, fm1, fn2, fm2 being Element of RAT_Music
for r1, r2 being positive Rational
for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2

proof end;

theorem Th19: :: MUSIC_S1:23

for f1, f2, f3, f4 being Element of RAT_Music holds
( the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) iff the Ratio of RAT_Music . (f2,f1) = the Ratio of RAT_Music . (f4,f3) )

proof end;

definition

let S be MusicStruct ;

attr S is satisfying_Real means :Def07a: :: MUSIC_S1:def 12
the carrier of S c= REALPLUS ;

attr S is satisfying_equiv means :Def08a: :: MUSIC_S1:def 13
for f1, f2, f3, f4 being Element of S holds
( f1,f2 equiv f3,f4 iff the Ratio of S . (f1,f2) = the Ratio of S . (f3,f4) );

attr S is satisfying_interval means :Def09a: :: MUSIC_S1:def 14
for f1, f2, f3 being Element of S st the Ratio of S . (f1,f2) = the Ratio of S . (f1,f3) holds
f2 = f3;

attr S is satisfying_tonic means :Def10a: :: MUSIC_S1:def 15
for f1, f2, f3 being Element of S st the Ratio of S . (f1,f1) = the Ratio of S . (f2,f3) holds
f2 = f3;

attr S is satisfying_commutativity means :Def11a: :: MUSIC_S1:def 16
for f1, f2, f3, f4 being Element of S holds
( the Ratio of S . (f1,f2) = the Ratio of S . (f3,f4) iff the Ratio of S . (f2,f1) = the Ratio of S . (f4,f3) );

attr S is satisfying_Nat means :Def12a: :: MUSIC_S1:def 17
NATPLUS c= the carrier of S;

attr S is satisfying_harmonic_closed means :Def13a: :: MUSIC_S1:def 18
for frequency being Element of S
for n being non zero Nat ex harmonique being Element of S st [frequency,harmonique] in Class ( the Equidistance of S,[1,n]);

end;

:: deftheorem Def07a defines satisfying_Real MUSIC_S1:def 12 :

:: deftheorem Def08a defines satisfying_equiv MUSIC_S1:def 13 :

:: deftheorem Def09a defines satisfying_interval MUSIC_S1:def 14 :

:: deftheorem Def10a defines satisfying_tonic MUSIC_S1:def 15 :

:: deftheorem Def11a defines satisfying_commutativity MUSIC_S1:def 16 :

:: deftheorem Def12a defines satisfying_Nat MUSIC_S1:def 17 :

:: deftheorem Def13a defines satisfying_harmonic_closed MUSIC_S1:def 18 :

registration

cluster non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed for MusicStruct ;

proof end;

end;

definition end;

theorem Th20: :: MUSIC_S1:24

for S being satisfying_Nat MusicStruct
for n being non zero Nat holds n is Element of S

proof end;

theorem Th21: :: MUSIC_S1:25

for MS being satisfying_equiv MusicStruct
for a, b being Element of MS holds a,b equiv a,b

proof end;

theorem Th22: :: MUSIC_S1:26

for MS being satisfying_equiv MusicStruct
for a, b, c, d being Element of MS holds
( a,b equiv c,d iff c,d equiv a,b )

proof end;

theorem Th23: :: MUSIC_S1:27

for MS being satisfying_equiv MusicStruct
for a, b, c, d, e, f being Element of MS st a,b equiv c,d & c,d equiv e,f holds
a,b equiv e,f

proof end;

theorem Th24: :: MUSIC_S1:28

for S being satisfying_equiv satisfying_interval MusicStruct
for a, b, c being Element of S holds
( a,b equiv a,c iff b = c )

proof end;

theorem :: MUSIC_S1:29

for MS being satisfying_equiv MusicStruct
for a being Element of MS holds a,a equiv a,a

proof end;

theorem Th25: :: MUSIC_S1:30

for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is_reflexive_in [: the carrier of MS, the carrier of MS:]

proof end;

theorem :: MUSIC_S1:31

for MS being satisfying_equiv MusicStruct st not MS is empty holds
( the Equidistance of MS is reflexive & field the Equidistance of MS = [: the carrier of MS, the carrier of MS:] )

proof end;

theorem Th26: :: MUSIC_S1:32

for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is_symmetric_in [: the carrier of MS, the carrier of MS:]

proof end;

theorem Th27: :: MUSIC_S1:33

for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is_transitive_in [: the carrier of MS, the carrier of MS:]

proof end;

theorem :: MUSIC_S1:34

for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is Equivalence_Relation of [: the carrier of MS, the carrier of MS:]

proof end;

theorem Th28: :: MUSIC_S1:35

for MS being satisfying_equiv satisfying_commutativity MusicStruct
for a, b, c, d being Element of MS holds
( a,b equiv c,d iff b,a equiv d,c )

proof end;

theorem Th29: :: MUSIC_S1:36

for S being satisfying_equiv satisfying_tonic MusicStruct
for a, b, c being Element of S st a,a equiv b,c holds
b = c

proof end;

definition

let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;
let frequency be Element of S;
let n be non zero Nat;

func n -harmonique (S,frequency) -> Element of S means :Def08b: :: MUSIC_S1:def 19
[frequency,it] in Class ( the Equidistance of S,[1,n]);

existence by Def13a;
uniqueness

proof end;

end;

:: deftheorem Def08b defines -harmonique MUSIC_S1:def 19 :

definition

let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

attr S is satisfying_linearite_harmonique means :Def09: :: MUSIC_S1:def 20
for frequency being Element of S
for n being non zero Nat ex fr being positive Real st
( frequency = fr & n -harmonique (S,frequency) = n * fr );

end;

:: deftheorem Def09 defines satisfying_linearite_harmonique MUSIC_S1:def 20 :

theorem Th30: :: MUSIC_S1:37

REAL_Music is satisfying_linearite_harmonique

proof end;

theorem Th31: :: MUSIC_S1:38

RAT_Music is satisfying_linearite_harmonique

proof end;

registration end;

definition end;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

attr MS is satisfying_harmonique_stable means :Def10: :: MUSIC_S1:def 21
for f1, f2 being Element of MS
for n, m being non zero Nat holds n -harmonique (MS,f1),m -harmonique (MS,f1) equiv n -harmonique (MS,f2),m -harmonique (MS,f2);

end;

:: deftheorem Def10 defines satisfying_harmonique_stable MUSIC_S1:def 21 :

theorem Th32: :: MUSIC_S1:39

REAL_Music is satisfying_harmonique_stable

proof end;

theorem Th33: :: MUSIC_S1:40

RAT_Music is satisfying_harmonique_stable

proof end;

registration end;

definition end;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;
let frequency be Element of MS;

func unison (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 22
Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(1 -harmonique (MS,frequency))]);

func octave (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 23
Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(2 -harmonique (MS,frequency))]);

func fifth (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 24
Class ( the Equidistance of MS,[(2 -harmonique (MS,frequency)),(3 -harmonique (MS,frequency))]);

func fourth (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 25
Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(4 -harmonique (MS,frequency))]);

func major_sixth (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 26
Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]);

func major_third (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 27
Class ( the Equidistance of MS,[(4 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]);

func minor_third (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 28
Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(6 -harmonique (MS,frequency))]);

func minor_sixth (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 29
Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(8 -harmonique (MS,frequency))]);

func major_tone (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 30
Class ( the Equidistance of MS,[(8 -harmonique (MS,frequency)),(9 -harmonique (MS,frequency))]);

func minor_tone (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 31
Class ( the Equidistance of MS,[(9 -harmonique (MS,frequency)),(10 -harmonique (MS,frequency))]);

end;

:: deftheorem defines unison MUSIC_S1:def 22 :

:: deftheorem defines octave MUSIC_S1:def 23 :

:: deftheorem defines fifth MUSIC_S1:def 24 :

:: deftheorem defines fourth MUSIC_S1:def 25 :

:: deftheorem defines major_sixth MUSIC_S1:def 26 :

:: deftheorem defines major_third MUSIC_S1:def 27 :

:: deftheorem defines minor_third MUSIC_S1:def 28 :

:: deftheorem defines minor_sixth MUSIC_S1:def 29 :

:: deftheorem defines major_tone MUSIC_S1:def 30 :

:: deftheorem defines minor_tone MUSIC_S1:def 31 :

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

func unison MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 32
Class ( the Equidistance of MS,[1,1]);

func octave MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 33
Class ( the Equidistance of MS,[1,2]);

func fifth MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 34
Class ( the Equidistance of MS,[2,3]);

func fourth MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 35
Class ( the Equidistance of MS,[3,4]);

func major_sixth MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 36
Class ( the Equidistance of MS,[3,5]);

func major_third MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 37
Class ( the Equidistance of MS,[4,5]);

func minor_third MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 38
Class ( the Equidistance of MS,[5,6]);

func minor_sixth MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 39
Class ( the Equidistance of MS,[5,8]);

func major_tone MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 40
Class ( the Equidistance of MS,[8,9]);

func minor_tone MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 41
Class ( the Equidistance of MS,[9,10]);

end;

:: deftheorem defines unison MUSIC_S1:def 32 :

:: deftheorem defines octave MUSIC_S1:def 33 :

:: deftheorem defines fifth MUSIC_S1:def 34 :

:: deftheorem defines fourth MUSIC_S1:def 35 :

:: deftheorem defines major_sixth MUSIC_S1:def 36 :

:: deftheorem defines major_third MUSIC_S1:def 37 :

:: deftheorem defines minor_third MUSIC_S1:def 38 :

:: deftheorem defines minor_sixth MUSIC_S1:def 39 :

:: deftheorem defines major_tone MUSIC_S1:def 40 :

:: deftheorem defines minor_tone MUSIC_S1:def 41 :

definition

let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

attr S is satisfying_fifth_constructible means :Def11: :: MUSIC_S1:def 42
for frequency being Element of S ex q being Element of S st [frequency,q] in fifth S;

end;

:: deftheorem Def11 defines satisfying_fifth_constructible MUSIC_S1:def 42 :

theorem Th34: :: MUSIC_S1:41

for frequency being Element of REAL_Music ex fr, qr being positive Real st
( fr = frequency & qr = (3 / 2) * fr & [fr,qr] in fifth REAL_Music )

proof end;

theorem Th35: :: MUSIC_S1:42

REAL_Music is satisfying_fifth_constructible

proof end;

theorem Th36: :: MUSIC_S1:43

for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = (3 / 2) * fr & [fr,qr] in fifth RAT_Music )

proof end;

theorem Th37: :: MUSIC_S1:44

RAT_Music is satisfying_fifth_constructible

proof end;

registration end;

definition end;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct ;
let frequency be Element of MS;

func Fifth (MS,frequency) -> Element of MS means :Def11bis: :: MUSIC_S1:def 43
[frequency,it] in fifth MS;

existence by Def11;
uniqueness

proof end;

end;

:: deftheorem Def11bis defines Fifth MUSIC_S1:def 43 :

theorem :: MUSIC_S1:45

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible MusicStruct
for frequency being Element of MS holds fifth (MS,frequency) = fifth MS

proof end;

theorem Th38: :: MUSIC_S1:46

for frequency being Element of REAL_Music ex fr being positive Real st
( frequency = fr & Fifth (REAL_Music,frequency) = (3 / 2) * fr )

proof end;

theorem Th39: :: MUSIC_S1:47

for frequency being Element of RAT_Music ex fr being positive Rational st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr )

proof end;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct ;

attr MS is classical_fifth means :Def12: :: MUSIC_S1:def 44
for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fifth (MS,frequency) = (3 / 2) * fr );

end;

:: deftheorem Def12 defines classical_fifth MUSIC_S1:def 44 :

registration end;

definition end;

theorem Th40: :: MUSIC_S1:48

for MS being satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed MusicStruct
for frequency being Element of MS holds 1 -harmonique (MS,frequency) = frequency

proof end;

theorem :: MUSIC_S1:49

for MS being satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_harmonique_stable MusicStruct
for a, b being Element of MS holds a,a equiv b,b

proof end;

theorem :: MUSIC_S1:50

for MS being satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct
for frequency being Element of MS holds octave (MS,frequency) = octave MS

proof end;

theorem :: MUSIC_S1:51

for MS being non empty satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct
for frequency being Element of MS ex seq being sequence of MS st
( seq . 0 = frequency & ( for n being Nat holds [(seq . n),(seq . (n + 1))] in fifth MS ) )

proof end;

definition

let MS be MusicStruct ;
let a, b, c be Element of MS;

pred b is_Between a,c means :: MUSIC_S1:def 45
ex r1, r2, r3 being positive Real st
( a = r1 & b = r2 & c = r3 & r1 <= r2 & r2 < r3 );

end;

:: deftheorem defines is_Between MUSIC_S1:def 45 :

definition

let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

attr S is satisfying_octave_constructible means :Def13: :: MUSIC_S1:def 46
for frequency being Element of S ex o being Element of S st [frequency,o] in octave S;

end;

:: deftheorem Def13 defines satisfying_octave_constructible MUSIC_S1:def 46 :

theorem Th41: :: MUSIC_S1:52

for frequency being Element of REAL_Music ex fr, qr being positive Real st
( fr = frequency & qr = 2 * fr & [fr,qr] in octave REAL_Music )

proof end;

theorem Th42: :: MUSIC_S1:53

REAL_Music is satisfying_octave_constructible

proof end;

theorem Th43: :: MUSIC_S1:54

for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = 2 * fr & [fr,qr] in octave RAT_Music )

proof end;

theorem Th44: :: MUSIC_S1:55

RAT_Music is satisfying_octave_constructible

proof end;

registration end;

definition end;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct ;
let frequency be Element of MS;

func Octave (MS,frequency) -> Element of MS means :Def14: :: MUSIC_S1:def 47
[frequency,it] in octave MS;

existence by Def13;
uniqueness

proof end;

end;

:: deftheorem Def14 defines Octave MUSIC_S1:def 47 :

definition

let MS be non empty satisfying_Real MusicStruct ;
let r be Element of MS;

func @ r -> positive Real equals :: MUSIC_S1:def 48
r;

proof end;

end;

:: deftheorem defines @ MUSIC_S1:def 48 :

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct ;

attr MS is classical_octave means :Def15: :: MUSIC_S1:def 49
for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Octave (MS,frequency) = 2 * fr );

end;

:: deftheorem Def15 defines classical_octave MUSIC_S1:def 49 :

theorem Th45: :: MUSIC_S1:56

REAL_Music is classical_octave

proof end;

theorem Th46: :: MUSIC_S1:57

RAT_Music is classical_octave

proof end;

registration end;

definition end;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct ;

attr MS is satisfying_octave_descendent_constructible means :Def16: :: MUSIC_S1:def 50
for frequency being Element of MS ex o being Element of MS st [o,frequency] in octave MS;

end;

:: deftheorem Def16 defines satisfying_octave_descendent_constructible MUSIC_S1:def 50 :

theorem Th47: :: MUSIC_S1:58

for frequency being Element of REAL_Music ex fr, qr being positive Real st
( fr = frequency & qr = (1 / 2) * fr & [qr,fr] in octave REAL_Music )

proof end;

theorem Th48: :: MUSIC_S1:59

REAL_Music is satisfying_octave_descendent_constructible

proof end;

theorem Th49: :: MUSIC_S1:60

for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = (1 / 2) * fr & [qr,fr] in octave RAT_Music )

proof end;

theorem Th50: :: MUSIC_S1:61

RAT_Music is satisfying_octave_descendent_constructible

proof end;

registration

cluster non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible for MusicStruct ;

existence by Th48;

end;

definition

:: original: REAL_Music
redefine func REAL_Music -> non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct ;
coherence by Th48;

end;

definition

:: original: RAT_Music
redefine func RAT_Music -> non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct ;
coherence by Th50;

end;

definition

let MS be satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct ;
let frequency be Element of MS;

func Octave_descendent (MS,frequency) -> Element of MS means :Def17: :: MUSIC_S1:def 51
[it,frequency] in octave MS;

existence by Def16;
uniqueness

proof end;

end;

:: deftheorem Def17 defines Octave_descendent MUSIC_S1:def 51 :

theorem Th51: :: MUSIC_S1:62

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency being Element of MS ex r being positive Real st
( frequency = r & Octave_descendent (MS,frequency) = r / 2 )

proof end;

theorem Th52: :: MUSIC_S1:63

for MS1, MS2 being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave MusicStruct
for f1 being Element of MS1
for f2 being Element of MS2 st f1 = f2 holds
( Fifth (MS1,f1) = Fifth (MS2,f2) & Octave (MS1,f1) = Octave (MS2,f2) )

proof end;

theorem Th53: :: MUSIC_S1:64

for MS1, MS2 being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency1 being Element of MS1
for frequency2 being Element of MS2 st frequency1 = frequency2 holds
Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2)

proof end;

definition

func Fifth_reduct (MS,fondamentale,frequency) -> Element of MS equals :Def18: :: MUSIC_S1:def 52
Fifth (MS,frequency) if Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale)
otherwise Octave_descendent (MS,(Fifth (MS,frequency)));

correctness ;

end;

:: deftheorem Def18 defines Fifth_reduct MUSIC_S1:def 52 :

theorem :: MUSIC_S1:65

for MS1, MS2 being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency1, fondamentale1 being Element of MS1
for frequency2, fondamentale2 being Element of MS2 st frequency1 = frequency2 & fondamentale1 = fondamentale2 holds
Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2)

proof end;

theorem Th54: :: MUSIC_S1:66

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth MusicStruct
for frequency being Element of MS ex r, s being positive Real st
( r = frequency & s = (3 / 2) * r & Fifth (MS,frequency) = s )

proof end;

theorem Th55: :: MUSIC_S1:67

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale, frequency being Element of MS st frequency is_Between fondamentale, Octave (MS,fondamentale) holds
ex r1, r2, r3 being positive Real st
( fondamentale = r1 & frequency = r2 & Octave (MS,fondamentale) = 2 * r1 & r1 <= r2 & r2 <= 2 * r1 )

proof end;

theorem Th56: :: MUSIC_S1:68

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale, frequency being Element of MS st frequency is_Between fondamentale, Octave (MS,fondamentale) holds
Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale)

proof end;

definition

mode MusicSpace is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct ;

end;

theorem :: MUSIC_S1:69

REAL_Music is MusicSpace ;

theorem :: MUSIC_S1:70

RAT_Music is MusicSpace ;

theorem Th56BIS: :: MUSIC_S1:71

for MS being non empty satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct
for fondamentale, frequency being Element of MS ex seq being sequence of MS st
( seq . 0 = frequency & ( for n being Nat holds seq . (n + 1) = Fifth_reduct (MS,fondamentale,(seq . n)) ) )

proof end;

definition

let MS be non empty satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct ;
let fondamentale, frequency be Element of MS;

func spiral_of_fifths (MS,fondamentale,frequency) -> sequence of MS means :Def19: :: MUSIC_S1:def 53
( it . 0 = frequency & ( for n being Nat holds it . (n + 1) = Fifth_reduct (MS,fondamentale,(it . n)) ) );

existence by Th56BIS;
uniqueness

proof end;

end;

:: deftheorem Def19 defines spiral_of_fifths MUSIC_S1:def 53 :

theorem Th57: :: MUSIC_S1:72

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale, frequency being Element of MS st frequency is_Between fondamentale, Octave (MS,fondamentale) holds
for n being Nat holds (spiral_of_fifths (MS,fondamentale,frequency)) . n is_Between fondamentale, Octave (MS,fondamentale)

proof end;

theorem Th58: :: MUSIC_S1:73

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale being Element of MS holds (spiral_of_fifths (MS,fondamentale,fondamentale)) . 1 = (3 / 2) * (@ fondamentale)

proof end;

theorem Th59: :: MUSIC_S1:74

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale being Element of MS holds (spiral_of_fifths (MS,fondamentale,fondamentale)) . 2 = (9 / 8) * (@ fondamentale)

proof end;

theorem Th60: :: MUSIC_S1:75

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale being Element of MS holds (spiral_of_fifths (MS,fondamentale,fondamentale)) . 3 = (27 / 16) * (@ fondamentale)

proof end;

theorem Th61: :: MUSIC_S1:76

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale being Element of MS holds (spiral_of_fifths (MS,fondamentale,fondamentale)) . 4 = (81 / 64) * (@ fondamentale)

proof end;

theorem :: MUSIC_S1:77

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale being Element of MS holds (spiral_of_fifths (MS,fondamentale,fondamentale)) . 5 = (243 / 128) * (@ fondamentale)

proof end;

theorem Th62: :: MUSIC_S1:78

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency being Element of MS holds (@ ((spiral_of_fifths (MS,frequency,frequency)) . 2)) / (@ frequency) = (3 * 3) / ((2 * 2) * 2)

proof end;

theorem Th63: :: MUSIC_S1:79

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency being Element of MS holds (@ ((spiral_of_fifths (MS,frequency,frequency)) . 4)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 2)) = (3 * 3) / ((2 * 2) * 2)

proof end;

theorem Th64: :: MUSIC_S1:80

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency being Element of MS holds (@ ((spiral_of_fifths (MS,frequency,frequency)) . 1)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 4)) = 32 / 27

proof end;

theorem Th65: :: MUSIC_S1:81

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency being Element of MS holds (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 1)) = 9 / 8

proof end;

theorem Th66: :: MUSIC_S1:82

for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency being Element of MS holds (@ (Octave (MS,frequency))) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) = 32 / 27

proof end;

definition

let MS be MusicSpace;
let scale be Element of 2 -tuples_on the carrier of MS;

attr scale is monotonic means :: MUSIC_S1:def 54
ex frequency being Element of MS ex r1, r2 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & r1 < r2 & scale . 2 = Octave (MS,frequency) );

end;

:: deftheorem defines monotonic MUSIC_S1:def 54 :

definition

let MS be MusicSpace;
let scale be Element of 3 -tuples_on the carrier of MS;

attr scale is ditonic means :: MUSIC_S1:def 55
ex frequency being Element of MS ex r1, r2, r3 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & r1 < r2 & r2 < r3 & scale . 3 = Octave (MS,frequency) );

end;

:: deftheorem defines ditonic MUSIC_S1:def 55 :

definition

let MS be MusicSpace;
let scale be Element of 4 -tuples_on the carrier of MS;

attr scale is tritonic means :: MUSIC_S1:def 56
ex frequency being Element of MS ex r1, r2, r3, r4 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & r1 < r2 & r2 < r3 & r3 < r4 & scale . 4 = Octave (MS,frequency) );

end;

:: deftheorem defines tritonic MUSIC_S1:def 56 :

definition

let MS be MusicSpace;
let scale be Element of 5 -tuples_on the carrier of MS;

attr scale is tetratonic means :: MUSIC_S1:def 57
ex frequency being Element of MS ex r1, r2, r3, r4, r5 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & scale . 5 = Octave (MS,frequency) );

end;

:: deftheorem defines tetratonic MUSIC_S1:def 57 :

definition

let MS be MusicSpace;
let n be natural Number ;
let scale be Element of n -tuples_on the carrier of MS;

attr scale is pentatonic means :: MUSIC_S1:def 58
( n = 6 & ex frequency being Element of MS ex r1, r2, r3, r4, r5, r6 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & scale . 6 = r6 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & scale . 6 = Octave (MS,frequency) ) );

end;

:: deftheorem defines pentatonic MUSIC_S1:def 58 :

definition

let MS be MusicSpace;
let scale be Element of 7 -tuples_on the carrier of MS;

attr scale is hexatonic means :: MUSIC_S1:def 59
ex frequency being Element of MS ex r1, r2, r3, r4, r5, r6, r7 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & scale . 6 = r6 & scale . 7 = r7 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & scale . 7 = Octave (MS,frequency) );

end;

:: deftheorem defines hexatonic MUSIC_S1:def 59 :

definition

let MS be MusicSpace;
let n be natural Number ;
let scale be Element of n -tuples_on the carrier of MS;

attr scale is heptatonic means :: MUSIC_S1:def 60
( n = 8 & ex frequency being Element of MS ex r1, r2, r3, r4, r5, r6, r7, r8 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & scale . 6 = r6 & scale . 7 = r7 & scale . 8 = r8 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 & scale . 8 = Octave (MS,frequency) ) );

end;

:: deftheorem defines heptatonic MUSIC_S1:def 60 :

definition

let MS be MusicSpace;
let scale be Element of 9 -tuples_on the carrier of MS;

attr scale is octatonic means :: MUSIC_S1:def 61
ex frequency being Element of MS ex r1, r2, r3, r4, r5, r6, r7, r8, r9 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & scale . 6 = r6 & scale . 7 = r7 & scale . 8 = r8 & scale . 9 = r9 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8 & r8 < r9 & scale . 9 = Octave (MS,frequency) );

end;

:: deftheorem defines octatonic MUSIC_S1:def 61 :

definition

let MS be MusicSpace;
let frequency be Element of MS;

func pentatonic_pythagorean_scale (MS,frequency) -> Element of 6 -tuples_on the carrier of MS means :Def20: :: MUSIC_S1:def 62
( it . 1 = frequency & it . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & it . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & it . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & it . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & it . 6 = Octave (MS,frequency) );

proof end;

proof end;

end;

:: deftheorem Def20 defines pentatonic_pythagorean_scale MUSIC_S1:def 62 :

theorem Th67: :: MUSIC_S1:83

for MS being MusicSpace
for frequency being Element of MS holds pentatonic_pythagorean_scale (MS,frequency) is pentatonic

proof end;

definition

let MS be MusicSpace;
let f1, f2 be Element of MS;

func intrval (f1,f2) -> positive Real means :Def21: :: MUSIC_S1:def 63
ex r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & it = r2 / r1 );

proof end;

uniqueness ;

end;

:: deftheorem Def21 defines intrval MUSIC_S1:def 63 :

definition

func pythagorean_tone -> positive Real equals :: MUSIC_S1:def 64
9 / 8;

end;

:: deftheorem defines pythagorean_tone MUSIC_S1:def 64 :

definition

func pentatonic_pythagorean_semiditone -> positive Real equals :: MUSIC_S1:def 65
32 / 27;

end;

:: deftheorem defines pentatonic_pythagorean_semiditone MUSIC_S1:def 65 :

definition

func major_third_pythagorean_tone -> positive Real equals :: MUSIC_S1:def 66
pythagorean_tone * pythagorean_tone;

end;

:: deftheorem defines major_third_pythagorean_tone MUSIC_S1:def 66 :

definition

func pure_major_third -> positive Real equals :: MUSIC_S1:def 67
5 / 4;

end;

:: deftheorem defines pure_major_third MUSIC_S1:def 67 :

definition

func syntonic_comma -> positive Real equals :: MUSIC_S1:def 68
major_third_pythagorean_tone / pure_major_third;

end;

:: deftheorem defines syntonic_comma MUSIC_S1:def 68 :

theorem :: MUSIC_S1:84

syntonic_comma = 81 / 80 ;

theorem :: MUSIC_S1:85

pythagorean_tone < pentatonic_pythagorean_semiditone ;

theorem :: MUSIC_S1:86

(((pythagorean_tone * pythagorean_tone) * pentatonic_pythagorean_semiditone) * pythagorean_tone) * pentatonic_pythagorean_semiditone = 2 ;

definition

let MS be MusicSpace;
let frequency be Element of MS;

func penta_fondamentale (MS,frequency) -> Element of MS equals :: MUSIC_S1:def 69
(pentatonic_pythagorean_scale (MS,frequency)) . 1;

coherence by Def20;

func penta_1 (MS,frequency) -> Element of MS equals :: MUSIC_S1:def 70
(pentatonic_pythagorean_scale (MS,frequency)) . 2;

proof end;

func penta_2 (MS,frequency) -> Element of MS equals :: MUSIC_S1:def 71
(pentatonic_pythagorean_scale (MS,frequency)) . 3;

proof end;

func penta_3 (MS,frequency) -> Element of MS equals :: MUSIC_S1:def 72
(pentatonic_pythagorean_scale (MS,frequency)) . 4;

proof end;

func penta_4 (MS,frequency) -> Element of MS equals :: MUSIC_S1:def 73
(pentatonic_pythagorean_scale (MS,frequency)) . 5;

proof end;

func penta_octave (MS,frequency) -> Element of MS equals :: MUSIC_S1:def 74
Octave (MS,frequency);

end;

:: deftheorem defines penta_fondamentale MUSIC_S1:def 69 :

:: deftheorem defines penta_1 MUSIC_S1:def 70 :

:: deftheorem defines penta_2 MUSIC_S1:def 71 :

:: deftheorem defines penta_3 MUSIC_S1:def 72 :

:: deftheorem defines penta_4 MUSIC_S1:def 73 :

:: deftheorem defines penta_octave MUSIC_S1:def 74 :

theorem :: MUSIC_S1:87

for MS being MusicSpace
for f1, f2 being Element of MS ex r1, r2 being Element of REALPLUS st intrval (f1,f2) = REAL_ratio (r1,r2)

proof end;

theorem Th68: :: MUSIC_S1:88

for MS being MusicSpace
for frequency being Element of MS
for r1, r2, r3, r4, r5, r6 being positive Real st (pentatonic_pythagorean_scale (MS,frequency)) . 1 = r1 & (pentatonic_pythagorean_scale (MS,frequency)) . 2 = r2 & (pentatonic_pythagorean_scale (MS,frequency)) . 3 = r3 & (pentatonic_pythagorean_scale (MS,frequency)) . 4 = r4 & (pentatonic_pythagorean_scale (MS,frequency)) . 5 = r5 & (pentatonic_pythagorean_scale (MS,frequency)) . 6 = r6 holds
( r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 32 / 27 & r5 / r4 = 9 / 8 & r6 / r5 = 32 / 27 )

proof end;

theorem Th69: :: MUSIC_S1:89

for MS being MusicSpace
for frequency being Element of MS ex r1, r2, r3, r4, r5, r6 being positive Real st
( (pentatonic_pythagorean_scale (MS,frequency)) . 1 = r1 & (pentatonic_pythagorean_scale (MS,frequency)) . 2 = r2 & (pentatonic_pythagorean_scale (MS,frequency)) . 3 = r3 & (pentatonic_pythagorean_scale (MS,frequency)) . 4 = r4 & (pentatonic_pythagorean_scale (MS,frequency)) . 5 = r5 & (pentatonic_pythagorean_scale (MS,frequency)) . 6 = r6 & r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 32 / 27 & r5 / r4 = 9 / 8 & r6 / r5 = 32 / 27 )

proof end;

theorem :: MUSIC_S1:90

9 / 8 = 9 / 8 ;

theorem :: MUSIC_S1:91

for MS being MusicSpace
for frequency being Element of MS holds
( intrval ((penta_fondamentale (MS,frequency)),(penta_1 (MS,frequency))) = pythagorean_tone & intrval ((penta_1 (MS,frequency)),(penta_2 (MS,frequency))) = pythagorean_tone & intrval ((penta_2 (MS,frequency)),(penta_3 (MS,frequency))) = pentatonic_pythagorean_semiditone & intrval ((penta_3 (MS,frequency)),(penta_4 (MS,frequency))) = pythagorean_tone & intrval ((penta_4 (MS,frequency)),(penta_octave (MS,frequency))) = pentatonic_pythagorean_semiditone )

proof end;

theorem :: MUSIC_S1:92

for MS being MusicSpace
for frequency being Element of MS holds Fifth (MS,frequency) is_Between frequency, Octave (MS,frequency)

proof end;

theorem Th70: :: MUSIC_S1:93

for MS being MusicSpace
for f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( Fifth (MS,f2) = 2 * r1 & not Fifth (MS,f2) is_Between f1, Octave (MS,f1) )

proof end;

theorem Th71: :: MUSIC_S1:94

for MS being MusicSpace
for fondamentale, f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( ( Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 ) & ( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 ) )

proof end;

theorem :: MUSIC_S1:95

for MS being MusicSpace
for f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
Fifth_reduct (MS,f1,f2) = f1

proof end;

definition

let S be MusicSpace;

attr S is satisfying_fourth_constructible means :Def22: :: MUSIC_S1:def 75
for frequency being Element of S ex q being Element of S st [frequency,q] in fourth S;

end;

:: deftheorem Def22 defines satisfying_fourth_constructible MUSIC_S1:def 75 :

theorem Th78: :: MUSIC_S1:96

for MS being MusicSpace st MS = REAL_Music holds
for frequency being Element of MS ex fr, qr being positive Real st
( fr = frequency & qr = (4 / 3) * fr & [fr,qr] in fourth MS )

proof end;

theorem Th79: :: MUSIC_S1:97

REAL_Music is satisfying_fourth_constructible

proof end;

registration end;

definition

let MS be satisfying_fourth_constructible MusicSpace;
let frequency be Element of MS;

func Fourth (MS,frequency) -> Element of MS means :Def23: :: MUSIC_S1:def 76
[frequency,it] in fourth MS;

existence by Def22;
uniqueness

proof end;

end;

:: deftheorem Def23 defines Fourth MUSIC_S1:def 76 :

definition

let MS be satisfying_fourth_constructible MusicSpace;

attr MS is classical_fourth means :Def24: :: MUSIC_S1:def 77
for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr );

end;

:: deftheorem Def24 defines classical_fourth MUSIC_S1:def 77 :

theorem Th80: :: MUSIC_S1:98

for MS being satisfying_fourth_constructible MusicSpace st MS = REAL_Music holds
for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr )

proof end;

registration end;

definition

let MS be non empty satisfying_Real MusicStruct ;

attr MS is satisfying_euclidean means :Def25: :: MUSIC_S1:def 78
for f1, f2 being Element of MS holds the Ratio of MS . (f1,f2) = (@ f2) / (@ f1);

end;

:: deftheorem Def25 defines satisfying_euclidean MUSIC_S1:def 78 :

registration

cluster non empty satisfying_Real satisfying_euclidean for MusicStruct ;

proof end;

end;

registration

cluster non empty satisfying_Real satisfying_euclidean -> non empty satisfying_Real satisfying_interval for MusicStruct ;

proof end;

end;

registration

cluster non empty satisfying_Real satisfying_euclidean -> non empty satisfying_Real satisfying_tonic for MusicStruct ;

proof end;

end;

registration

cluster non empty satisfying_Real satisfying_euclidean -> non empty satisfying_Real satisfying_commutativity for MusicStruct ;

proof end;

end;

registration end;

definition

mode Heptatonic_Pythagorean_Score is satisfying_fourth_constructible classical_fourth MusicSpace;

end;

definition

let HPS be Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;

func heptatonic_pythagorean_scale (HPS,frequency) -> Element of 8 -tuples_on the carrier of HPS means :Def26: :: MUSIC_S1:def 79
( it . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & it . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & it . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & it . 4 = Fourth (HPS,frequency) & it . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & it . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & it . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & it . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) );

proof end;

proof end;

end;

:: deftheorem Def26 defines heptatonic_pythagorean_scale MUSIC_S1:def 79 :

theorem Th81: :: MUSIC_S1:99

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds Fourth (HPS,frequency) is_Between frequency, Octave (HPS,frequency)

proof end;

theorem :: MUSIC_S1:100

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS
for n being Nat holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . n is_Between frequency, Octave (HPS,frequency) by Th57, Th81;

theorem Th82: :: MUSIC_S1:101

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 = frequency

proof end;

theorem Th83: :: MUSIC_S1:102

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 = (3 / 2) * (@ frequency)

proof end;

theorem Th84: :: MUSIC_S1:103

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 = (9 / 8) * (@ frequency)

proof end;

theorem Th85: :: MUSIC_S1:104

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 = (27 / 16) * (@ frequency)

proof end;

theorem Th86: :: MUSIC_S1:105

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 = (81 / 64) * (@ frequency)

proof end;

theorem Th87: :: MUSIC_S1:106

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 = (243 / 128) * (@ frequency)

proof end;

theorem Th88: :: MUSIC_S1:107

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = 1 * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = (9 / 8) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = (81 / 64) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = (4 / 3) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = (3 / 2) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = (27 / 16) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = (243 / 128) * (@ frequency) & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = 2 * (@ frequency) )

proof end;

theorem Th88BIS: :: MUSIC_S1:108

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is heptatonic

proof end;

definition

func heptatonic_pythagorean_semitone -> positive Real equals :: MUSIC_S1:def 80
256 / 243;

end;

:: deftheorem defines heptatonic_pythagorean_semitone MUSIC_S1:def 80 :

notation

synonym limma_pythagoricien for heptatonic_pythagorean_semitone ;

end;

notation

synonym diatonic_tone for pythagorean_tone ;

end;

theorem :: MUSIC_S1:109

pythagorean_tone / 2 < heptatonic_pythagorean_semitone ;

theorem :: MUSIC_S1:110

(((((pythagorean_tone * pythagorean_tone) * heptatonic_pythagorean_semitone) * pythagorean_tone) * pythagorean_tone) * pythagorean_tone) * heptatonic_pythagorean_semitone = 2 ;

definition

let HPS be Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;

func hepta_fondamental (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 81
(heptatonic_pythagorean_scale (HPS,frequency)) . 1;

proof end;

func hepta_1 (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 82
(heptatonic_pythagorean_scale (HPS,frequency)) . 2;

proof end;

func hepta_2 (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 83
(heptatonic_pythagorean_scale (HPS,frequency)) . 3;

proof end;

func hepta_3 (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 84
(heptatonic_pythagorean_scale (HPS,frequency)) . 4;

proof end;

func hepta_4 (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 85
(heptatonic_pythagorean_scale (HPS,frequency)) . 5;

proof end;

func hepta_5 (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 86
(heptatonic_pythagorean_scale (HPS,frequency)) . 6;

proof end;

func hepta_6 (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 87
(heptatonic_pythagorean_scale (HPS,frequency)) . 7;

proof end;

func hepta_octave (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 88
Octave (HPS,frequency);

end;

:: deftheorem defines hepta_fondamental MUSIC_S1:def 81 :

:: deftheorem defines hepta_1 MUSIC_S1:def 82 :

:: deftheorem defines hepta_2 MUSIC_S1:def 83 :

:: deftheorem defines hepta_3 MUSIC_S1:def 84 :

:: deftheorem defines hepta_4 MUSIC_S1:def 85 :

:: deftheorem defines hepta_5 MUSIC_S1:def 86 :

:: deftheorem defines hepta_6 MUSIC_S1:def 87 :

:: deftheorem defines hepta_octave MUSIC_S1:def 88 :

Lem89: for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS
for r1, r2, r3, r4, r5, r6, r7, r8 being positive Real st (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r1 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r2 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r3 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 holds
( r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 256 / 243 & r5 / r4 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )

proof end;

Lem90: for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS ex r1, r2, r3, r4, r5, r6, r7, r8 being positive Real st
( (heptatonic_pythagorean_scale (HPS,frequency)) . 1 = r1 & (heptatonic_pythagorean_scale (HPS,frequency)) . 2 = r2 & (heptatonic_pythagorean_scale (HPS,frequency)) . 3 = r3 & (heptatonic_pythagorean_scale (HPS,frequency)) . 4 = r4 & (heptatonic_pythagorean_scale (HPS,frequency)) . 5 = r5 & (heptatonic_pythagorean_scale (HPS,frequency)) . 6 = r6 & (heptatonic_pythagorean_scale (HPS,frequency)) . 7 = r7 & (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = r8 & r2 / r1 = 9 / 8 & r3 / r2 = 9 / 8 & r4 / r3 = 256 / 243 & r5 / r4 = 9 / 8 & r6 / r5 = 9 / 8 & r7 / r6 = 9 / 8 & r8 / r7 = 256 / 243 )

proof end;

theorem Th90: :: MUSIC_S1:111

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
( intrval ((hepta_fondamental (HPS,frequency)),(hepta_1 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_1 (HPS,frequency)),(hepta_2 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_2 (HPS,frequency)),(hepta_3 (HPS,frequency))) = heptatonic_pythagorean_semitone & intrval ((hepta_3 (HPS,frequency)),(hepta_4 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_4 (HPS,frequency)),(hepta_5 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_5 (HPS,frequency)),(hepta_6 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_6 (HPS,frequency)),(hepta_octave (HPS,frequency))) = heptatonic_pythagorean_semitone )

proof end;

definition

let MS be MusicSpace;
let n be natural Number ;
let scale be Element of n -tuples_on the carrier of MS;
assume scale is heptatonic ;

attr scale is perfect_fifth means :Def27: :: MUSIC_S1:def 89
( [(scale . 1),(scale . 5)] in fifth MS & [(scale . 2),(scale . 6)] in fifth MS & [(scale . 3),(scale . 7)] in fifth MS & [(scale . 4),(scale . 8)] in fifth MS );

end;

:: deftheorem Def27 defines perfect_fifth MUSIC_S1:def 89 :

theorem :: MUSIC_S1:112

for HPS being satisfying_euclidean Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is perfect_fifth

proof end;

definition

let HPS be Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;

func heptatonic_pythagorean_scale_ascending (HPS,frequency) -> Element of 8 -tuples_on the carrier of HPS equals :: MUSIC_S1:def 90
heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)));