:: {P}ythagorean Tuning: Pentatonic and Heptatonic Scale
:: by Roland Coghetto
::
:: Received September 29, 2018
:: Copyright (c) 2018-2019 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,
FINSEQ_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;