:: {P}ythagorean Tuning: Pentatonic and Heptatonic Scale
:: by Roland Coghetto
::
:: Received September 29, 2018
:: Copyright (c) 2018-2019 Association of Mizar Users

theorem Th1: :: MUSIC_S1:1
for r being object holds
( r in REAL+ \ iff r is positive Real )
proof end;

registration
existence
ex b1 being Rational st b1 is positive
proof end;
end;

definition
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 } is non empty Subset of REAL+
proof end;
end;

:: deftheorem defines RATPLUS MUSIC_S1:def 1 :
RATPLUS = { r where r is positive Rational : verum } ;

theorem Th2: :: MUSIC_S1:2
for r being object holds
( r is Element of RATPLUS iff r is positive Rational )
proof end;

theorem :: MUSIC_S1:3
proof end;

definition
func REALPLUS -> non empty Subset of REAL+ equals :: MUSIC_S1:def 2
REAL+ \ ;
coherence
REAL+ \ is non empty Subset of REAL+
proof end;
end;

:: deftheorem defines REALPLUS MUSIC_S1:def 2 :

theorem Th3: :: MUSIC_S1:4
proof end;

theorem Th4: :: MUSIC_S1:5
proof end;

theorem Th5: :: MUSIC_S1:6
proof end;

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

definition
let S be MusicStruct ;
let a, b, c, d be Element of S;
pred a,b equiv c,d means :: MUSIC_S1:def 3
[[a,b],[c,d]] in the Equidistance of S;
end;

:: deftheorem defines equiv MUSIC_S1:def 3 :
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 ;
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 b1 being Element of REALPLUS ex r, s being positive Real st
( x = r & s = y & b1 = s / r )
proof end;
uniqueness
for b1, b2 being Element of REALPLUS st ex r, s being positive Real st
( x = r & s = y & b1 = s / r ) & ex r, s being positive Real st
( x = r & s = y & b2 = s / r ) holds
b1 = b2
;
end;

:: deftheorem Def01 defines REAL_ratio MUSIC_S1:def 4 :
for x, y, b3 being Element of REALPLUS holds
( b3 = REAL_ratio (x,y) iff ex r, s being positive Real st
( x = r & s = y & b3 = s / r ) );

theorem Th6: :: MUSIC_S1:7
for a, b, c, d being Element of REALPLUS holds
( REAL_ratio (a,b) = REAL_ratio (c,d) iff REAL_ratio (b,a) = REAL_ratio (d,c) )
proof end;

definition
func REAL_ratio -> Function of ,REALPLUS means :Def02: :: MUSIC_S1:def 5
for x being Element of ex y, z being Element of REALPLUS st
( x = [y,z] & it . x = REAL_ratio (y,z) );
existence
ex b1 being Function of ,REALPLUS st
for x being Element of ex y, z being Element of REALPLUS st
( x = [y,z] & b1 . x = REAL_ratio (y,z) )
proof end;
uniqueness
for b1, b2 being Function of ,REALPLUS st ( for x being Element of ex y, z being Element of REALPLUS st
( x = [y,z] & b1 . x = REAL_ratio (y,z) ) ) & ( for x being Element of ex y, z being Element of REALPLUS st
( x = [y,z] & b2 . x = REAL_ratio (y,z) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def02 defines REAL_ratio MUSIC_S1:def 5 :
for b1 being Function of ,REALPLUS holds
( b1 = REAL_ratio iff for x being Element of ex y, z being Element of REALPLUS st
( x = [y,z] & b1 . x = REAL_ratio (y,z) ) );

definition
func EQUIV_REAL_ratio -> Relation of , means :Def03: :: MUSIC_S1:def 6
for x, y being Element of 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
ex b1 being Relation of , st
for x, y being Element of holds
( [x,y] in b1 iff ex a, b, c, d being Element of REALPLUS st
( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) )
proof end;
uniqueness
for b1, b2 being Relation of , st ( for x, y being Element of holds
( [x,y] in b1 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 holds
( [x,y] in b2 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
b1 = b2
proof end;
end;

:: deftheorem Def03 defines EQUIV_REAL_ratio MUSIC_S1:def 6 :
for b1 being Relation of , holds
( b1 = EQUIV_REAL_ratio iff for x, y being Element of holds
( [x,y] in b1 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) ) ) );

definition
coherence ;
end;

:: deftheorem defines REAL_Music MUSIC_S1:def 7 :

theorem Th7: :: MUSIC_S1:8
( not REAL_Music is empty & the carrier of REAL_Music c= REALPLUS & ( for f1, f2, f3, f4 being Element of REAL_Music holds
( f1,f2 equiv f3,f4 iff the Ratio of REAL_Music . (f1,f2) = the Ratio of REAL_Music . (f3,f4) ) ) )
proof end;

theorem Th8: :: MUSIC_S1:9
for f1, f2, f3 being Element of REAL_Music st the Ratio of REAL_Music . (f1,f2) = the Ratio of REAL_Music . (f1,f3) holds
f2 = f3
proof end;

theorem :: MUSIC_S1:10
NATPLUS c= the carrier of REAL_Music by Th4;

theorem Th9: :: MUSIC_S1:11
for frequency being Element of REAL_Music
for n being non zero Nat ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])
proof end;

theorem Th10: :: MUSIC_S1:12
for f1, f2, f3 being Element of REAL_Music st the Ratio of REAL_Music . (f1,f1) = the Ratio of REAL_Music . (f2,f3) holds
f2 = f3
proof end;

theorem Th11: :: MUSIC_S1:13
for f1, f2, fn1, fm1, fn2, fm2 being Element of REAL_Music
for r1, r2 being positive Real
for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2
proof end;

theorem Th12: :: MUSIC_S1:14
for f1, f2, f3, f4 being Element of REAL_Music holds
( the Ratio of REAL_Music . (f1,f2) = the Ratio of REAL_Music . (f3,f4) iff the Ratio of REAL_Music . (f2,f1) = the Ratio of REAL_Music . (f4,f3) )
proof end;

definition
let x, y be Element of RATPLUS ;
func RAT_ratio (x,y) -> Element of RATPLUS means :Def04: :: MUSIC_S1:def 8
ex r, s being positive Rational st
( x = r & s = y & it = s / r );
existence
ex b1 being Element of RATPLUS ex r, s being positive Rational st
( x = r & s = y & b1 = s / r )
proof end;
uniqueness
for b1, b2 being Element of RATPLUS st ex r, s being positive Rational st
( x = r & s = y & b1 = s / r ) & ex r, s being positive Rational st
( x = r & s = y & b2 = s / r ) holds
b1 = b2
;
end;

:: deftheorem Def04 defines RAT_ratio MUSIC_S1:def 8 :
for x, y, b3 being Element of RATPLUS holds
( b3 = RAT_ratio (x,y) iff ex r, s being positive Rational st
( x = r & s = y & b3 = s / r ) );

theorem Th13: :: MUSIC_S1:15
for a, b, c, d being Element of RATPLUS holds
( RAT_ratio (a,b) = RAT_ratio (c,d) iff RAT_ratio (b,a) = RAT_ratio (d,c) )
proof end;

definition
func RAT_ratio -> Function of ,RATPLUS means :Def05: :: MUSIC_S1:def 9
for x being Element of ex y, z being Element of RATPLUS st
( x = [y,z] & it . x = RAT_ratio (y,z) );
existence
ex b1 being Function of ,RATPLUS st
for x being Element of ex y, z being Element of RATPLUS st
( x = [y,z] & b1 . x = RAT_ratio (y,z) )
proof end;
uniqueness
for b1, b2 being Function of ,RATPLUS st ( for x being Element of ex y, z being Element of RATPLUS st
( x = [y,z] & b1 . x = RAT_ratio (y,z) ) ) & ( for x being Element of ex y, z being Element of RATPLUS st
( x = [y,z] & b2 . x = RAT_ratio (y,z) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def05 defines RAT_ratio MUSIC_S1:def 9 :
for b1 being Function of ,RATPLUS holds
( b1 = RAT_ratio iff for x being Element of ex y, z being Element of RATPLUS st
( x = [y,z] & b1 . x = RAT_ratio (y,z) ) );

definition
func EQUIV_RAT_ratio -> Relation of , means :Def06: :: MUSIC_S1:def 10
for x, y being Element of 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
ex b1 being Relation of , st
for x, y being Element of holds
( [x,y] in b1 iff ex a, b, c, d being Element of RATPLUS st
( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) )
proof end;
uniqueness
for b1, b2 being Relation of , st ( for x, y being Element of holds
( [x,y] in b1 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 holds
( [x,y] in b2 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
b1 = b2
proof end;
end;

:: deftheorem Def06 defines EQUIV_RAT_ratio MUSIC_S1:def 10 :
for b1 being Relation of , holds
( b1 = EQUIV_RAT_ratio iff for x, y being Element of holds
( [x,y] in b1 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) ) ) );

definition
coherence ;
end;

:: deftheorem defines RAT_Music MUSIC_S1:def 11 :

theorem Th14: :: MUSIC_S1:16
( not RAT_Music is empty & the carrier of RAT_Music c= REALPLUS & ( for f1, f2, f3, f4 being Element of RAT_Music holds
( f1,f2 equiv f3,f4 iff the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) ) ) )
proof end;

theorem Th15: :: MUSIC_S1:17
for f1, f2, f3 being Element of RAT_Music st the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f1,f3) holds
f2 = f3
proof end;

theorem :: MUSIC_S1:18
NATPLUS c= the carrier of RAT_Music by Th3;

theorem Th16: :: MUSIC_S1:19
for frequency being Element of RAT_Music
for n being non zero Nat ex harmonique being Element of RAT_Music st [frequency,harmonique] in Class ( the Equidistance of RAT_Music,[1,n])
proof end;

theorem Th17: :: MUSIC_S1:20
for f1, f2, f3 being Element of RAT_Music st the Ratio of RAT_Music . (f1,f1) = the Ratio of RAT_Music . (f2,f3) holds
f2 = f3
proof end;

theorem :: MUSIC_S1:21
for frequency being Element of RAT_Music ex r being positive Real st
( frequency = r & ( for n being non zero Nat holds n * r is Element of RAT_Music ) )
proof end;

theorem Th18: :: MUSIC_S1:22
for f1, f2, fn1, fm1, fn2, fm2 being Element of RAT_Music
for r1, r2 being positive Rational
for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2
proof end;

theorem Th19: :: MUSIC_S1:23
for f1, f2, f3, f4 being Element of RAT_Music holds
( the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) iff the Ratio of RAT_Music . (f2,f1) = the Ratio of RAT_Music . (f4,f3) )
proof end;

definition
let S be MusicStruct ;
attr S is satisfying_Real means :Def07a: :: MUSIC_S1:def 12
the carrier of S c= REALPLUS ;
attr S is satisfying_equiv means :Def08a: :: MUSIC_S1:def 13
for f1, f2, f3, f4 being Element of S holds
( f1,f2 equiv f3,f4 iff the Ratio of S . (f1,f2) = the Ratio of S . (f3,f4) );
attr S is satisfying_interval means :Def09a: :: MUSIC_S1:def 14
for f1, f2, f3 being Element of S st the Ratio of S . (f1,f2) = the Ratio of S . (f1,f3) holds
f2 = f3;
attr S is satisfying_tonic means :Def10a: :: MUSIC_S1:def 15
for f1, f2, f3 being Element of S st the Ratio of S . (f1,f1) = the Ratio of S . (f2,f3) holds
f2 = f3;
attr S is satisfying_commutativity means :Def11a: :: MUSIC_S1:def 16
for f1, f2, f3, f4 being Element of S holds
( the Ratio of S . (f1,f2) = the Ratio of S . (f3,f4) iff the Ratio of S . (f2,f1) = the Ratio of S . (f4,f3) );
attr S is satisfying_Nat means :Def12a: :: MUSIC_S1:def 17
NATPLUS c= the carrier of S;
attr S is satisfying_harmonic_closed means :Def13a: :: MUSIC_S1:def 18
for frequency being Element of S
for n being non zero Nat ex harmonique being Element of S st [frequency,harmonique] in Class ( the Equidistance of S,[1,n]);
end;

:: deftheorem Def07a defines satisfying_Real MUSIC_S1:def 12 :
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) ) );

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

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

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

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

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

registration
existence
ex b1 being MusicStruct st
( b1 is satisfying_harmonic_closed & b1 is satisfying_Nat & b1 is satisfying_commutativity & b1 is satisfying_tonic & b1 is satisfying_interval & b1 is satisfying_equiv & b1 is satisfying_Real & not b1 is empty )
proof end;
end;

definition end;

definition end;

theorem Th20: :: MUSIC_S1:24
for S being satisfying_Nat MusicStruct
for n being non zero Nat holds n is Element of S
proof end;

theorem Th21: :: MUSIC_S1:25
for MS being satisfying_equiv MusicStruct
for a, b being Element of MS holds a,b equiv a,b
proof end;

theorem Th22: :: MUSIC_S1:26
for MS being satisfying_equiv MusicStruct
for a, b, c, d being Element of MS holds
( a,b equiv c,d iff c,d equiv a,b )
proof end;

theorem Th23: :: MUSIC_S1:27
for MS being satisfying_equiv MusicStruct
for a, b, c, d, e, f being Element of MS st a,b equiv c,d & c,d equiv e,f holds
a,b equiv e,f
proof end;

theorem Th24: :: MUSIC_S1:28
for S being satisfying_equiv satisfying_interval MusicStruct
for a, b, c being Element of S holds
( a,b equiv a,c iff b = c )
proof end;

theorem :: MUSIC_S1:29
for MS being satisfying_equiv MusicStruct
for a being Element of MS holds a,a equiv a,a
proof end;

theorem Th25: :: MUSIC_S1:30
for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is_reflexive_in [: the carrier of MS, the carrier of MS:]
proof end;

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

theorem Th26: :: MUSIC_S1:32
for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is_symmetric_in [: the carrier of MS, the carrier of MS:]
proof end;

theorem Th27: :: MUSIC_S1:33
for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is_transitive_in [: the carrier of MS, the carrier of MS:]
proof end;

theorem :: MUSIC_S1:34
for MS being satisfying_equiv MusicStruct holds the Equidistance of MS is Equivalence_Relation of [: the carrier of MS, the carrier of MS:]
proof end;

theorem Th28: :: MUSIC_S1:35
for MS being satisfying_equiv satisfying_commutativity MusicStruct
for a, b, c, d being Element of MS holds
( a,b equiv c,d iff b,a equiv d,c )
proof end;

theorem Th29: :: MUSIC_S1:36
for S being satisfying_equiv satisfying_tonic MusicStruct
for a, b, c being Element of S st a,a equiv b,c holds
b = c
proof end;

definition
let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;
let frequency be Element of S;
let n be non zero Nat;
func n -harmonique (S,frequency) -> Element of S means :Def08b: :: MUSIC_S1:def 19
[frequency,it] in Class ( the Equidistance of S,[1,n]);
existence
ex b1 being Element of S st [frequency,b1] in Class ( the Equidistance of S,[1,n])
by Def13a;
uniqueness
for b1, b2 being Element of S st [frequency,b1] in Class ( the Equidistance of S,[1,n]) & [frequency,b2] in Class ( the Equidistance of S,[1,n]) holds
b1 = b2
proof end;
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 b4 being Element of S holds
( b4 = n -harmonique (S,frequency) iff [frequency,b4] in Class ( the Equidistance of S,[1,n]) );

definition
let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;
attr S is satisfying_linearite_harmonique means :Def09: :: MUSIC_S1:def 20
for frequency being Element of S
for n being non zero Nat ex fr being positive Real st
( frequency = fr & n -harmonique (S,frequency) = n * fr );
end;

:: deftheorem Def09 defines satisfying_linearite_harmonique MUSIC_S1:def 20 :
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 ) );

theorem Th30: :: MUSIC_S1:37
proof end;

theorem Th31: :: MUSIC_S1:38
proof end;

registration
existence by Th30;
end;

definition end;

definition end;

definition
let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;
attr MS is satisfying_harmonique_stable means :Def10: :: MUSIC_S1:def 21
for f1, f2 being Element of MS
for n, m being non zero Nat holds n -harmonique (MS,f1),m -harmonique (MS,f1) equiv n -harmonique (MS,f2),m -harmonique (MS,f2);
end;

:: deftheorem Def10 defines satisfying_harmonique_stable MUSIC_S1:def 21 :
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) );

theorem Th32: :: MUSIC_S1:39
proof end;

theorem Th33: :: MUSIC_S1:40
proof end;

registration end;

definition end;

definition end;

definition
let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;
let frequency be Element of MS;
func unison (MS,frequency) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 22
Class ( the Equidistance of MS,[(1 -harmonique (MS,frequency)),(1 -harmonique (MS,frequency))]);
coherence
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))]) 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))]) 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))]) 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))]) 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))]) 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))]) 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))]) 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))]) 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))]) is Subset of [: the carrier of MS, the carrier of MS:]
;
end;

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

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

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

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

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

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

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

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

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

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

definition
let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;
func unison MS -> Subset of [: the carrier of MS, the carrier of MS:] equals :: MUSIC_S1:def 32
Class ( the Equidistance of MS,[1,1]);
coherence
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]) 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]) 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]) 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]) 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]) 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]) 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]) 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]) 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]) is Subset of [: the carrier of MS, the carrier of MS:]
;
end;

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

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

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

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

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

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

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

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

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

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

definition
let S be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct ;
attr S is satisfying_fifth_constructible means :Def11: :: MUSIC_S1:def 42
for frequency being Element of S ex q being Element of S st [frequency,q] in fifth S;
end;

:: deftheorem Def11 defines satisfying_fifth_constructible MUSIC_S1:def 42 :
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 )
proof end;

theorem Th35: :: MUSIC_S1:42
proof end;

theorem Th36: :: MUSIC_S1:43
for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = (3 / 2) * fr & [fr,qr] in fifth RAT_Music )
proof end;

theorem Th37: :: MUSIC_S1:44
proof end;

registration end;

definition end;

definition end;

definition
let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct ;
let frequency be Element of MS;
func Fifth (MS,frequency) -> Element of MS means :Def11bis: :: MUSIC_S1:def 43
[frequency,it] in fifth MS;
existence
ex b1 being Element of MS st [frequency,b1] in fifth MS
by Def11;
uniqueness
for b1, b2 being Element of MS st [frequency,b1] in fifth MS & [frequency,b2] in fifth MS holds
b1 = b2
proof end;
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, b3 being Element of MS holds
( b3 = Fifth (MS,frequency) iff [frequency,b3] in fifth MS );

theorem :: MUSIC_S1:45
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible MusicStruct
for frequency being Element of MS holds fifth (MS,frequency) = fifth MS
proof end;

theorem Th38: :: MUSIC_S1:46
for frequency being Element of REAL_Music ex fr being positive Real st
( frequency = fr & Fifth (REAL_Music,frequency) = (3 / 2) * fr )
proof end;

theorem Th39: :: MUSIC_S1:47
for frequency being Element of RAT_Music ex fr being positive Rational st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr )
proof end;

definition
let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct ;
attr MS is classical_fifth means :Def12: :: MUSIC_S1:def 44
for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fifth (MS,frequency) = (3 / 2) * fr );
end;

:: deftheorem Def12 defines classical_fifth MUSIC_S1:def 44 :
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 end;

definition end;

definition end;

theorem Th40: :: MUSIC_S1:48
for MS being satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed MusicStruct
for frequency being Element of MS holds 1 -harmonique (MS,frequency) = frequency
proof end;

theorem :: MUSIC_S1:49
for MS being satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_harmonique_stable MusicStruct
for a, b being Element of MS holds a,a equiv b,b
proof end;

theorem :: MUSIC_S1:50
for MS being satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct
for frequency being Element of MS holds octave (MS,frequency) = octave MS
proof end;

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

definition
let MS be MusicStruct ;
let a, b, c be Element of MS;
pred b is_Between a,c means :: MUSIC_S1:def 45
ex r1, r2, r3 being positive Real st
( a = r1 & b = r2 & c = r3 & r1 <= r2 & r2 < r3 );
end;

:: deftheorem defines is_Between MUSIC_S1:def 45 :
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 ;
attr S is satisfying_octave_constructible means :Def13: :: MUSIC_S1:def 46
for frequency being Element of S ex o being Element of S st [frequency,o] in octave S;
end;

:: deftheorem Def13 defines satisfying_octave_constructible MUSIC_S1:def 46 :
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 )
proof end;

theorem Th42: :: MUSIC_S1:53
proof end;

theorem Th43: :: MUSIC_S1:54
for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = 2 * fr & [fr,qr] in octave RAT_Music )
proof end;

theorem Th44: :: MUSIC_S1:55
proof end;

registration end;

definition end;

definition
let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct ;
let frequency be Element of MS;
func Octave (MS,frequency) -> Element of MS means :Def14: :: MUSIC_S1:def 47
[frequency,it] in octave MS;
existence
ex b1 being Element of MS st [frequency,b1] in octave MS
by Def13;
uniqueness
for b1, b2 being Element of MS st [frequency,b1] in octave MS & [frequency,b2] in octave MS holds
b1 = b2
proof end;
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, b3 being Element of MS holds
( b3 = Octave (MS,frequency) iff [frequency,b3] in octave MS );

definition
let MS be non empty satisfying_Real MusicStruct ;
let r be Element of MS;
func @ r -> positive Real equals :: MUSIC_S1:def 48
r;
coherence
r is positive Real
proof end;
end;

:: deftheorem defines @ MUSIC_S1:def 48 :
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 ;
attr MS is classical_octave means :Def15: :: MUSIC_S1:def 49
for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Octave (MS,frequency) = 2 * fr );
end;

:: deftheorem Def15 defines classical_octave MUSIC_S1:def 49 :
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 ) );

theorem Th45: :: MUSIC_S1:56
proof end;

theorem Th46: :: MUSIC_S1:57
proof end;

registration end;

definition
let MS be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct ;
attr MS is satisfying_octave_descendent_constructible means :Def16: :: MUSIC_S1:def 50
for frequency being Element of MS ex o being Element of MS st [o,frequency] in octave MS;
end;

:: deftheorem Def16 defines satisfying_octave_descendent_constructible MUSIC_S1:def 50 :
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 )
proof end;

theorem Th48: :: MUSIC_S1:59
proof end;

theorem Th49: :: MUSIC_S1:60
for frequency being Element of RAT_Music ex fr, qr being positive Rational st
( fr = frequency & qr = (1 / 2) * fr & [qr,fr] in octave RAT_Music )
proof end;

theorem Th50: :: MUSIC_S1:61
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 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
ex b1 being Element of MS st [b1,frequency] in octave MS
by Def16;
uniqueness
for b1, b2 being Element of MS st [b1,frequency] in octave MS & [b2,frequency] in octave MS holds
b1 = b2
proof end;
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, b3 being Element of MS holds
( b3 = Octave_descendent (MS,frequency) iff [b3,frequency] in octave MS );

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

theorem Th52: :: MUSIC_S1:63
for MS1, MS2 being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave MusicStruct
for f1 being Element of MS1
for f2 being Element of MS2 st f1 = f2 holds
( Fifth (MS1,f1) = Fifth (MS2,f2) & Octave (MS1,f1) = Octave (MS2,f2) )
proof end;

theorem Th53: :: MUSIC_S1:64
for MS1, MS2 being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency1 being Element of MS1
for frequency2 being Element of MS2 st frequency1 = frequency2 holds
Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2)
proof end;

definition
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;
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
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 b1 being Element of MS holds verum
;
;
end;

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

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

theorem Th54: :: MUSIC_S1:66
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth MusicStruct
for frequency being Element of MS ex r, s being positive Real st
( r = frequency & s = (3 / 2) * r & Fifth (MS,frequency) = s )
proof end;

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

theorem Th56: :: MUSIC_S1:68
for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale, frequency being Element of MS st frequency is_Between fondamentale, Octave (MS,fondamentale) holds
Fifth_reduct (MS,fondamentale,frequency) is_Between fondamentale, Octave (MS,fondamentale)
proof end;

theorem :: MUSIC_S1:69

theorem :: MUSIC_S1:70

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

definition
let MS be non empty satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct ;
let fondamentale, frequency be Element of MS;
func spiral_of_fifths (MS,fondamentale,frequency) -> sequence of MS means :Def19: :: MUSIC_S1:def 53
( it . 0 = frequency & ( for n being Nat holds it . (n + 1) = Fifth_reduct (MS,fondamentale,(it . n)) ) );
existence
ex b1 being sequence of MS st
( b1 . 0 = frequency & ( for n being Nat holds b1 . (n + 1) = Fifth_reduct (MS,fondamentale,(b1 . n)) ) )
by Th56BIS;
uniqueness
for b1, b2 being sequence of MS st b1 . 0 = frequency & ( for n being Nat holds b1 . (n + 1) = Fifth_reduct (MS,fondamentale,(b1 . n)) ) & b2 . 0 = frequency & ( for n being Nat holds b2 . (n + 1) = Fifth_reduct (MS,fondamentale,(b2 . n)) ) holds
b1 = b2
proof end;
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 b4 being sequence of MS holds
( b4 = spiral_of_fifths (MS,fondamentale,frequency) iff ( b4 . 0 = frequency & ( for n being Nat holds b4 . (n + 1) = Fifth_reduct (MS,fondamentale,(b4 . n)) ) ) );

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

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

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

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

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

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

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

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

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

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

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

definition
let MS be MusicSpace;
let scale be Element of 2 -tuples_on the carrier of MS;
attr scale is monotonic means :: MUSIC_S1:def 54
ex frequency being Element of MS ex r1, r2 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & r1 < r2 & scale . 2 = Octave (MS,frequency) );
end;

:: deftheorem defines monotonic MUSIC_S1:def 54 :
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) ) );

definition
let MS be MusicSpace;
let scale be Element of 3 -tuples_on the carrier of MS;
attr scale is ditonic means :: MUSIC_S1:def 55
ex frequency being Element of MS ex r1, r2, r3 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & r1 < r2 & r2 < r3 & scale . 3 = Octave (MS,frequency) );
end;

:: deftheorem defines ditonic MUSIC_S1:def 55 :
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) ) );

definition
let MS be MusicSpace;
let scale be Element of 4 -tuples_on the carrier of MS;
attr scale is tritonic means :: MUSIC_S1:def 56
ex frequency being Element of MS ex r1, r2, r3, r4 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & r1 < r2 & r2 < r3 & r3 < r4 & scale . 4 = Octave (MS,frequency) );
end;

:: deftheorem defines tritonic MUSIC_S1:def 56 :
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;
attr scale is tetratonic means :: MUSIC_S1:def 57
ex frequency being Element of MS ex r1, r2, r3, r4, r5 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & scale . 5 = Octave (MS,frequency) );
end;

:: deftheorem defines tetratonic MUSIC_S1:def 57 :
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;
attr scale is pentatonic means :: MUSIC_S1:def 58
( n = 6 & ex frequency being Element of MS ex r1, r2, r3, r4, r5, r6 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & scale . 6 = r6 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & scale . 6 = Octave (MS,frequency) ) );
end;

:: deftheorem defines pentatonic MUSIC_S1:def 58 :
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;
attr scale is hexatonic means :: MUSIC_S1:def 59
ex frequency being Element of MS ex r1, r2, r3, r4, r5, r6, r7 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & scale . 4 = r4 & scale . 5 = r5 & scale . 6 = r6 & scale . 7 = r7 & r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 & r6 < r7 & scale . 7 = Octave (MS,frequency) );
end;

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

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

:: deftheorem defines octatonic MUSIC_S1:def 61 :
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;
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
ex b1 being Element of 6 -tuples_on the carrier of MS st
( b1 . 1 = frequency & b1 . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b1 . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b1 . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b1 . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b1 . 6 = Octave (MS,frequency) )
proof end;
uniqueness
for b1, b2 being Element of 6 -tuples_on the carrier of MS st b1 . 1 = frequency & b1 . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b1 . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b1 . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b1 . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b1 . 6 = Octave (MS,frequency) & b2 . 1 = frequency & b2 . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b2 . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b2 . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b2 . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b2 . 6 = Octave (MS,frequency) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines pentatonic_pythagorean_scale MUSIC_S1:def 62 :
for MS being MusicSpace
for frequency being Element of MS
for b3 being Element of 6 -tuples_on the carrier of MS holds
( b3 = pentatonic_pythagorean_scale (MS,frequency) iff ( b3 . 1 = frequency & b3 . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b3 . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b3 . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b3 . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b3 . 6 = Octave (MS,frequency) ) );

theorem Th67: :: MUSIC_S1:83
for MS being MusicSpace
for frequency being Element of MS holds pentatonic_pythagorean_scale (MS,frequency) is pentatonic
proof end;

definition
let MS be MusicSpace;
let f1, f2 be Element of MS;
func intrval (f1,f2) -> positive Real means :Def21: :: MUSIC_S1:def 63
ex r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & it = r2 / r1 );
existence
ex b1, r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & b1 = r2 / r1 )
proof end;
uniqueness
for b1, b2 being positive Real st ex r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & b1 = r2 / r1 ) & ex r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & b2 = r2 / r1 ) holds
b1 = b2
;
end;

:: deftheorem Def21 defines intrval MUSIC_S1:def 63 :
for MS being MusicSpace
for f1, f2 being Element of MS
for b4 being positive Real holds
( b4 = intrval (f1,f2) iff ex r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & b4 = r2 / r1 ) );

definition
coherence
9 / 8 is positive Real
;
end;

:: deftheorem defines pythagorean_tone MUSIC_S1:def 64 :

definition
coherence
32 / 27 is positive Real
;
end;

:: deftheorem defines pentatonic_pythagorean_semiditone MUSIC_S1:def 65 :

definition end;

definition
coherence
5 / 4 is positive Real
;
end;

:: deftheorem defines pure_major_third MUSIC_S1:def 67 :

definition end;

:: deftheorem defines syntonic_comma MUSIC_S1:def 68 :

theorem :: MUSIC_S1:84
syntonic_comma = 81 / 80 ;

definition
let MS be MusicSpace;
let frequency be Element of MS;
func penta_fondamentale (MS,frequency) -> Element of MS equals :: MUSIC_S1:def 69
(pentatonic_pythagorean_scale (MS,frequency)) . 1;
coherence
(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 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 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 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 is Element of MS
proof end;
func penta_octave (MS,frequency) -> Element of MS equals :: MUSIC_S1:def 74
Octave (MS,frequency);
coherence
Octave (MS,frequency) is Element of MS
;
end;

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

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

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

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

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

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

theorem :: MUSIC_S1:87
for MS being MusicSpace
for f1, f2 being Element of MS ex r1, r2 being Element of REALPLUS st intrval (f1,f2) = REAL_ratio (r1,r2)
proof end;

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

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

theorem :: MUSIC_S1:90
9 / 8 = 9 / 8 ;

theorem :: MUSIC_S1:91
for MS being MusicSpace
for frequency being Element of MS holds
( intrval ((penta_fondamentale (MS,frequency)),(penta_1 (MS,frequency))) = pythagorean_tone & intrval ((penta_1 (MS,frequency)),(penta_2 (MS,frequency))) = pythagorean_tone & intrval ((penta_2 (MS,frequency)),(penta_3 (MS,frequency))) = pentatonic_pythagorean_semiditone & intrval ((penta_3 (MS,frequency)),(penta_4 (MS,frequency))) = pythagorean_tone & intrval ((penta_4 (MS,frequency)),(penta_octave (MS,frequency))) = pentatonic_pythagorean_semiditone )
proof end;

theorem :: MUSIC_S1:92
for MS being MusicSpace
for frequency being Element of MS holds Fifth (MS,frequency) is_Between frequency, Octave (MS,frequency)
proof end;

theorem Th70: :: MUSIC_S1:93
for MS being MusicSpace
for f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( Fifth (MS,f2) = 2 * r1 & not Fifth (MS,f2) is_Between f1, Octave (MS,f1) )
proof end;

theorem Th71: :: MUSIC_S1:94
for MS being MusicSpace
for fondamentale, f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
( ( Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Octave_descendent (MS,(Fifth_reduct (MS,fondamentale,f2))) = f1 ) & ( not Fifth (MS,f2) is_Between fondamentale, Octave (MS,fondamentale) implies Fifth_reduct (MS,fondamentale,f2) = f1 ) )
proof end;

theorem :: MUSIC_S1:95
for MS being MusicSpace
for f1, f2 being Element of MS
for r1, r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 / 3) * r1 holds
Fifth_reduct (MS,f1,f2) = f1
proof end;

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

:: deftheorem Def22 defines satisfying_fourth_constructible MUSIC_S1:def 75 :
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 )
proof end;

theorem Th79: :: MUSIC_S1:97
proof end;

registration end;

definition
let MS be satisfying_fourth_constructible MusicSpace;
let frequency be Element of MS;
func Fourth (MS,frequency) -> Element of MS means :Def23: :: MUSIC_S1:def 76
[frequency,it] in fourth MS;
existence
ex b1 being Element of MS st [frequency,b1] in fourth MS
by Def22;
uniqueness
for b1, b2 being Element of MS st [frequency,b1] in fourth MS & [frequency,b2] in fourth MS holds
b1 = b2
proof end;
end;

:: deftheorem Def23 defines Fourth MUSIC_S1:def 76 :
for MS being satisfying_fourth_constructible MusicSpace
for frequency, b3 being Element of MS holds
( b3 = Fourth (MS,frequency) iff [frequency,b3] in fourth MS );

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

:: deftheorem Def24 defines classical_fourth MUSIC_S1:def 77 :
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 )
proof end;

registration end;

definition
let MS be non empty satisfying_Real MusicStruct ;
attr MS is satisfying_euclidean means :Def25: :: MUSIC_S1:def 78
for f1, f2 being Element of MS holds the Ratio of MS . (f1,f2) = (@ f2) / (@ f1);
end;

:: deftheorem Def25 defines satisfying_euclidean MUSIC_S1:def 78 :
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 b1 being non empty satisfying_Real MusicStruct st b1 is satisfying_euclidean
proof end;
end;

registration
coherence
for b1 being non empty satisfying_Real MusicStruct st b1 is satisfying_euclidean holds
b1 is satisfying_interval
proof end;
end;

registration
coherence
for b1 being non empty satisfying_Real MusicStruct st b1 is satisfying_euclidean holds
b1 is satisfying_tonic
proof end;
end;

registration
coherence
for b1 being non empty satisfying_Real MusicStruct st b1 is satisfying_euclidean holds
b1 is satisfying_commutativity
proof end;
end;

registration end;

definition
let HPS be Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;
func heptatonic_pythagorean_scale (HPS,frequency) -> Element of 8 -tuples_on the carrier of HPS means :Def26: :: MUSIC_S1:def 79
( it . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & it . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & it . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & it . 4 = Fourth (HPS,frequency) & it . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & it . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & it . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & it . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) );
existence
ex b1 being Element of 8 -tuples_on the carrier of HPS st
( b1 . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & b1 . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & b1 . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & b1 . 4 = Fourth (HPS,frequency) & b1 . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & b1 . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & b1 . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & b1 . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) )
proof end;
uniqueness
for b1, b2 being Element of 8 -tuples_on the carrier of HPS st b1 . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & b1 . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & b1 . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & b1 . 4 = Fourth (HPS,frequency) & b1 . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & b1 . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & b1 . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & b1 . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) & b2 . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & b2 . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & b2 . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & b2 . 4 = Fourth (HPS,frequency) & b2 . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & b2 . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & b2 . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & b2 . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) holds
b1 = b2
proof end;
end;

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

theorem Th81: :: MUSIC_S1:99
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds Fourth (HPS,frequency) is_Between frequency, Octave (HPS,frequency)
proof end;

theorem :: MUSIC_S1:100
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS
for n being Nat holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . n is_Between frequency, Octave (HPS,frequency) by ;

theorem Th82: :: MUSIC_S1:101
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 = frequency
proof end;

theorem Th83: :: MUSIC_S1:102
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 = (3 / 2) * (@ frequency)
proof end;

theorem Th84: :: MUSIC_S1:103
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 = (9 / 8) * (@ frequency)
proof end;

theorem Th85: :: MUSIC_S1:104
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 = (27 / 16) * (@ frequency)
proof end;

theorem Th86: :: MUSIC_S1:105
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 = (81 / 64) * (@ frequency)
proof end;

theorem Th87: :: MUSIC_S1:106
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 = (243 / 128) * (@ frequency)
proof end;

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

theorem Th88BIS: :: MUSIC_S1:108
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is heptatonic
proof end;

definition
coherence
256 / 243 is positive Real
;
end;

:: deftheorem defines heptatonic_pythagorean_semitone MUSIC_S1:def 80 :

notation end;

notation end;

theorem :: MUSIC_S1:109

definition
let HPS be Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;
func hepta_fondamental (HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 81
(heptatonic_pythagorean_scale (HPS,frequency)) . 1;
coherence
(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 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 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 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 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 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 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) is Element of HPS
;
end;

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

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

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

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

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

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

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

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

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

proof end;

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

proof end;

theorem Th90: :: MUSIC_S1:111
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
( intrval ((hepta_fondamental (HPS,frequency)),(hepta_1 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_1 (HPS,frequency)),(hepta_2 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_2 (HPS,frequency)),(hepta_3 (HPS,frequency))) = heptatonic_pythagorean_semitone & intrval ((hepta_3 (HPS,frequency)),(hepta_4 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_4 (HPS,frequency)),(hepta_5 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_5 (HPS,frequency)),(hepta_6 (HPS,frequency))) = pythagorean_tone & intrval ((hepta_6 (HPS,frequency)),(hepta_octave (HPS,frequency))) = heptatonic_pythagorean_semitone )
proof end;

definition
let MS be MusicSpace;
let n be natural Number ;
let scale be Element of n -tuples_on the carrier of MS;
assume scale is heptatonic ;
attr scale is perfect_fifth means :Def27: :: MUSIC_S1:def 89
( [(scale . 1),(scale . 5)] in fifth MS & [(scale . 2),(scale . 6)] in fifth MS & [(scale . 3),(scale . 7)] in fifth MS & [(scale . 4),(scale . 8)] in fifth MS );
end;

:: deftheorem Def27 defines perfect_fifth MUSIC_S1:def 89 :
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
proof end;

definition
let HPS be Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;
func heptatonic_pythagorean_scale_ascending (HPS,frequency) -> Element of 8 -tuples_on the carrier of HPS equals :: MUSIC_S1:def 90
heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)));
coherence
heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency))) is Element of 8 -tuples_on the carrier of HPS
;
end;

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

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) )
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
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 )
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)
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 )
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;
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
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 b1 being Element of HPS holds verum
;
proof end;
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 ) );

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: MUSIC_S1:118
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is ionan
proof end;