:: by Roland Coghetto

::

:: Received September 29, 2018

:: Copyright (c) 2018-2019 Association of Mizar Users

definition

{ r where r is positive Rational : verum } is non empty Subset of REAL+
end;

func RATPLUS -> non empty Subset of REAL+ equals :: MUSIC_S1:def 1

{ r where r is positive Rational : verum } ;

coherence { r where r is positive Rational : verum } ;

{ r where r is positive Rational : verum } is non empty Subset of REAL+

proof end;

:: deftheorem defines RATPLUS MUSIC_S1:def 1 :

RATPLUS = { r where r is positive Rational : verum } ;

RATPLUS = { r where r is positive Rational : verum } ;

definition

attr c_{1} is strict ;

struct MusicStruct -> 1-sorted ;

aggr MusicStruct(# carrier, Equidistance, Ratio #) -> MusicStruct ;

sel Equidistance c_{1} -> Relation of [: the carrier of c_{1}, the carrier of c_{1}:],[: the carrier of c_{1}, the carrier of c_{1}:];

sel Ratio c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier of c_{1};

end;
struct MusicStruct -> 1-sorted ;

aggr MusicStruct(# carrier, Equidistance, Ratio #) -> MusicStruct ;

sel Equidistance c

sel Ratio c

:: deftheorem defines equiv MUSIC_S1:def 3 :

for S being MusicStruct

for a, b, c, d being Element of S holds

( a,b equiv c,d iff [[a,b],[c,d]] in the Equidistance of S );

for S being MusicStruct

for a, b, c, d being Element of S holds

( a,b equiv c,d iff [[a,b],[c,d]] in the Equidistance of S );

definition

let x, y be Element of REALPLUS ;

ex b_{1} being Element of REALPLUS ex r, s being positive Real st

( x = r & s = y & b_{1} = s / r )

for b_{1}, b_{2} being Element of REALPLUS st ex r, s being positive Real st

( x = r & s = y & b_{1} = s / r ) & ex r, s being positive Real st

( x = r & s = y & b_{2} = s / r ) holds

b_{1} = b_{2}
;

end;
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 );

existence ex r, s being positive Real st

( x = r & s = y & it = s / r );

ex b

( x = r & s = y & b

proof end;

uniqueness for b

( x = r & s = y & b

( x = r & s = y & b

b

:: deftheorem Def01 defines REAL_ratio MUSIC_S1:def 4 :

for x, y, b_{3} being Element of REALPLUS holds

( b_{3} = REAL_ratio (x,y) iff ex r, s being positive Real st

( x = r & s = y & b_{3} = s / r ) );

for x, y, b

( b

( x = r & s = y & b

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) )

( REAL_ratio (a,b) = REAL_ratio (c,d) iff REAL_ratio (b,a) = REAL_ratio (d,c) )

proof end;

definition

ex b_{1} being Function of [:REALPLUS,REALPLUS:],REALPLUS st

for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st

( x = [y,z] & b_{1} . x = REAL_ratio (y,z) )

for b_{1}, b_{2} being Function of [:REALPLUS,REALPLUS:],REALPLUS st ( for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st

( x = [y,z] & b_{1} . x = REAL_ratio (y,z) ) ) & ( for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st

( x = [y,z] & b_{2} . x = REAL_ratio (y,z) ) ) holds

b_{1} = b_{2}
end;

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) );

existence for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st

( x = [y,z] & it . x = REAL_ratio (y,z) );

ex b

for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st

( x = [y,z] & b

proof end;

uniqueness for b

( x = [y,z] & b

( x = [y,z] & b

b

proof end;

:: deftheorem Def02 defines REAL_ratio MUSIC_S1:def 5 :

for b_{1} being Function of [:REALPLUS,REALPLUS:],REALPLUS holds

( b_{1} = REAL_ratio iff for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st

( x = [y,z] & b_{1} . x = REAL_ratio (y,z) ) );

for b

( b

( x = [y,z] & b

definition

ex b_{1} being Relation of [:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:] st

for x, y being Element of [:REALPLUS,REALPLUS:] holds

( [x,y] in b_{1} 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) ) )

for b_{1}, b_{2} being Relation of [:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:] st ( for x, y being Element of [:REALPLUS,REALPLUS:] holds

( [x,y] in b_{1} 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) ) ) ) & ( for x, y being Element of [:REALPLUS,REALPLUS:] holds

( [x,y] in b_{2} 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) ) ) ) holds

b_{1} = b_{2}
end;

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) ) );

existence 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) ) );

ex b

for x, y being Element of [:REALPLUS,REALPLUS:] holds

( [x,y] in b

( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) )

proof end;

uniqueness for b

( [x,y] in b

( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) ) ) & ( for x, y being Element of [:REALPLUS,REALPLUS:] holds

( [x,y] in b

( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) ) ) holds

b

proof end;

:: deftheorem Def03 defines EQUIV_REAL_ratio MUSIC_S1:def 6 :

for b_{1} being Relation of [:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:] holds

( b_{1} = EQUIV_REAL_ratio iff for x, y being Element of [:REALPLUS,REALPLUS:] holds

( [x,y] in b_{1} 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) ) ) );

for b

( b

( [x,y] in b

( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) ) );

definition

MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #) is MusicStruct ;

end;

func REAL_Music -> MusicStruct equals :: MUSIC_S1:def 7

MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #);

coherence MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #);

MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #) is MusicStruct ;

:: deftheorem defines REAL_Music MUSIC_S1:def 7 :

REAL_Music = MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #);

REAL_Music = MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #);

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) ) ) )

( 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

f2 = f3

proof end;

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])

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

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

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) )

( 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 ;

ex b_{1} being Element of RATPLUS ex r, s being positive Rational st

( x = r & s = y & b_{1} = s / r )

for b_{1}, b_{2} being Element of RATPLUS st ex r, s being positive Rational st

( x = r & s = y & b_{1} = s / r ) & ex r, s being positive Rational st

( x = r & s = y & b_{2} = s / r ) holds

b_{1} = b_{2}
;

end;
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 );

existence ex r, s being positive Rational st

( x = r & s = y & it = s / r );

ex b

( x = r & s = y & b

proof end;

uniqueness for b

( x = r & s = y & b

( x = r & s = y & b

b

:: deftheorem Def04 defines RAT_ratio MUSIC_S1:def 8 :

for x, y, b_{3} being Element of RATPLUS holds

( b_{3} = RAT_ratio (x,y) iff ex r, s being positive Rational st

( x = r & s = y & b_{3} = s / r ) );

for x, y, b

( b

( x = r & s = y & b

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) )

( RAT_ratio (a,b) = RAT_ratio (c,d) iff RAT_ratio (b,a) = RAT_ratio (d,c) )

proof end;

definition

ex b_{1} being Function of [:RATPLUS,RATPLUS:],RATPLUS st

for x being Element of [:RATPLUS,RATPLUS:] ex y, z being Element of RATPLUS st

( x = [y,z] & b_{1} . x = RAT_ratio (y,z) )

for b_{1}, b_{2} being Function of [:RATPLUS,RATPLUS:],RATPLUS st ( for x being Element of [:RATPLUS,RATPLUS:] ex y, z being Element of RATPLUS st

( x = [y,z] & b_{1} . x = RAT_ratio (y,z) ) ) & ( for x being Element of [:RATPLUS,RATPLUS:] ex y, z being Element of RATPLUS st

( x = [y,z] & b_{2} . x = RAT_ratio (y,z) ) ) holds

b_{1} = b_{2}
end;

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) );

existence for x being Element of [:RATPLUS,RATPLUS:] ex y, z being Element of RATPLUS st

( x = [y,z] & it . x = RAT_ratio (y,z) );

ex b

for x being Element of [:RATPLUS,RATPLUS:] ex y, z being Element of RATPLUS st

( x = [y,z] & b

proof end;

uniqueness for b

( x = [y,z] & b

( x = [y,z] & b

b

proof end;

:: deftheorem Def05 defines RAT_ratio MUSIC_S1:def 9 :

for b_{1} being Function of [:RATPLUS,RATPLUS:],RATPLUS holds

( b_{1} = RAT_ratio iff for x being Element of [:RATPLUS,RATPLUS:] ex y, z being Element of RATPLUS st

( x = [y,z] & b_{1} . x = RAT_ratio (y,z) ) );

for b

( b

( x = [y,z] & b

definition

ex b_{1} being Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] st

for x, y being Element of [:RATPLUS,RATPLUS:] holds

( [x,y] in b_{1} 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) ) )

for b_{1}, b_{2} being Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] st ( for x, y being Element of [:RATPLUS,RATPLUS:] holds

( [x,y] in b_{1} 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) ) ) ) & ( for x, y being Element of [:RATPLUS,RATPLUS:] holds

( [x,y] in b_{2} 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) ) ) ) holds

b_{1} = b_{2}
end;

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) ) );

existence 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) ) );

ex b

for x, y being Element of [:RATPLUS,RATPLUS:] holds

( [x,y] in b

( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) )

proof end;

uniqueness for b

( [x,y] in b

( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) ) ) & ( for x, y being Element of [:RATPLUS,RATPLUS:] holds

( [x,y] in b

( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) ) ) holds

b

proof end;

:: deftheorem Def06 defines EQUIV_RAT_ratio MUSIC_S1:def 10 :

for b_{1} being Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] holds

( b_{1} = EQUIV_RAT_ratio iff for x, y being Element of [:RATPLUS,RATPLUS:] holds

( [x,y] in b_{1} 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) ) ) );

for b

( b

( [x,y] in b

( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) ) );

definition

MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #) is MusicStruct ;

end;

func RAT_Music -> MusicStruct equals :: MUSIC_S1:def 11

MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #);

coherence MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #);

MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #) is MusicStruct ;

:: deftheorem defines RAT_Music MUSIC_S1:def 11 :

RAT_Music = MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #);

RAT_Music = MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #);

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) ) ) )

( 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

f2 = f3

proof end;

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])

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

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 ) )

( 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

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) )

( 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 ;

end;
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) );

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;

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;

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) );

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_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]);

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]);

:: deftheorem Def07a defines satisfying_Real MUSIC_S1:def 12 :

for S being MusicStruct holds

( S is satisfying_Real iff the carrier of S c= REALPLUS );

for S being MusicStruct holds

( S is satisfying_Real iff the carrier of S c= REALPLUS );

:: deftheorem Def08a defines satisfying_equiv MUSIC_S1:def 13 :

for S being MusicStruct holds

( S is satisfying_equiv iff 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) ) );

for S being MusicStruct holds

( S is satisfying_equiv iff 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) ) );

:: deftheorem Def09a defines satisfying_interval MUSIC_S1:def 14 :

for S being MusicStruct holds

( S is satisfying_interval iff for f1, f2, f3 being Element of S st the Ratio of S . (f1,f2) = the Ratio of S . (f1,f3) holds

f2 = f3 );

for S being MusicStruct holds

( S is satisfying_interval iff for f1, f2, f3 being Element of S st the Ratio of S . (f1,f2) = the Ratio of S . (f1,f3) holds

f2 = f3 );

:: deftheorem Def10a defines satisfying_tonic MUSIC_S1:def 15 :

for S being MusicStruct holds

( S is satisfying_tonic iff for f1, f2, f3 being Element of S st the Ratio of S . (f1,f1) = the Ratio of S . (f2,f3) holds

f2 = f3 );

for S being MusicStruct holds

( S is satisfying_tonic iff for f1, f2, f3 being Element of S st the Ratio of S . (f1,f1) = the Ratio of S . (f2,f3) holds

f2 = f3 );

:: deftheorem Def11a defines satisfying_commutativity MUSIC_S1:def 16 :

for S being MusicStruct holds

( S is satisfying_commutativity iff 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) ) );

for S being MusicStruct holds

( S is satisfying_commutativity iff 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) ) );

:: deftheorem Def12a defines satisfying_Nat MUSIC_S1:def 17 :

for S being MusicStruct holds

( S is satisfying_Nat iff NATPLUS c= the carrier of S );

for S being MusicStruct holds

( S is satisfying_Nat iff NATPLUS c= the carrier of S );

:: deftheorem Def13a defines satisfying_harmonic_closed MUSIC_S1:def 18 :

for S being MusicStruct holds

( S is satisfying_harmonic_closed iff 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]) );

for S being MusicStruct holds

( S is satisfying_harmonic_closed iff 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]) );

registration

ex b_{1} being MusicStruct st

( b_{1} is satisfying_harmonic_closed & b_{1} is satisfying_Nat & b_{1} is satisfying_commutativity & b_{1} is satisfying_tonic & b_{1} is satisfying_interval & b_{1} is satisfying_equiv & b_{1} is satisfying_Real & not b_{1} is empty )
end;

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

existence ex b

( b

proof 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 MusicStruct ;

coherence

REAL_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct

end;
redefine func REAL_Music -> non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct ;

coherence

REAL_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct

proof 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 MusicStruct ;

coherence

RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct

end;
redefine func RAT_Music -> non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct ;

coherence

RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct

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 )

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

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 )

for a, b, c being Element of S holds

( a,b equiv a,c iff b = c )

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:] )

( 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 )

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

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;

ex b_{1} being Element of S st [frequency,b_{1}] in Class ( the Equidistance of S,[1,n])
by Def13a;

uniqueness

for b_{1}, b_{2} being Element of S st [frequency,b_{1}] in Class ( the Equidistance of S,[1,n]) & [frequency,b_{2}] in Class ( the Equidistance of S,[1,n]) holds

b_{1} = b_{2}

end;
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 [frequency,it] in Class ( the Equidistance of S,[1,n]);

ex b

uniqueness

for b

b

proof end;

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

for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of S

for n being non zero Nat

for b_{4} being Element of S holds

( b_{4} = n -harmonique (S,frequency) iff [frequency,b_{4}] in Class ( the Equidistance of S,[1,n]) );

for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of S

for n being non zero Nat

for b

( b

definition

let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

end;
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 );

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 );

:: deftheorem Def09 defines satisfying_linearite_harmonique MUSIC_S1:def 20 :

for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds

( S is satisfying_linearite_harmonique iff 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 ) );

for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds

( S is satisfying_linearite_harmonique iff 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 ) );

registration

ex b_{1} being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct st b_{1} is satisfying_linearite_harmonique
by Th30;

end;

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

existence ex b

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 MusicStruct ;

coherence

REAL_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique MusicStruct by Th30;

end;
redefine func REAL_Music -> non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique MusicStruct ;

coherence

REAL_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique MusicStruct by Th30;

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 MusicStruct ;

coherence

RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique MusicStruct by Th31;

end;
redefine func RAT_Music -> non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique MusicStruct ;

coherence

RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique MusicStruct by Th31;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

end;
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);

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);

:: deftheorem Def10 defines satisfying_harmonique_stable MUSIC_S1:def 21 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds

( MS is satisfying_harmonique_stable iff 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) );

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds

( MS is satisfying_harmonique_stable iff 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) );

registration

ex b_{1} being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique MusicStruct st b_{1} is satisfying_harmonique_stable
by Th32;

end;

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

existence ex b

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 MusicStruct ;

coherence

REAL_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct by Th32;

end;
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 MusicStruct ;

coherence

REAL_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct by Th32;

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 MusicStruct ;

coherence

RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct by Th33;

end;
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 MusicStruct ;

coherence

RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct by Th33;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

let frequency be Element of MS;

Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(1 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(2 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(2 -harmonique (MS,frequency)),(3 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(4 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(4 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(6 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(8 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(8 -harmonique (MS,frequency)),(9 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[(9 -harmonique (MS,frequency)),(10 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

end;
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))]);

coherence Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(1 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(1 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(2 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(2 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(2 -harmonique (MS,frequency)),(3 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(2 -harmonique (MS,frequency)),(3 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(4 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(4 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(4 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(4 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(6 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(6 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(8 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(8 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(8 -harmonique (MS,frequency)),(9 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(8 -harmonique (MS,frequency)),(9 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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))]);

coherence Class ( the Equidistance of MS,[(9 -harmonique (MS,frequency)),(10 -harmonique (MS,frequency))]);

Class ( the Equidistance of MS,[(9 -harmonique (MS,frequency)),(10 -harmonique (MS,frequency))]) is Subset of [: the carrier of MS, the carrier of MS:] ;

:: deftheorem defines unison MUSIC_S1:def 22 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds unison (MS,frequency) = Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(1 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds unison (MS,frequency) = Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(1 -harmonique (MS,frequency))]);

:: deftheorem defines octave MUSIC_S1:def 23 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds octave (MS,frequency) = Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(2 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds octave (MS,frequency) = Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(2 -harmonique (MS,frequency))]);

:: deftheorem defines fifth MUSIC_S1:def 24 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds fifth (MS,frequency) = Class ( the Equidistance of MS,[(2 -harmonique (MS,frequency)),(3 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds fifth (MS,frequency) = Class ( the Equidistance of MS,[(2 -harmonique (MS,frequency)),(3 -harmonique (MS,frequency))]);

:: deftheorem defines fourth MUSIC_S1:def 25 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds fourth (MS,frequency) = Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(4 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds fourth (MS,frequency) = Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(4 -harmonique (MS,frequency))]);

:: deftheorem defines major_sixth MUSIC_S1:def 26 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds major_sixth (MS,frequency) = Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds major_sixth (MS,frequency) = Class ( the Equidistance of MS,[(3 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]);

:: deftheorem defines major_third MUSIC_S1:def 27 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds major_third (MS,frequency) = Class ( the Equidistance of MS,[(4 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds major_third (MS,frequency) = Class ( the Equidistance of MS,[(4 -harmonique (MS,frequency)),(5 -harmonique (MS,frequency))]);

:: deftheorem defines minor_third MUSIC_S1:def 28 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds minor_third (MS,frequency) = Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(6 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds minor_third (MS,frequency) = Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(6 -harmonique (MS,frequency))]);

:: deftheorem defines minor_sixth MUSIC_S1:def 29 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds minor_sixth (MS,frequency) = Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(8 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds minor_sixth (MS,frequency) = Class ( the Equidistance of MS,[(5 -harmonique (MS,frequency)),(8 -harmonique (MS,frequency))]);

:: deftheorem defines major_tone MUSIC_S1:def 30 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds major_tone (MS,frequency) = Class ( the Equidistance of MS,[(8 -harmonique (MS,frequency)),(9 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds major_tone (MS,frequency) = Class ( the Equidistance of MS,[(8 -harmonique (MS,frequency)),(9 -harmonique (MS,frequency))]);

:: deftheorem defines minor_tone MUSIC_S1:def 31 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds minor_tone (MS,frequency) = Class ( the Equidistance of MS,[(9 -harmonique (MS,frequency)),(10 -harmonique (MS,frequency))]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct

for frequency being Element of MS holds minor_tone (MS,frequency) = Class ( the Equidistance of MS,[(9 -harmonique (MS,frequency)),(10 -harmonique (MS,frequency))]);

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

Class ( the Equidistance of MS,[1,1]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[1,2]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[2,3]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[3,4]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[3,5]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[4,5]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[5,6]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[5,8]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[8,9]) is Subset of [: the carrier of MS, the carrier of MS:] ;

Class ( the Equidistance of MS,[9,10]) is Subset of [: the carrier of MS, the carrier of MS:] ;

end;
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]);

coherence Class ( the Equidistance of MS,[1,1]);

Class ( the Equidistance of MS,[1,1]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[1,2]);

Class ( the Equidistance of MS,[1,2]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[2,3]);

Class ( the Equidistance of MS,[2,3]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[3,4]);

Class ( the Equidistance of MS,[3,4]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[3,5]);

Class ( the Equidistance of MS,[3,5]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[4,5]);

Class ( the Equidistance of MS,[4,5]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[5,6]);

Class ( the Equidistance of MS,[5,6]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[5,8]);

Class ( the Equidistance of MS,[5,8]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[8,9]);

Class ( the Equidistance of MS,[8,9]) is Subset of [: the carrier of MS, the carrier of MS:] ;

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]);

coherence Class ( the Equidistance of MS,[9,10]);

Class ( the Equidistance of MS,[9,10]) is Subset of [: the carrier of MS, the carrier of MS:] ;

:: deftheorem defines unison MUSIC_S1:def 32 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds unison MS = Class ( the Equidistance of MS,[1,1]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds unison MS = Class ( the Equidistance of MS,[1,1]);

:: deftheorem defines octave MUSIC_S1:def 33 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds octave MS = Class ( the Equidistance of MS,[1,2]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds octave MS = Class ( the Equidistance of MS,[1,2]);

:: deftheorem defines fifth MUSIC_S1:def 34 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds fifth MS = Class ( the Equidistance of MS,[2,3]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds fifth MS = Class ( the Equidistance of MS,[2,3]);

:: deftheorem defines fourth MUSIC_S1:def 35 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds fourth MS = Class ( the Equidistance of MS,[3,4]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds fourth MS = Class ( the Equidistance of MS,[3,4]);

:: deftheorem defines major_sixth MUSIC_S1:def 36 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds major_sixth MS = Class ( the Equidistance of MS,[3,5]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds major_sixth MS = Class ( the Equidistance of MS,[3,5]);

:: deftheorem defines major_third MUSIC_S1:def 37 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds major_third MS = Class ( the Equidistance of MS,[4,5]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds major_third MS = Class ( the Equidistance of MS,[4,5]);

:: deftheorem defines minor_third MUSIC_S1:def 38 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds minor_third MS = Class ( the Equidistance of MS,[5,6]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds minor_third MS = Class ( the Equidistance of MS,[5,6]);

:: deftheorem defines minor_sixth MUSIC_S1:def 39 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds minor_sixth MS = Class ( the Equidistance of MS,[5,8]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds minor_sixth MS = Class ( the Equidistance of MS,[5,8]);

:: deftheorem defines major_tone MUSIC_S1:def 40 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds major_tone MS = Class ( the Equidistance of MS,[8,9]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds major_tone MS = Class ( the Equidistance of MS,[8,9]);

:: deftheorem defines minor_tone MUSIC_S1:def 41 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds minor_tone MS = Class ( the Equidistance of MS,[9,10]);

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds minor_tone MS = Class ( the Equidistance of MS,[9,10]);

definition

let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

end;
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;

for frequency being Element of S ex q being Element of S st [frequency,q] in fifth S;

:: deftheorem Def11 defines satisfying_fifth_constructible MUSIC_S1:def 42 :

for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds

( S is satisfying_fifth_constructible iff for frequency being Element of S ex q being Element of S st [frequency,q] in fifth S );

for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds

( S is satisfying_fifth_constructible iff for frequency being Element of S ex q being Element of S st [frequency,q] in fifth S );

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 )

( fr = frequency & qr = (3 / 2) * fr & [fr,qr] in fifth REAL_Music )

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 )

( fr = frequency & qr = (3 / 2) * fr & [fr,qr] in fifth RAT_Music )

proof end;

registration

ex b_{1} being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct st b_{1} is satisfying_fifth_constructible
by Th35;

end;

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 for MusicStruct ;

existence ex b

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 MusicStruct ;

coherence

REAL_Music 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 MusicStruct by Th35;

end;
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 MusicStruct ;

coherence

REAL_Music 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 MusicStruct by Th35;

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 MusicStruct ;

coherence

RAT_Music 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 MusicStruct by Th37;

end;
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 MusicStruct ;

coherence

RAT_Music 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 MusicStruct by Th37;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct ;

let frequency be Element of MS;

ex b_{1} being Element of MS st [frequency,b_{1}] in fifth MS
by Def11;

uniqueness

for b_{1}, b_{2} being Element of MS st [frequency,b_{1}] in fifth MS & [frequency,b_{2}] in fifth MS holds

b_{1} = b_{2}

end;
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 [frequency,it] in fifth MS;

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def11bis defines Fifth MUSIC_S1:def 43 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct

for frequency, b_{3} being Element of MS holds

( b_{3} = Fifth (MS,frequency) iff [frequency,b_{3}] in fifth MS );

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct

for frequency, b

( b

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

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 )

( 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 )

( 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 ;

end;
:: deftheorem Def12 defines classical_fifth MUSIC_S1:def 44 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct holds

( MS is classical_fifth iff for frequency being Element of MS ex fr being positive Real st

( frequency = fr & Fifth (MS,frequency) = (3 / 2) * fr ) );

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct holds

( MS is classical_fifth iff for frequency being Element of MS ex fr being positive Real st

( frequency = fr & Fifth (MS,frequency) = (3 / 2) * fr ) );

registration

ex b_{1} being 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 MusicStruct st b_{1} is classical_fifth
end;

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 for MusicStruct ;

existence ex b

proof 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 MusicStruct ;

coherence

REAL_Music 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 MusicStruct by Def12, Th38;

end;
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 MusicStruct ;

coherence

REAL_Music 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 MusicStruct by Def12, Th38;

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 MusicStruct ;

coherence

RAT_Music 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 MusicStruct

end;
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 MusicStruct ;

coherence

RAT_Music 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 MusicStruct

proof 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

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

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

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 ) )

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;

end;
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 );

ex r1, r2, r3 being positive Real st

( a = r1 & b = r2 & c = r3 & r1 <= r2 & r2 < r3 );

:: deftheorem defines is_Between MUSIC_S1:def 45 :

for MS being MusicStruct

for a, b, c being Element of MS holds

( b is_Between a,c iff ex r1, r2, r3 being positive Real st

( a = r1 & b = r2 & c = r3 & r1 <= r2 & r2 < r3 ) );

for MS being MusicStruct

for a, b, c being Element of MS holds

( b is_Between a,c iff ex r1, r2, r3 being positive Real st

( a = r1 & b = r2 & c = r3 & r1 <= r2 & r2 < r3 ) );

definition

let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;

end;
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;

for frequency being Element of S ex o being Element of S st [frequency,o] in octave S;

:: deftheorem Def13 defines satisfying_octave_constructible MUSIC_S1:def 46 :

for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds

( S is satisfying_octave_constructible iff for frequency being Element of S ex o being Element of S st [frequency,o] in octave S );

for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds

( S is satisfying_octave_constructible iff for frequency being Element of S ex o being Element of S st [frequency,o] in octave S );

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 )

( fr = frequency & qr = 2 * fr & [fr,qr] in octave REAL_Music )

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 )

( fr = frequency & qr = 2 * fr & [fr,qr] in octave RAT_Music )

proof end;

registration

ex b_{1} being 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 MusicStruct st b_{1} is satisfying_octave_constructible
by Th42;

end;

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 for MusicStruct ;

existence ex b

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 MusicStruct ;

coherence

REAL_Music 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 MusicStruct by Th42;

end;
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 MusicStruct ;

coherence

REAL_Music 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 MusicStruct by Th42;

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 MusicStruct ;

coherence

RAT_Music 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 MusicStruct by Th44;

end;
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 MusicStruct ;

coherence

RAT_Music 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 MusicStruct by Th44;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct ;

let frequency be Element of MS;

ex b_{1} being Element of MS st [frequency,b_{1}] in octave MS
by Def13;

uniqueness

for b_{1}, b_{2} being Element of MS st [frequency,b_{1}] in octave MS & [frequency,b_{2}] in octave MS holds

b_{1} = b_{2}

end;
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 [frequency,it] in octave MS;

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def14 defines Octave MUSIC_S1:def 47 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct

for frequency, b_{3} being Element of MS holds

( b_{3} = Octave (MS,frequency) iff [frequency,b_{3}] in octave MS );

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct

for frequency, b

( b

definition

let MS be non empty satisfying_Real MusicStruct ;

let r be Element of MS;

coherence

r is positive Real

end;
let r be Element of MS;

coherence

r is positive Real

proof end;

:: deftheorem defines @ MUSIC_S1:def 48 :

for MS being non empty satisfying_Real MusicStruct

for r being Element of MS holds @ r = r;

for MS being non empty satisfying_Real MusicStruct

for r being Element of MS holds @ r = r;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct ;

end;
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 );

for frequency being Element of MS ex fr being positive Real st

( frequency = fr & Octave (MS,frequency) = 2 * fr );

:: deftheorem Def15 defines classical_octave MUSIC_S1:def 49 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct holds

( MS is classical_octave iff for frequency being Element of MS ex fr being positive Real st

( frequency = fr & Octave (MS,frequency) = 2 * fr ) );

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct holds

( MS is classical_octave iff for frequency being Element of MS ex fr being positive Real st

( frequency = fr & Octave (MS,frequency) = 2 * fr ) );

registration

ex b_{1} being 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 MusicStruct st b_{1} is classical_octave
by Th45;

end;

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 for MusicStruct ;

existence ex b

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 MusicStruct ;

coherence

REAL_Music 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 MusicStruct by Th45;

end;
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 MusicStruct ;

coherence

REAL_Music 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 MusicStruct by Th45;

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 MusicStruct ;

coherence

RAT_Music 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 MusicStruct by Th46;

end;
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 MusicStruct ;

coherence

RAT_Music 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 MusicStruct by Th46;

definition

let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct ;

end;
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;

for frequency being Element of MS ex o being Element of MS st [o,frequency] in octave MS;

:: deftheorem Def16 defines satisfying_octave_descendent_constructible MUSIC_S1:def 50 :

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct holds

( MS is satisfying_octave_descendent_constructible iff for frequency being Element of MS ex o being Element of MS st [o,frequency] in octave MS );

for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct holds

( MS is satisfying_octave_descendent_constructible iff for frequency being Element of MS ex o being Element of MS st [o,frequency] in octave MS );

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 )

( fr = frequency & qr = (1 / 2) * fr & [qr,fr] in octave REAL_Music )

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 )

( fr = frequency & qr = (1 / 2) * fr & [qr,fr] in octave RAT_Music )

proof end;

registration

ex b_{1} being 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 MusicStruct st b_{1} is satisfying_octave_descendent_constructible
by Th48;

end;

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 ex b

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

REAL_Music 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 by Th48;

end;
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

REAL_Music 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 by Th48;

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

RAT_Music 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 by Th50;

end;
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

RAT_Music 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 by Th50;

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;

ex b_{1} being Element of MS st [b_{1},frequency] in octave MS
by Def16;

uniqueness

for b_{1}, b_{2} being Element of MS st [b_{1},frequency] in octave MS & [b_{2},frequency] in octave MS holds

b_{1} = b_{2}

end;
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 [it,frequency] in octave MS;

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def17 defines Octave_descendent MUSIC_S1:def 51 :

for MS being satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct

for frequency, b_{3} being Element of MS holds

( b_{3} = Octave_descendent (MS,frequency) iff [b_{3},frequency] in octave MS );

for MS being satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct

for frequency, b

( b

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 )

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) )

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)

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

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 fondamentale, frequency be Element of MS;

coherence

( ( Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth (MS,frequency) is Element of MS ) & ( not Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth (MS,frequency))) is Element of MS ) );

consistency

for b_{1} being Element of MS holds verum;

;

end;
let fondamentale, frequency be Element of MS;

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 Fifth (MS,frequency) if Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale)

otherwise Octave_descendent (MS,(Fifth (MS,frequency)));

coherence

( ( Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth (MS,frequency) is Element of MS ) & ( not Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth (MS,frequency))) is Element of MS ) );

consistency

for b

;

:: deftheorem Def18 defines Fifth_reduct MUSIC_S1:def 52 :

for MS being 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 holds

( ( Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,frequency) = Fifth (MS,frequency) ) & ( not Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,frequency) = Octave_descendent (MS,(Fifth (MS,frequency))) ) );

for MS being 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 holds

( ( Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,frequency) = Fifth (MS,frequency) ) & ( not Fifth (MS,frequency) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,frequency) = Octave_descendent (MS,(Fifth (MS,frequency))) ) );

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)

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 )

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 )

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)

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 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)) ) )

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;

ex b_{1} being sequence of MS st

( b_{1} . 0 = frequency & ( for n being Nat holds b_{1} . (n + 1) = Fifth_reduct (MS,fondamentale,(b_{1} . n)) ) )
by Th56BIS;

uniqueness

for b_{1}, b_{2} being sequence of MS st b_{1} . 0 = frequency & ( for n being Nat holds b_{1} . (n + 1) = Fifth_reduct (MS,fondamentale,(b_{1} . n)) ) & b_{2} . 0 = frequency & ( for n being Nat holds b_{2} . (n + 1) = Fifth_reduct (MS,fondamentale,(b_{2} . n)) ) holds

b_{1} = b_{2}

end;
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 ( it . 0 = frequency & ( for n being Nat holds it . (n + 1) = Fifth_reduct (MS,fondamentale,(it . n)) ) );

ex b

( b

uniqueness

for b

b

proof end;

:: deftheorem Def19 defines spiral_of_fifths MUSIC_S1:def 53 :

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

for b_{4} being sequence of MS holds

( b_{4} = spiral_of_fifths (MS,fondamentale,frequency) iff ( b_{4} . 0 = frequency & ( for n being Nat holds b_{4} . (n + 1) = Fifth_reduct (MS,fondamentale,(b_{4} . n)) ) ) );

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

for b

( b

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)

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)

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)

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)

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)

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)

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)

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)

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

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

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

for frequency being Element of MS holds (@ (Octave (MS,frequency))) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) = 32 / 27

proof end;

:: deftheorem defines monotonic MUSIC_S1:def 54 :

for MS being MusicSpace

for scale being Element of 2 -tuples_on the carrier of MS holds

( scale is monotonic iff 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) ) );

for MS being MusicSpace

for scale being Element of 2 -tuples_on the carrier of MS holds

( scale is monotonic iff 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) ) );

:: deftheorem defines ditonic MUSIC_S1:def 55 :

for MS being MusicSpace

for scale being Element of 3 -tuples_on the carrier of MS holds

( scale is ditonic iff 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) ) );

for MS being MusicSpace

for scale being Element of 3 -tuples_on the carrier of MS holds

( scale is ditonic iff 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) ) );

:: deftheorem defines tritonic MUSIC_S1:def 56 :

for MS being MusicSpace

for scale being Element of 4 -tuples_on the carrier of MS holds

( scale is tritonic iff 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) ) );

for MS being MusicSpace

for scale being Element of 4 -tuples_on the carrier of MS holds

( scale is tritonic iff 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) ) );

definition

let MS be MusicSpace;

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

end;
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) );

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) );

:: deftheorem defines tetratonic MUSIC_S1:def 57 :

for MS being MusicSpace

for scale being Element of 5 -tuples_on the carrier of MS holds

( scale is tetratonic iff 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) ) );

for MS being MusicSpace

for scale being Element of 5 -tuples_on the carrier of MS holds

( scale is tetratonic iff 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) ) );

definition

let MS be MusicSpace;

let n be natural Number ;

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

end;
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) ) );

( 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) ) );

:: deftheorem defines pentatonic MUSIC_S1:def 58 :

for MS being MusicSpace

for n being natural Number

for scale being Element of n -tuples_on the carrier of MS holds

( scale is pentatonic iff ( 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) ) ) );

for MS being MusicSpace

for n being natural Number

for scale being Element of n -tuples_on the carrier of MS holds

( scale is pentatonic iff ( 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) ) ) );

definition

let MS be MusicSpace;

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

end;
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) );

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) );

:: deftheorem defines hexatonic MUSIC_S1:def 59 :

for MS being MusicSpace

for scale being Element of 7 -tuples_on the carrier of MS holds

( scale is hexatonic iff 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) ) );

for MS being MusicSpace

for scale being Element of 7 -tuples_on the carrier of MS holds

( scale is hexatonic iff 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) ) );

definition

let MS be MusicSpace;

let n be natural Number ;

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

end;
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) ) );

( 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) ) );

:: deftheorem defines heptatonic MUSIC_S1:def 60 :

for MS being MusicSpace

for n being natural Number

for scale being Element of n -tuples_on the carrier of MS holds

( scale is heptatonic iff ( 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) ) ) );

for MS being MusicSpace

for n being natural Number

for scale being Element of n -tuples_on the carrier of MS holds

( scale is heptatonic iff ( 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) ) ) );

definition

let MS be MusicSpace;

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

end;
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) );

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) );

:: deftheorem defines octatonic MUSIC_S1:def 61 :

for MS being MusicSpace

for scale being Element of 9 -tuples_on the carrier of MS holds

( scale is octatonic iff 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) ) );

for MS being MusicSpace

for scale being Element of 9 -tuples_on the carrier of MS holds

( scale is octatonic iff 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) ) );

definition

let MS be MusicSpace;

let frequency be Element of MS;

ex b_{1} being Element of 6 -tuples_on the carrier of MS st

( b_{1} . 1 = frequency & b_{1} . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b_{1} . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b_{1} . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b_{1} . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b_{1} . 6 = Octave (MS,frequency) )

for b_{1}, b_{2} being Element of 6 -tuples_on the carrier of MS st b_{1} . 1 = frequency & b_{1} . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b_{1} . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b_{1} . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b_{1} . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b_{1} . 6 = Octave (MS,frequency) & b_{2} . 1 = frequency & b_{2} . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b_{2} . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b_{2} . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b_{2} . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b_{2} . 6 = Octave (MS,frequency) holds

b_{1} = b_{2}

end;
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) );

existence ( 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) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def20 defines pentatonic_pythagorean_scale MUSIC_S1:def 62 :

for MS being MusicSpace

for frequency being Element of MS

for b_{3} being Element of 6 -tuples_on the carrier of MS holds

( b_{3} = pentatonic_pythagorean_scale (MS,frequency) iff ( b_{3} . 1 = frequency & b_{3} . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b_{3} . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b_{3} . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b_{3} . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b_{3} . 6 = Octave (MS,frequency) ) );

for MS being MusicSpace

for frequency being Element of MS

for b

( b

theorem Th67: :: MUSIC_S1:83

for MS being MusicSpace

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

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;

ex b_{1}, r1, r2 being positive Real st

( r1 = f1 & r2 = f2 & b_{1} = r2 / r1 )

for b_{1}, b_{2} being positive Real st ex r1, r2 being positive Real st

( r1 = f1 & r2 = f2 & b_{1} = r2 / r1 ) & ex r1, r2 being positive Real st

( r1 = f1 & r2 = f2 & b_{2} = r2 / r1 ) holds

b_{1} = b_{2}
;

end;
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 );

existence ex r1, r2 being positive Real st

( r1 = f1 & r2 = f2 & it = r2 / r1 );

ex b

( r1 = f1 & r2 = f2 & b

proof end;

uniqueness for b

( r1 = f1 & r2 = f2 & b

( r1 = f1 & r2 = f2 & b

b

:: deftheorem Def21 defines intrval MUSIC_S1:def 63 :

for MS being MusicSpace

for f1, f2 being Element of MS

for b_{4} being positive Real holds

( b_{4} = intrval (f1,f2) iff ex r1, r2 being positive Real st

( r1 = f1 & r2 = f2 & b_{4} = r2 / r1 ) );

for MS being MusicSpace

for f1, f2 being Element of MS

for b

( b

( r1 = f1 & r2 = f2 & b

:: deftheorem defines pentatonic_pythagorean_semiditone MUSIC_S1:def 65 :

pentatonic_pythagorean_semiditone = 32 / 27;

pentatonic_pythagorean_semiditone = 32 / 27;

definition

pythagorean_tone * pythagorean_tone is positive Real ;

end;

func major_third_pythagorean_tone -> positive Real equals :: MUSIC_S1:def 66

pythagorean_tone * pythagorean_tone;

coherence pythagorean_tone * pythagorean_tone;

pythagorean_tone * pythagorean_tone is positive Real ;

:: deftheorem defines major_third_pythagorean_tone MUSIC_S1:def 66 :

major_third_pythagorean_tone = pythagorean_tone * pythagorean_tone;

major_third_pythagorean_tone = pythagorean_tone * pythagorean_tone;

definition

major_third_pythagorean_tone / pure_major_third is positive Real ;

end;

func syntonic_comma -> positive Real equals :: MUSIC_S1:def 68

major_third_pythagorean_tone / pure_major_third;

coherence major_third_pythagorean_tone / pure_major_third;

major_third_pythagorean_tone / pure_major_third is positive Real ;

:: deftheorem defines syntonic_comma MUSIC_S1:def 68 :

syntonic_comma = major_third_pythagorean_tone / pure_major_third;

syntonic_comma = major_third_pythagorean_tone / pure_major_third;

theorem :: MUSIC_S1:86

definition

let MS be MusicSpace;

let frequency be Element of MS;

(pentatonic_pythagorean_scale (MS,frequency)) . 1 is Element of MS by Def20;

(pentatonic_pythagorean_scale (MS,frequency)) . 2 is Element of MS

(pentatonic_pythagorean_scale (MS,frequency)) . 3 is Element of MS

(pentatonic_pythagorean_scale (MS,frequency)) . 4 is Element of MS

(pentatonic_pythagorean_scale (MS,frequency)) . 5 is Element of MS

Octave (MS,frequency) is Element of MS ;

end;
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 (pentatonic_pythagorean_scale (MS,frequency)) . 1;

(pentatonic_pythagorean_scale (MS,frequency)) . 1 is Element of MS by Def20;

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

(pentatonic_pythagorean_scale (MS,frequency)) . 2;

coherence (pentatonic_pythagorean_scale (MS,frequency)) . 2;

(pentatonic_pythagorean_scale (MS,frequency)) . 2 is Element of MS

proof end;

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

(pentatonic_pythagorean_scale (MS,frequency)) . 3;

coherence (pentatonic_pythagorean_scale (MS,frequency)) . 3;

(pentatonic_pythagorean_scale (MS,frequency)) . 3 is Element of MS

proof end;

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

(pentatonic_pythagorean_scale (MS,frequency)) . 4;

coherence (pentatonic_pythagorean_scale (MS,frequency)) . 4;

(pentatonic_pythagorean_scale (MS,frequency)) . 4 is Element of MS

proof end;

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

(pentatonic_pythagorean_scale (MS,frequency)) . 5;

coherence (pentatonic_pythagorean_scale (MS,frequency)) . 5;

(pentatonic_pythagorean_scale (MS,frequency)) . 5 is Element of MS

proof end;

coherence Octave (MS,frequency) is Element of MS ;

:: deftheorem defines penta_fondamentale MUSIC_S1:def 69 :

for MS being MusicSpace

for frequency being Element of MS holds penta_fondamentale (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 1;

for MS being MusicSpace

for frequency being Element of MS holds penta_fondamentale (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 1;

:: deftheorem defines penta_1 MUSIC_S1:def 70 :

for MS being MusicSpace

for frequency being Element of MS holds penta_1 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 2;

for MS being MusicSpace

for frequency being Element of MS holds penta_1 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 2;

:: deftheorem defines penta_2 MUSIC_S1:def 71 :

for MS being MusicSpace

for frequency being Element of MS holds penta_2 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 3;

for MS being MusicSpace

for frequency being Element of MS holds penta_2 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 3;

:: deftheorem defines penta_3 MUSIC_S1:def 72 :

for MS being MusicSpace

for frequency being Element of MS holds penta_3 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 4;

for MS being MusicSpace

for frequency being Element of MS holds penta_3 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 4;

:: deftheorem defines penta_4 MUSIC_S1:def 73 :

for MS being MusicSpace

for frequency being Element of MS holds penta_4 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 5;

for MS being MusicSpace

for frequency being Element of MS holds penta_4 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 5;

:: deftheorem defines penta_octave MUSIC_S1:def 74 :

for MS being MusicSpace

for frequency being Element of MS holds penta_octave (MS,frequency) = Octave (MS,frequency);

for MS being MusicSpace

for frequency being Element of MS holds penta_octave (MS,frequency) = Octave (MS,frequency);

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)

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 )

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 )

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: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 )

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)

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) )

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 ) )

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

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;

end;
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;

for frequency being Element of S ex q being Element of S st [frequency,q] in fourth S;

:: deftheorem Def22 defines satisfying_fourth_constructible MUSIC_S1:def 75 :

for S being MusicSpace holds

( S is satisfying_fourth_constructible iff for frequency being Element of S ex q being Element of S st [frequency,q] in fourth S );

for S being MusicSpace holds

( S is satisfying_fourth_constructible iff for frequency being Element of S ex q being Element of S st [frequency,q] in fourth S );

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 )

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;

registration

ex b_{1} being MusicSpace st b_{1} is satisfying_fourth_constructible
by Th79;

end;

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 satisfying_fourth_constructible for MusicStruct ;

existence ex b

definition

let MS be satisfying_fourth_constructible MusicSpace;

let frequency be Element of MS;

ex b_{1} being Element of MS st [frequency,b_{1}] in fourth MS
by Def22;

uniqueness

for b_{1}, b_{2} being Element of MS st [frequency,b_{1}] in fourth MS & [frequency,b_{2}] in fourth MS holds

b_{1} = b_{2}

end;
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 [frequency,it] in fourth MS;

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def23 defines Fourth MUSIC_S1:def 76 :

for MS being satisfying_fourth_constructible MusicSpace

for frequency, b_{3} being Element of MS holds

( b_{3} = Fourth (MS,frequency) iff [frequency,b_{3}] in fourth MS );

for MS being satisfying_fourth_constructible MusicSpace

for frequency, b

( b

:: deftheorem Def24 defines classical_fourth MUSIC_S1:def 77 :

for MS being satisfying_fourth_constructible MusicSpace holds

( MS is classical_fourth iff for frequency being Element of MS ex fr being positive Real st

( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr ) );

for MS being satisfying_fourth_constructible MusicSpace holds

( MS is classical_fourth iff for frequency being Element of MS ex fr being positive Real st

( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr ) );

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 )

for frequency being Element of MS ex fr being positive Real st

( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr )

proof end;

registration

ex b_{1} being satisfying_fourth_constructible MusicSpace st b_{1} is classical_fourth
end;

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 satisfying_fourth_constructible classical_fourth for MusicStruct ;

existence ex b

proof end;

definition

let MS be non empty satisfying_Real MusicStruct ;

end;
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);

for f1, f2 being Element of MS holds the Ratio of MS . (f1,f2) = (@ f2) / (@ f1);

:: deftheorem Def25 defines satisfying_euclidean MUSIC_S1:def 78 :

for MS being non empty satisfying_Real MusicStruct holds

( MS is satisfying_euclidean iff for f1, f2 being Element of MS holds the Ratio of MS . (f1,f2) = (@ f2) / (@ f1) );

for MS being non empty satisfying_Real MusicStruct holds

( MS is satisfying_euclidean iff for f1, f2 being Element of MS holds the Ratio of MS . (f1,f2) = (@ f2) / (@ f1) );

registration

existence

ex b_{1} being non empty satisfying_Real MusicStruct st b_{1} is satisfying_euclidean

end;
ex b

proof end;

registration

for b_{1} being non empty satisfying_Real MusicStruct st b_{1} is satisfying_euclidean holds

b_{1} is satisfying_interval
end;

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

coherence for b

b

proof end;

registration

for b_{1} being non empty satisfying_Real MusicStruct st b_{1} is satisfying_euclidean holds

b_{1} is satisfying_tonic
end;

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

coherence for b

b

proof end;

registration

for b_{1} being non empty satisfying_Real MusicStruct st b_{1} is satisfying_euclidean holds

b_{1} is satisfying_commutativity
end;

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

coherence for b

b

proof end;

registration

ex b_{1} being satisfying_fourth_constructible classical_fourth MusicSpace st b_{1} is satisfying_euclidean
end;

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 satisfying_fourth_constructible classical_fourth satisfying_euclidean for MusicStruct ;

existence ex b

proof end;

definition
end;

definition

let HPS be Heptatonic_Pythagorean_Score;

let frequency be Element of HPS;

ex b_{1} being Element of 8 -tuples_on the carrier of HPS st

( b_{1} . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & b_{1} . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & b_{1} . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & b_{1} . 4 = Fourth (HPS,frequency) & b_{1} . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & b_{1} . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & b_{1} . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & b_{1} . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) )

for b_{1}, b_{2} being Element of 8 -tuples_on the carrier of HPS st b_{1} . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & b_{1} . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & b_{1} . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & b_{1} . 4 = Fourth (HPS,frequency) & b_{1} . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & b_{1} . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & b_{1} . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & b_{1} . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) & b_{2} . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & b_{2} . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & b_{2} . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & b_{2} . 4 = Fourth (HPS,frequency) & b_{2} . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & b_{2} . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & b_{2} . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & b_{2} . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) holds

b_{1} = b_{2}

end;
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)) );

existence ( 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)) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def26 defines heptatonic_pythagorean_scale MUSIC_S1:def 79 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS

for b_{3} being Element of 8 -tuples_on the carrier of HPS holds

( b_{3} = heptatonic_pythagorean_scale (HPS,frequency) iff ( b_{3} . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & b_{3} . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & b_{3} . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & b_{3} . 4 = Fourth (HPS,frequency) & b_{3} . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & b_{3} . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & b_{3} . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & b_{3} . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) ) );

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS

for b

( b

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)

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;

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

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)

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)

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)

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)

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)

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) )

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

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

proof end;

:: deftheorem defines heptatonic_pythagorean_semitone MUSIC_S1:def 80 :

heptatonic_pythagorean_semitone = 256 / 243;

heptatonic_pythagorean_semitone = 256 / 243;

theorem :: MUSIC_S1:110

definition

let HPS be Heptatonic_Pythagorean_Score;

let frequency be Element of HPS;

(heptatonic_pythagorean_scale (HPS,frequency)) . 1 is Element of HPS

(heptatonic_pythagorean_scale (HPS,frequency)) . 2 is Element of HPS

(heptatonic_pythagorean_scale (HPS,frequency)) . 3 is Element of HPS

(heptatonic_pythagorean_scale (HPS,frequency)) . 4 is Element of HPS

(heptatonic_pythagorean_scale (HPS,frequency)) . 5 is Element of HPS

(heptatonic_pythagorean_scale (HPS,frequency)) . 6 is Element of HPS

(heptatonic_pythagorean_scale (HPS,frequency)) . 7 is Element of HPS

Octave (HPS,frequency) is Element of HPS ;

end;
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;

coherence (heptatonic_pythagorean_scale (HPS,frequency)) . 1;

(heptatonic_pythagorean_scale (HPS,frequency)) . 1 is Element of HPS

proof end;

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

(heptatonic_pythagorean_scale (HPS,frequency)) . 2;

coherence (heptatonic_pythagorean_scale (HPS,frequency)) . 2;

(heptatonic_pythagorean_scale (HPS,frequency)) . 2 is Element of HPS

proof end;

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

(heptatonic_pythagorean_scale (HPS,frequency)) . 3;

coherence (heptatonic_pythagorean_scale (HPS,frequency)) . 3;

(heptatonic_pythagorean_scale (HPS,frequency)) . 3 is Element of HPS

proof end;

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

(heptatonic_pythagorean_scale (HPS,frequency)) . 4;

coherence (heptatonic_pythagorean_scale (HPS,frequency)) . 4;

(heptatonic_pythagorean_scale (HPS,frequency)) . 4 is Element of HPS

proof end;

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

(heptatonic_pythagorean_scale (HPS,frequency)) . 5;

coherence (heptatonic_pythagorean_scale (HPS,frequency)) . 5;

(heptatonic_pythagorean_scale (HPS,frequency)) . 5 is Element of HPS

proof end;

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

(heptatonic_pythagorean_scale (HPS,frequency)) . 6;

coherence (heptatonic_pythagorean_scale (HPS,frequency)) . 6;

(heptatonic_pythagorean_scale (HPS,frequency)) . 6 is Element of HPS

proof end;

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

(heptatonic_pythagorean_scale (HPS,frequency)) . 7;

coherence (heptatonic_pythagorean_scale (HPS,frequency)) . 7;

(heptatonic_pythagorean_scale (HPS,frequency)) . 7 is Element of HPS

proof end;

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

Octave (HPS,frequency);

coherence Octave (HPS,frequency);

Octave (HPS,frequency) is Element of HPS ;

:: deftheorem defines hepta_fondamental MUSIC_S1:def 81 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_fondamental (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 1;

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_fondamental (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 1;

:: deftheorem defines hepta_1 MUSIC_S1:def 82 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_1 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 2;

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_1 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 2;

:: deftheorem defines hepta_2 MUSIC_S1:def 83 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_2 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 3;

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_2 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 3;

:: deftheorem defines hepta_3 MUSIC_S1:def 84 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_3 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 4;

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_3 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 4;

:: deftheorem defines hepta_4 MUSIC_S1:def 85 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_4 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 5;

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_4 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 5;

:: deftheorem defines hepta_5 MUSIC_S1:def 86 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_5 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 6;

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_5 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 6;

:: deftheorem defines hepta_6 MUSIC_S1:def 87 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_6 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 7;

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_6 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 7;

:: deftheorem defines hepta_octave MUSIC_S1:def 88 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_octave (HPS,frequency) = Octave (HPS,frequency);

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds hepta_octave (HPS,frequency) = Octave (HPS,frequency);

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 )

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 ;

end;
let n be natural Number ;

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

assume scale is heptatonic ;

:: deftheorem Def27 defines perfect_fifth MUSIC_S1:def 89 :

for MS being MusicSpace

for n being natural Number

for scale being Element of n -tuples_on the carrier of MS st scale is heptatonic holds

( scale is perfect_fifth iff ( [(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 ) );

for MS being MusicSpace

for n being natural Number

for scale being Element of n -tuples_on the carrier of MS st scale is heptatonic holds

( scale is perfect_fifth iff ( [(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 ) );

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

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;

heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency))) is Element of 8 -tuples_on the carrier of HPS ;

end;
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)));

coherence heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)));

heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency))) is Element of 8 -tuples_on the carrier of HPS ;

:: deftheorem defines heptatonic_pythagorean_scale_ascending MUSIC_S1:def 90 :

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds heptatonic_pythagorean_scale_ascending (HPS,frequency) = heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)));

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds heptatonic_pythagorean_scale_ascending (HPS,frequency) = heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)));

theorem Th91: :: MUSIC_S1:113

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds

( (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1 = 2 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2 = (9 / 4) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3 = (81 / 32) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4 = (8 / 3) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 5 = 3 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 6 = (27 / 8) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 7 = (243 / 64) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 8 = 4 * (@ frequency) )

for frequency being Element of HPS holds

( (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1 = 2 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2 = (9 / 4) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3 = (81 / 32) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4 = (8 / 3) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 5 = 3 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 6 = (27 / 8) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 7 = (243 / 64) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 8 = 4 * (@ frequency) )

proof end;

theorem :: MUSIC_S1:114

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1

for frequency being Element of HPS holds (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1

proof end;

theorem Th92: :: MUSIC_S1:115

for HPS being Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds

( intrval ((hepta_4 (HPS,frequency)),(hepta_1 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 )

for frequency being Element of HPS holds

( intrval ((hepta_4 (HPS,frequency)),(hepta_1 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 )

proof end;

theorem Th93: :: MUSIC_S1:116

for HPS being satisfying_euclidean Heptatonic_Pythagorean_Score

for f1, f2 being Element of HPS holds intrval (f1,f2) = the Ratio of HPS . (f1,f2)

for f1, f2 being Element of HPS holds intrval (f1,f2) = the Ratio of HPS . (f1,f2)

proof end;

theorem :: MUSIC_S1:117

for HPS being satisfying_euclidean Heptatonic_Pythagorean_Score

for frequency being Element of HPS holds

( [((heptatonic_pythagorean_scale (HPS,frequency)) . 5),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2)] in fifth HPS & [((heptatonic_pythagorean_scale (HPS,frequency)) . 6),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3)] in fifth HPS & not [((heptatonic_pythagorean_scale (HPS,frequency)) . 7),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4)] in fifth HPS )

for frequency being Element of HPS holds

( [((heptatonic_pythagorean_scale (HPS,frequency)) . 5),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2)] in fifth HPS & [((heptatonic_pythagorean_scale (HPS,frequency)) . 6),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3)] in fifth HPS & not [((heptatonic_pythagorean_scale (HPS,frequency)) . 7),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4)] in fifth HPS )

proof end;

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

let i be Nat;

coherence

( ( i in Seg n implies scale . i is Element of HPS ) & ( not i in Seg n implies the Element of HPS is Element of HPS ) );

consistency

for b_{1} being Element of HPS holds verum;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

let i be Nat;

func # (scale,i) -> Element of HPS equals :Def28: :: MUSIC_S1:def 91

scale . i if i in Seg n

otherwise the Element of HPS;

correctness scale . i if i in Seg n

otherwise the Element of HPS;

coherence

( ( i in Seg n implies scale . i is Element of HPS ) & ( not i in Seg n implies the Element of HPS is Element of HPS ) );

consistency

for b

proof end;

:: deftheorem Def28 defines # MUSIC_S1:def 91 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS

for i being Nat holds

( ( i in Seg n implies # (scale,i) = scale . i ) & ( not i in Seg n implies # (scale,i) = the Element of HPS ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS

for i being Nat holds

( ( i in Seg n implies # (scale,i) = scale . i ) & ( not i in Seg n implies # (scale,i) = the Element of HPS ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is dorian means :: MUSIC_S1:def 92

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines dorian MUSIC_S1:def 92 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is dorian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is dorian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is hypodorian means :: MUSIC_S1:def 93

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines hypodorian MUSIC_S1:def 93 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypodorian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypodorian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is phrygian means :: MUSIC_S1:def 94

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t2 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t2 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines phrygian MUSIC_S1:def 94 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is phrygian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t2 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is phrygian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t2 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is hypophrygian means :: MUSIC_S1:def 95

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t2 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t2 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t2 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t2 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines hypophrygian MUSIC_S1:def 95 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypophrygian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t2 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t2 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypophrygian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t2 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t2 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is lydian means :: MUSIC_S1:def 96

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines lydian MUSIC_S1:def 96 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is lydian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is lydian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is hypolydian means :: MUSIC_S1:def 97

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t2 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t2 );

:: deftheorem defines hypolydian MUSIC_S1:def 97 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypolydian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t2 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypolydian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t2 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is mixolydian means :: MUSIC_S1:def 98

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines mixolydian MUSIC_S1:def 98 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is mixolydian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is mixolydian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is hypomixolydian means :: MUSIC_S1:def 99

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines hypomixolydian MUSIC_S1:def 99 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypomixolydian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypomixolydian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is eolian means :: MUSIC_S1:def 100

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines eolian MUSIC_S1:def 100 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is eolian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is eolian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t2 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is hypoeolian means :: MUSIC_S1:def 101

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t2 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t2 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines hypoeolian MUSIC_S1:def 101 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypoeolian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t2 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypoeolian iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t2 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t1 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t2 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is ionan means :Def29: :: MUSIC_S1:def 102

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t2 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t2 );

:: deftheorem Def29 defines ionan MUSIC_S1:def 102 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is ionan iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t2 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is ionan iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t1 & intrval ((# (scale,7)),(# (scale,8))) = t2 ) );

definition

let HPS be MusicSpace;

let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

end;
let n be natural non zero Number ;

let scale be Element of n -tuples_on the carrier of HPS;

assume scale is heptatonic ;

attr scale is hypoionan means :: MUSIC_S1:def 103

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 );

:: deftheorem defines hypoionan MUSIC_S1:def 103 :

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypoionan iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

for HPS being MusicSpace

for n being natural non zero Number

for scale being Element of n -tuples_on the carrier of HPS st scale is heptatonic holds

( scale is hypoionan iff ex t1, t2 being positive Real st

( (((((t1 * t1) * t1) * t1) * t1) * t2) * t2 = 2 & intrval ((# (scale,1)),(# (scale,2))) = t1 & intrval ((# (scale,2)),(# (scale,3))) = t1 & intrval ((# (scale,3)),(# (scale,4))) = t2 & intrval ((# (scale,4)),(# (scale,5))) = t1 & intrval ((# (scale,5)),(# (scale,6))) = t1 & intrval ((# (scale,6)),(# (scale,7))) = t2 & intrval ((# (scale,7)),(# (scale,8))) = t1 ) );

theorem :: MUSIC_S1:118

for HPS being Heptatonic_Pythagorean_Score

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

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

proof end;