:: {P}ythagorean Tuning: Pentatonic and Heptatonic Scale :: by Roland Coghetto :: :: Received September 29, 2018 :: Copyright (c) 2018-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, STRUCT_0, FUNCT_1, ZFMISC_1, XXREAL_0, TARSKI, EQREL_1, RELAT_2, PARTFUN1, ORDINAL1, RAT_1, FINSEQ_1, QC_LANG1, NAT_LAT, MUSIC_S1, MSAFREE2, GTARSKI1, FINSEQ_2, XCMPLX_0, ARYTM_2, PBOOLE, FUNCT_2; notations RAT_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, PARTFUN1, DOMAIN_1, XREAL_0, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, NAT_1, STRUCT_0, EQREL_1, RELAT_2, ARYTM_3, ORDINAL1, ARYTM_2, FINSEQ_1, FINSEQ_2, NAT_LAT; constructors ARYTM_1, TOPREALA, NAT_LAT; registrations ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, STRUCT_0, CARD_1, SUBSET_1, XCMPLX_0, FUNCT_2, FINSEQ_2, XXREAL_0, ARYTM_2, RAT_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries theorem :: MUSIC_S1:1 for r being object holds r in REAL+ \ {0} iff r is positive Real; registration cluster positive for Rational; end; definition func RATPLUS -> non empty Subset of REAL+ equals :: MUSIC_S1:def 1 the set of all r where r is positive Rational; end; theorem :: MUSIC_S1:2 for r being object holds r is Element of RATPLUS iff r is positive Rational; theorem :: MUSIC_S1:3 RAT+ c= RAT; definition func REALPLUS -> non empty Subset of REAL+ equals :: MUSIC_S1:def 2 REAL+ \ {0}; end; theorem :: MUSIC_S1:4 NATPLUS c= RATPLUS; theorem :: MUSIC_S1:5 NATPLUS c= REALPLUS; theorem :: MUSIC_S1:6 RATPLUS c= REALPLUS; begin :: Real frequency definition struct (1-sorted) MusicStruct (# carrier->set, Equidistance -> Relation of [:the carrier,the carrier :],[:the carrier,the carrier:], Ratio -> Function of [:the carrier,the carrier:],the carrier #); 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; definition let x,y be Element of REALPLUS; func REAL_ratio(x,y) -> Element of REALPLUS means :: MUSIC_S1:def 4 ex r,s be positive Real st x = r & s = y & it = s / r; end; theorem :: 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); definition func REAL_ratio -> Function of [:REALPLUS,REALPLUS:],REALPLUS means :: MUSIC_S1:def 5 for x being Element of [:REALPLUS,REALPLUS:] holds ex y,z being Element of REALPLUS st x = [y,z] & it.x = REAL_ratio(y,z); end; definition func EQUIV_REAL_ratio -> Relation of [:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:] means :: MUSIC_S1:def 6 for x,y being Element of [:REALPLUS,REALPLUS:] holds [x,y] in it iff ex a,b,c,d being Element of REALPLUS st x = [a,b] & y = [c,d] & REAL_ratio(a,b) = REAL_ratio(c,d); end; definition func REAL_Music -> MusicStruct equals :: MUSIC_S1:def 7 MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #); end; theorem :: MUSIC_S1:8 REAL_Music is non 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))); theorem :: 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; theorem :: MUSIC_S1:10 NATPLUS c= the carrier of REAL_Music; theorem :: MUSIC_S1:11 for frequency being Element of REAL_Music for n being non zero Nat ex harmonique be Element of REAL_Music st [frequency,harmonique] in Class(the Equidistance of REAL_Music,[1,n]); theorem :: 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; theorem :: MUSIC_S1:13 for f1,f2,fn1,fm1,fn2,fm2 being Element of REAL_Music for r1,r2 being positive Real :::st f1 = r1 & f2 = r2 holds 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; theorem :: MUSIC_S1:14 for f1,f2,f3,f4 be 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); begin :: Definition of RATPLUS definition let x,y be Element of RATPLUS; func RAT_ratio(x,y) -> Element of RATPLUS means :: MUSIC_S1:def 8 ex r,s be positive Rational st x = r & s = y & it = s / r; end; theorem :: 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); definition func RAT_ratio -> Function of [:RATPLUS,RATPLUS:],RATPLUS means :: MUSIC_S1:def 9 for x being Element of [:RATPLUS,RATPLUS:] holds ex y,z being Element of RATPLUS st x = [y,z] & it.x = RAT_ratio(y,z); end; definition func EQUIV_RAT_ratio -> Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] means :: MUSIC_S1:def 10 for x,y being Element of [:RATPLUS,RATPLUS:] holds [x,y] in it iff ex a,b,c,d being Element of RATPLUS st x = [a,b] & y = [c,d] & RAT_ratio(a,b) = RAT_ratio(c,d); end; definition func RAT_Music -> MusicStruct equals :: MUSIC_S1:def 11 MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #); end; theorem :: MUSIC_S1:16 RAT_Music is non 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))); theorem :: 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; theorem :: MUSIC_S1:18 NATPLUS c= the carrier of RAT_Music; theorem :: MUSIC_S1:19 for frequency being Element of RAT_Music for n being non zero Nat ex harmonique be Element of RAT_Music st [frequency,harmonique] in Class(the Equidistance of RAT_Music,[1,n]); theorem :: 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; 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); theorem :: MUSIC_S1:22 for f1,f2,fn1,fm1,fn2,fm2 being Element of RAT_Music for r1,r2 being positive Rational :::st f1 = r1 & f2 = r2 holds 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; theorem :: MUSIC_S1:23 for f1,f2,f3,f4 be 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); begin :: Musical structure and somes axioms definition let S be MusicStruct; attr S is satisfying_Real means :: MUSIC_S1:def 12 the carrier of S c= REALPLUS; attr S is satisfying_equiv means :: 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 :: 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 :: 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 :: 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 :: MUSIC_S1:def 17 NATPLUS c= the carrier of S; attr S is satisfying_harmonic_closed means :: MUSIC_S1:def 18 for frequency being Element of S for n being non zero Nat ex harmonique be Element of S st [frequency,harmonique] in Class(the Equidistance of S,[1,n]); end; registration cluster satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty for MusicStruct; end; definition redefine func REAL_Music -> satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func RAT_Music -> satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; theorem :: MUSIC_S1:24 for S being satisfying_Nat MusicStruct for n being non zero Nat holds n is Element of S; theorem :: MUSIC_S1:25 for MS being satisfying_equiv MusicStruct for a,b being Element of MS holds a,b equiv a,b; theorem :: 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; theorem :: MUSIC_S1:27 for MS being satisfying_equiv MusicStruct for a,b,c,d,e,f being Element of MS holds a,b equiv c,d & c,d equiv e,f implies a,b equiv e,f; theorem :: MUSIC_S1:28 for S being satisfying_interval satisfying_equiv MusicStruct for a,b,c being Element of S holds (a,b equiv a,c iff b = c); reserve MS for satisfying_equiv MusicStruct; reserve a,b,c,d,e,f for Element of MS; theorem :: MUSIC_S1:29 a,a equiv a,a; theorem :: MUSIC_S1:30 the Equidistance of MS is_reflexive_in [:the carrier of MS,the carrier of MS:]; theorem :: MUSIC_S1:31 MS is non empty implies the Equidistance of MS is reflexive & field the Equidistance of MS = [:the carrier of MS,the carrier of MS:]; theorem :: MUSIC_S1:32 the Equidistance of MS is_symmetric_in [:the carrier of MS,the carrier of MS:]; theorem :: MUSIC_S1:33 the Equidistance of MS is_transitive_in [:the carrier of MS,the carrier of MS:]; theorem :: MUSIC_S1:34 the Equidistance of MS is Equivalence_Relation of [:the carrier of MS,the carrier of MS:]; theorem :: MUSIC_S1:35 for MS being satisfying_commutativity satisfying_equiv MusicStruct for a,b,c,d being Element of MS holds a,b equiv c,d iff b,a equiv d,c; theorem :: MUSIC_S1:36 for S being satisfying_tonic satisfying_equiv MusicStruct for a,b,c being Element of S st a,a equiv b,c holds b = c; definition let S be satisfying_Nat satisfying_interval satisfying_harmonic_closed satisfying_equiv MusicStruct; let frequency be Element of S; let n be non zero Nat; func n-harmonique(S,frequency) -> Element of S means :: MUSIC_S1:def 19 [frequency,it] in Class(the Equidistance of S,[1,n]); end; definition let S be satisfying_Nat satisfying_interval satisfying_harmonic_closed satisfying_equiv MusicStruct; attr S is satisfying_linearite_harmonique means :: MUSIC_S1:def 20 for frequency being Element of S for n being non zero Nat holds ex fr being positive Real st frequency = fr & n-harmonique(S,frequency) = n * fr; end; theorem :: MUSIC_S1:37 REAL_Music is satisfying_linearite_harmonique; theorem :: MUSIC_S1:38 RAT_Music is satisfying_linearite_harmonique; registration cluster satisfying_linearite_harmonique for satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func REAL_Music -> satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func RAT_Music -> satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition let MS be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; attr MS is satisfying_harmonique_stable means :: 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; theorem :: MUSIC_S1:39 REAL_Music is satisfying_harmonique_stable; theorem :: MUSIC_S1:40 RAT_Music is satisfying_harmonique_stable; registration cluster satisfying_harmonique_stable for satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func REAL_Music -> satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func RAT_Music -> satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition let MS be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; let frequency be Element of MS; func unison(MS,frequency) -> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 22 Class(the Equidistance of MS, [1-harmonique(MS,frequency),1-harmonique(MS,frequency)]); func octave(MS,frequency) -> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 23 Class(the Equidistance of MS, [1-harmonique(MS,frequency),2-harmonique(MS,frequency)]); func fifth(MS,frequency) -> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 24 Class(the Equidistance of MS, [2-harmonique(MS,frequency),3-harmonique(MS,frequency)]); func fourth(MS,frequency)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 25 Class(the Equidistance of MS, [3-harmonique(MS,frequency),4-harmonique(MS,frequency)]); func major_sixth(MS,frequency)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 26 Class(the Equidistance of MS, [3-harmonique(MS,frequency),5-harmonique(MS,frequency)]); func major_third(MS,frequency)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 27 Class(the Equidistance of MS, [4-harmonique(MS,frequency),5-harmonique(MS,frequency)]); func minor_third(MS,frequency)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 28 Class(the Equidistance of MS, [5-harmonique(MS,frequency),6-harmonique(MS,frequency)]); func minor_sixth(MS,frequency)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 29 Class(the Equidistance of MS, [5-harmonique(MS,frequency),8-harmonique(MS,frequency)]); func major_tone(MS,frequency)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 30 Class(the Equidistance of MS, [8-harmonique(MS,frequency),9-harmonique(MS,frequency)]); func minor_tone(MS,frequency)-> Subset of [:the carrier of MS,the carrier of MS:]equals :: MUSIC_S1:def 31 Class(the Equidistance of MS, [9-harmonique(MS,frequency),10-harmonique(MS,frequency)]); end; definition let MS be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; func unison(MS) -> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 32 Class(the Equidistance of MS,[1,1]); func octave(MS) -> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 33 Class(the Equidistance of MS,[1,2]); func fifth(MS) -> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 34 Class(the Equidistance of MS,[2,3]); func fourth(MS)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 35 Class(the Equidistance of MS,[3,4]); func major_sixth(MS)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 36 Class(the Equidistance of MS,[3,5]); func major_third(MS)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 37 Class(the Equidistance of MS,[4,5]); func minor_third(MS)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 38 Class(the Equidistance of MS,[5,6]); func minor_sixth(MS)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 39 Class(the Equidistance of MS,[5,8]); func major_tone(MS)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 40 Class(the Equidistance of MS,[8,9]); func minor_tone(MS)-> Subset of [:the carrier of MS,the carrier of MS:] equals :: MUSIC_S1:def 41 Class(the Equidistance of MS,[9,10]); end; definition let S be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; attr S is satisfying_fifth_constructible means :: MUSIC_S1:def 42 for frequency being Element of S holds ex q being Element of S st [frequency,q] in fifth(S); end; theorem :: MUSIC_S1:41 for frequency be Element of REAL_Music holds ex fr,qr being positive Real st fr = frequency & qr = (3 qua Real) / 2 * fr & [fr,qr] in fifth(REAL_Music); theorem :: MUSIC_S1:42 REAL_Music is satisfying_fifth_constructible; theorem :: MUSIC_S1:43 for frequency be Element of RAT_Music holds ex fr,qr being positive Rational st fr = frequency & qr = (3 qua Rational) / 2 * fr & [fr,qr] in fifth(RAT_Music); theorem :: MUSIC_S1:44 RAT_Music is satisfying_fifth_constructible; registration cluster satisfying_fifth_constructible for satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func REAL_Music -> satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func RAT_Music -> satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition let MS be satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; let frequency be Element of MS; func Fifth(MS,frequency) -> Element of MS means :: MUSIC_S1:def 43 [frequency,it] in fifth(MS); end; theorem :: MUSIC_S1:45 for MS being satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct for frequency being Element of MS holds fifth(MS,frequency) = fifth(MS); theorem :: MUSIC_S1:46 for frequency being Element of REAL_Music ex fr being positive Real st frequency = fr & Fifth(REAL_Music,frequency) = (3 qua Real) / 2 * fr; theorem :: MUSIC_S1:47 for frequency being Element of RAT_Music ex fr being positive Rational st frequency = fr & Fifth(RAT_Music,frequency) = (3 qua Rational) / 2 * fr; definition let MS be satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; attr MS is classical_fifth means :: MUSIC_S1:def 44 for frequency being Element of MS ex fr be positive Real st frequency = fr & Fifth(MS,frequency) = (3 qua Real) / 2 * fr; end; registration cluster classical_fifth for satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func REAL_Music -> classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func RAT_Music -> classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; begin :: Harmonic theorem :: MUSIC_S1:48 for MS being satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct for frequency being Element of MS holds 1-harmonique(MS,frequency) = frequency; theorem :: MUSIC_S1:49 for MS being satisfying_harmonique_stable satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct for a,b being Element of MS holds a,a equiv b,b; theorem :: MUSIC_S1:50 for MS being satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_tonic satisfying_interval satisfying_equiv MusicStruct for frequency being Element of MS holds octave(MS,frequency) = octave(MS); theorem :: MUSIC_S1:51 for MS being satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv non empty MusicStruct for frequency being Element of MS holds (ex seq being sequence of MS st seq.0 = frequency & (for n being Nat holds [seq.n,seq.(n+1)] in fifth(MS))); 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 < r3; end; definition let S be satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; attr S is satisfying_octave_constructible means :: MUSIC_S1:def 46 for frequency being Element of S holds ex o being Element of S st [frequency,o] in octave(S); end; theorem :: MUSIC_S1:52 for frequency be Element of REAL_Music holds ex fr,qr being positive Real st fr = frequency & qr = 2 * fr & [fr,qr] in octave(REAL_Music); theorem :: MUSIC_S1:53 REAL_Music is satisfying_octave_constructible; theorem :: MUSIC_S1:54 for frequency be Element of RAT_Music holds ex fr,qr being positive Rational st fr = frequency & qr = 2 * fr & [fr,qr] in octave(RAT_Music); theorem :: MUSIC_S1:55 RAT_Music is satisfying_octave_constructible; registration cluster satisfying_octave_constructible for classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func REAL_Music -> satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func RAT_Music -> satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition let MS be satisfying_octave_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; let frequency be Element of MS; func Octave(MS,frequency) -> Element of MS means :: MUSIC_S1:def 47 [frequency,it] in octave(MS); end; definition let MS be satisfying_Real non empty MusicStruct; let r be Element of MS; func @r -> positive Real equals :: MUSIC_S1:def 48 r; end; definition let MS be satisfying_octave_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; attr MS is classical_octave means :: MUSIC_S1:def 49 for frequency being Element of MS ex fr being positive Real st frequency = fr & Octave(MS,frequency) = 2 * fr; end; theorem :: MUSIC_S1:56 REAL_Music is classical_octave; theorem :: MUSIC_S1:57 RAT_Music is classical_octave; registration cluster classical_octave for satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func REAL_Music -> classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func RAT_Music -> classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition let MS be satisfying_octave_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct; attr MS is satisfying_octave_descendent_constructible means :: MUSIC_S1:def 50 for frequency being Element of MS holds ex o being Element of MS st [o,frequency] in octave(MS); end; theorem :: MUSIC_S1:58 for frequency be Element of REAL_Music holds ex fr,qr being positive Real st fr = frequency & qr = (1 qua Real) / 2 * fr & [qr,fr] in octave(REAL_Music); theorem :: MUSIC_S1:59 REAL_Music is satisfying_octave_descendent_constructible; theorem :: MUSIC_S1:60 for frequency be Element of RAT_Music holds ex fr,qr being positive Rational st fr = frequency & qr = (1 qua Rational) / 2 * fr & [qr,fr] in octave(RAT_Music); theorem :: MUSIC_S1:61 RAT_Music is satisfying_octave_descendent_constructible; registration cluster satisfying_octave_descendent_constructible for classical_octavesatisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func REAL_Music -> satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition redefine func RAT_Music -> satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; definition let MS be satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv MusicStruct; let frequency be Element of MS; func Octave_descendent(MS,frequency) -> Element of MS means :: MUSIC_S1:def 51 [it,frequency] in octave(MS); end; theorem :: MUSIC_S1:62 for MS being satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct for frequency being Element of MS holds ex r being positive Real st frequency = r & Octave_descendent(MS,frequency) = r / 2; theorem :: MUSIC_S1:63 for MS1,MS2 being classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv 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); theorem :: MUSIC_S1:64 for MS1,MS2 being satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty 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); definition let MS be satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv MusicStruct; let fondamentale,frequency be Element of MS; func Fifth_reduct(MS,fondamentale,frequency) -> Element of MS equals :: MUSIC_S1:def 52 Fifth(MS,frequency) if Fifth(MS,frequency) is_Between fondamentale,Octave(MS,fondamentale) otherwise Octave_descendent(MS,Fifth(MS,frequency)); end; theorem :: MUSIC_S1:65 for MS1,MS2 being satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty 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); theorem :: MUSIC_S1:66 for MS being classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct for frequency being Element of MS holds ex r,s being positive Real st r = frequency & s = (3 qua Real) / 2 * r & Fifth(MS,frequency) = s; theorem :: MUSIC_S1:67 for MS being satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_interval satisfying_equiv MusicStruct for fondamentale,frequency being Element of MS st frequency is_Between fondamentale,Octave(MS,fondamentale) ex r1,r2,r3 being positive Real st fondamentale = r1 & frequency = r2 & Octave(MS,fondamentale) = 2 * r1 & r1 <= r2 <= 2 * r1; theorem :: MUSIC_S1:68 for MS being satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty 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); definition mode MusicSpace is satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonique_stable satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct; end; theorem :: MUSIC_S1:69 REAL_Music is MusicSpace; theorem :: MUSIC_S1:70 RAT_Music is MusicSpace; begin :: Spiral of fifths theorem :: MUSIC_S1:71 for MS being satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv non empty MusicStruct for fondamentale,frequency being Element of MS holds (ex seq being sequence of MS st (seq.0 = frequency & for n being Nat holds seq.(n+1) = Fifth_reduct (MS,fondamentale,seq.(n)))); definition let MS be satisfying_octave_descendent_constructible satisfying_octave_constructible satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv non empty MusicStruct; let fondamentale,frequency be Element of MS; func spiral_of_fifths(MS,fondamentale,frequency) -> sequence of MS means :: MUSIC_S1:def 53 it.0 = frequency & for n being Nat holds it.(n+1) = Fifth_reduct (MS,fondamentale,it.n); end; reserve MS for satisfying_octave_descendent_constructible classical_octave satisfying_octave_constructible classical_fifth satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat satisfying_commutativity satisfying_interval satisfying_equiv satisfying_Real non empty MusicStruct, fondamentale,frequency for Element of MS; theorem :: MUSIC_S1:72 frequency is_Between fondamentale,Octave(MS,fondamentale) implies for n being Nat holds spiral_of_fifths(MS,fondamentale,frequency).n is_Between fondamentale,Octave(MS,fondamentale); theorem :: MUSIC_S1:73 spiral_of_fifths(MS,fondamentale,fondamentale).1 = (3 qua Real) / 2 * @fondamentale; theorem :: MUSIC_S1:74 spiral_of_fifths(MS,fondamentale,fondamentale).2 = (9 qua Real) / 8 * @fondamentale; theorem :: MUSIC_S1:75 spiral_of_fifths(MS,fondamentale,fondamentale).3 = (27 qua Real) / 16 * @fondamentale; theorem :: MUSIC_S1:76 spiral_of_fifths(MS,fondamentale,fondamentale).4 = (81 qua Real) / 64 * @fondamentale; theorem :: MUSIC_S1:77 spiral_of_fifths(MS,fondamentale,fondamentale).5 = (243 qua Real) / 128 * @fondamentale; theorem :: MUSIC_S1:78 @(spiral_of_fifths(MS,frequency,frequency).2) / @frequency = (3 * 3 qua Real) / (2 * 2 * 2); theorem :: MUSIC_S1:79 @(spiral_of_fifths(MS,frequency,frequency).4) / @(spiral_of_fifths(MS,frequency,frequency).2) = (3 * 3 qua Real) / (2 * 2 * 2); theorem :: MUSIC_S1:80 @(spiral_of_fifths(MS,frequency,frequency).1) / @(spiral_of_fifths(MS,frequency,frequency).4) = ((32 qua Real) / 27); theorem :: MUSIC_S1:81 @(spiral_of_fifths(MS,frequency,frequency).3) / @(spiral_of_fifths(MS,frequency,frequency).1) = ((9 qua Real) / 8); theorem :: MUSIC_S1:82 @Octave(MS,frequency) / @(spiral_of_fifths(MS,frequency,frequency).3) = ((32 qua Real) / 27); 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, r1,r2 being positive Real st scale.1 = frequency & scale.1 = r1 & scale.2 = r2 & r1 < r2 & scale.2 = Octave(MS,frequency); end; 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, r1,r2,r3 being positive Real st scale.1 = frequency & scale.1 = r1 & scale.2 = r2 & scale.3 = r3 & r1 < r2 < r3 & scale.3 = Octave(MS,frequency); end; 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, 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 < r3 & r3 < r4 & scale.4 = Octave(MS,frequency); end; 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, 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 < r3 & r3 < r4 < r5 & scale.5 = Octave(MS,frequency); end; 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 be Element of MS, r1,r2,r3,r4,r5,r6 be 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 < r3 & r3 < r4 < r5 & r5 < r6 & scale.6 = Octave(MS,frequency); end; 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, 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 < r3 & r3 < r4 < r5 & r5 < r6 < r7 & scale.7 = Octave(MS,frequency); end; 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, 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 < r3 & r3 < r4 < r5 & r5 < r6 < r7 & r7 < r8 & scale.8 = Octave(MS,frequency); end; 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, 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 < r3 & r3 < r4 < r5 & r5 < r6 < r7 & r7 < r8 < r9 & scale.9 = Octave(MS,frequency); end; begin :: Pentatonic pythagorean scale 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 :: 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); end; reserve MS for MusicSpace, fondamentale, frequency, f1, f2 for Element of MS; theorem :: MUSIC_S1:83 pentatonic_pythagorean_scale(MS,frequency) is pentatonic; definition let MS be MusicSpace; let f1,f2 be Element of MS; func intrval(f1,f2) -> positive Real means :: MUSIC_S1:def 63 ex r1,r2 being positive Real st r1 = f1 & r2 = f2 & it = r2 / r1; end; definition func pythagorean_tone -> positive Real equals :: MUSIC_S1:def 64 (9 qua Real) / 8; end; definition func pentatonic_pythagorean_semiditone -> positive Real equals :: MUSIC_S1:def 65 (32 qua Real) / 27; end; definition func major_third_pythagorean_tone -> positive Real equals :: MUSIC_S1:def 66 pythagorean_tone * pythagorean_tone; end; definition func pure_major_third -> positive Real equals :: MUSIC_S1:def 67 (5 qua Real) / 4; end; definition func syntonic_comma -> positive Real equals :: MUSIC_S1:def 68 major_third_pythagorean_tone / pure_major_third; end; theorem :: MUSIC_S1:84 syntonic_comma = (81 qua Real) / 80; theorem :: MUSIC_S1:85 pythagorean_tone < pentatonic_pythagorean_semiditone; theorem :: MUSIC_S1:86 pythagorean_tone * pythagorean_tone * pentatonic_pythagorean_semiditone * pythagorean_tone * pentatonic_pythagorean_semiditone = 2; definition let MS be MusicSpace; let frequency be Element of MS; func penta_fondamentale(MS,frequency) -> Element of MS equals :: MUSIC_S1:def 69 pentatonic_pythagorean_scale(MS,frequency).1; func penta_1(MS,frequency) -> Element of MS equals :: MUSIC_S1:def 70 pentatonic_pythagorean_scale(MS,frequency).2; func penta_2(MS,frequency) -> Element of MS equals :: MUSIC_S1:def 71 pentatonic_pythagorean_scale(MS,frequency).3; func penta_3(MS,frequency) -> Element of MS equals :: MUSIC_S1:def 72 pentatonic_pythagorean_scale(MS,frequency).4; func penta_4(MS,frequency) -> Element of MS equals :: MUSIC_S1:def 73 pentatonic_pythagorean_scale(MS,frequency).5; func penta_octave(MS,frequency) -> Element of MS equals :: MUSIC_S1:def 74 Octave(MS,frequency); end; theorem :: MUSIC_S1:87 ex r1,r2 being Element of REALPLUS st intrval(f1,f2) = REAL_ratio(r1,r2); theorem :: MUSIC_S1:88 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 qua Real) / 8 & r3 / r2 = (9 qua Real) / 8 & r4 / r3 = (32 qua Real) / 27 & r5 / r4 = (9 qua Real) / 8 & r6 / r5 = (32 qua Real) / 27; theorem :: MUSIC_S1:89 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 qua Real) / 8 & r3 / r2 = (9 qua Real) / 8 & r4 / r3 = (32 qua Real) / 27 & r5 / r4 = (9 qua Real) / 8 & r6 / r5 = (32 qua Real) / 27; theorem :: MUSIC_S1:90 (9 qua Real) / 8 = (9 qua Rational) / 8; theorem :: MUSIC_S1:91 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; theorem :: MUSIC_S1:92 Fifth(MS,frequency) is_Between frequency,Octave(MS,frequency); theorem :: MUSIC_S1:93 for r1,r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 qua Real) / 3 * r1 holds Fifth(MS,f2) = 2 * r1 & not Fifth(MS,f2) is_Between f1,Octave(MS,f1); theorem :: MUSIC_S1:94 for r1,r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 qua Real) / 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); theorem :: MUSIC_S1:95 for r1,r2 being positive Real st f1 = r1 & f2 = r2 & r2 = (4 qua Real) / 3 * r1 holds Fifth_reduct(MS,f1,f2) = f1; begin :: Heptatonic pythagorean scale definition let S be MusicSpace; attr S is satisfying_fourth_constructible means :: MUSIC_S1:def 75 for frequency being Element of S holds ex q being Element of S st [frequency,q] in fourth(S); end; theorem :: MUSIC_S1:96 for MS being MusicSpace st MS = REAL_Music holds for frequency being Element of MS holds ex fr,qr being positive Real st fr = frequency & qr = (4 qua Real) / 3 * fr & [fr,qr] in fourth(MS); theorem :: MUSIC_S1:97 REAL_Music is satisfying_fourth_constructible; registration cluster satisfying_fourth_constructible for MusicSpace; end; definition let MS be satisfying_fourth_constructible MusicSpace; let frequency be Element of MS; func Fourth(MS,frequency) -> Element of MS means :: MUSIC_S1:def 76 [frequency,it] in fourth(MS); end; definition let MS be satisfying_fourth_constructible MusicSpace; attr MS is classical_fourth means :: MUSIC_S1:def 77 for frequency being Element of MS ex fr being positive Real st frequency = fr & Fourth(MS,frequency) = (4 qua Real) / 3 * fr; end; theorem :: 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 qua Real) / 3 * fr; registration cluster classical_fourth for satisfying_fourth_constructible MusicSpace; end; definition let MS be satisfying_Real non empty MusicStruct; attr MS is satisfying_euclidean means :: MUSIC_S1:def 78 for f1,f2 being Element of MS holds (the Ratio of MS).(f1,f2) = @f2 / @f1; end; registration cluster satisfying_euclidean for satisfying_Real non empty MusicStruct; end; registration cluster satisfying_euclidean -> satisfying_interval for satisfying_Real non empty MusicStruct; end; registration cluster satisfying_euclidean -> satisfying_tonic for satisfying_Real non empty MusicStruct; end; registration cluster satisfying_euclidean -> satisfying_commutativity for satisfying_Real non empty MusicStruct; end; registration cluster satisfying_euclidean for classical_fourth satisfying_fourth_constructible MusicSpace; end; definition mode Heptatonic_Pythagorean_Score is classical_fourth satisfying_fourth_constructible MusicSpace; end; reserve HPS for Heptatonic_Pythagorean_Score, frequency for Element of HPS; 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 :: 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); end; theorem :: MUSIC_S1:99 Fourth(HPS,frequency) is_Between frequency,Octave(HPS,frequency); theorem :: MUSIC_S1:100 for n being Nat holds spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).n is_Between frequency,Octave(HPS,frequency); theorem :: MUSIC_S1:101 spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).1 = frequency; theorem :: MUSIC_S1:102 spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).2 = (3 qua Real) / 2 * @frequency; theorem :: MUSIC_S1:103 spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).3 = (9 qua Real) / 8 * @(frequency); theorem :: MUSIC_S1:104 spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).4 = (27 qua Real) / 16 * @frequency; theorem :: MUSIC_S1:105 spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).5 = (81 qua Real) / 64 * @frequency; theorem :: MUSIC_S1:106 spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).6 = (243 qua Real) / 128 * @frequency; theorem :: MUSIC_S1:107 heptatonic_pythagorean_scale(HPS,frequency).1 = 1 * @frequency & heptatonic_pythagorean_scale(HPS,frequency).2 = (9 qua Real) / 8 * @frequency & heptatonic_pythagorean_scale(HPS,frequency).3 = (81 qua Real) / 64 * @frequency & heptatonic_pythagorean_scale(HPS,frequency).4 = (4 qua Real) / 3 * @frequency & heptatonic_pythagorean_scale(HPS,frequency).5 = (3 qua Real) / 2 * @frequency & heptatonic_pythagorean_scale(HPS,frequency).6 = (27 qua Real) / 16 * @frequency & heptatonic_pythagorean_scale(HPS,frequency).7 = (243 qua Real) / 128 * @frequency & heptatonic_pythagorean_scale(HPS,frequency).8 = 2 * @frequency; theorem :: MUSIC_S1:108 heptatonic_pythagorean_scale(HPS,frequency) is heptatonic; definition func heptatonic_pythagorean_semitone -> positive Real equals :: MUSIC_S1:def 80 (256 qua Real) / 243; end; notation synonym limma_pythagoricien for heptatonic_pythagorean_semitone; end; notation synonym diatonic_tone for pythagorean_tone; end; theorem :: MUSIC_S1:109 pythagorean_tone / 2 < heptatonic_pythagorean_semitone; theorem :: MUSIC_S1:110 pythagorean_tone * pythagorean_tone * heptatonic_pythagorean_semitone * pythagorean_tone * pythagorean_tone * pythagorean_tone * heptatonic_pythagorean_semitone = 2; definition let HPS be Heptatonic_Pythagorean_Score; let frequency be Element of HPS; func hepta_fondamental(HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 81 heptatonic_pythagorean_scale(HPS,frequency).1; func hepta_1(HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 82 heptatonic_pythagorean_scale(HPS,frequency).2; func hepta_2(HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 83 heptatonic_pythagorean_scale(HPS,frequency).3; func hepta_3(HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 84 heptatonic_pythagorean_scale(HPS,frequency).4; func hepta_4(HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 85 heptatonic_pythagorean_scale(HPS,frequency).5; func hepta_5(HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 86 heptatonic_pythagorean_scale(HPS,frequency).6; func hepta_6(HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 87 heptatonic_pythagorean_scale(HPS,frequency).7; func hepta_octave(HPS,frequency) -> Element of HPS equals :: MUSIC_S1:def 88 Octave(HPS,frequency); end; theorem :: MUSIC_S1:111 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; reserve HPS for Heptatonic_Pythagorean_Score, frequency for Element of HPS; 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 :: 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; 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; 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)); end; theorem :: MUSIC_S1:113 heptatonic_pythagorean_scale_ascending(HPS,frequency).1 = 2 * @frequency & heptatonic_pythagorean_scale_ascending(HPS,frequency).2 = (9 qua Real) / 4 * @frequency & heptatonic_pythagorean_scale_ascending(HPS,frequency).3 = (81 qua Real) / 32 * @frequency & heptatonic_pythagorean_scale_ascending(HPS,frequency).4 = (8 qua Real) / 3 * @frequency & heptatonic_pythagorean_scale_ascending(HPS,frequency).5 = (3 qua Real) * @frequency & heptatonic_pythagorean_scale_ascending(HPS,frequency).6 = (27 qua Real) / 8 * @frequency & heptatonic_pythagorean_scale_ascending(HPS,frequency).7 = (243 qua Real) / 64 * @frequency & heptatonic_pythagorean_scale_ascending(HPS,frequency).8 = 4 * @frequency; theorem :: MUSIC_S1:114 heptatonic_pythagorean_scale(HPS,frequency).8 = heptatonic_pythagorean_scale_ascending(HPS,frequency).1; theorem :: MUSIC_S1:115 intrval(hepta_4(HPS,frequency), hepta_1(HPS,Octave(HPS,frequency))) = (3 qua Real) / 2 & intrval(hepta_5(HPS,frequency), hepta_2(HPS,Octave(HPS,frequency))) = (3 qua Real) / 2 & intrval(hepta_6(HPS,frequency), hepta_3(HPS,Octave(HPS,frequency))) <> (3 qua Real) / 2 & intrval(hepta_octave(HPS,frequency), hepta_4(HPS,Octave(HPS,frequency))) = (3 qua Real) / 2; theorem :: 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); 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); definition let HPS be MusicSpace; let n be non zero natural Number; let scale be Element of n-tuples_on the carrier of HPS; let i be Nat; func #(scale,i) -> Element of HPS equals :: MUSIC_S1:def 91 scale.i if i in Seg n otherwise the Element of HPS; end; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural 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; definition let HPS be MusicSpace; let n be non zero natural Number; let scale be Element of n-tuples_on the carrier of HPS; assume scale is heptatonic; attr scale is ionan means :: 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; definition let HPS be MusicSpace; let n be non zero natural 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; theorem :: MUSIC_S1:118 heptatonic_pythagorean_scale(HPS,frequency) is ionan;