:: {P}ythagorean Tuning: Pentatonic and Heptatonic Scale
:: by Roland Coghetto
::
:: Received September 29, 2018
:: Copyright (c) 2018-2026 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;
definitions TARSKI;
equalities XBOOLE_0;
expansions TARSKI, RELAT_1;
theorems XREAL_1, XXREAL_0, XTUPLE_0, ZFMISC_1, TAXONOM1, RELAT_2, REAL_1,
XBOOLE_0, TARSKI, PARTIT_2, NUMBERS, XBOOLE_1, XCMPLX_1, PARTFUN1,
EQREL_1, ARYTM_3, ORDINAL1, FINSEQ_1, FINSEQ_2, FUNCT_1, NAT_LAT,
BINOP_1, FUNCT_2;
schemes RELSET_1, RECDEF_1, FINSEQ_1, NAT_1, FUNCT_2;
begin :: Preliminaries
theorem Th1:
for r being object holds r in REAL+ \ {0} iff r is positive Real
proof
let r be object;
hereby
assume r in REAL+ \ {0};
then r in {r where r is Real: 0 <= r} & not r in {0}
by REAL_1:1,XBOOLE_0:def 5;
then r <> 0 & ex s be Real st r = s & 0 <= s by TARSKI:def 1;
hence r is positive Real;
end;
assume r is positive Real;
then r in {r where r is Real: 0 <= r} & not r in {0} by TARSKI:def 1;
hence thesis by REAL_1:1,XBOOLE_0:def 5;
end;
registration
cluster positive for Rational;
existence
proof
1 is positive;
hence thesis;
end;
end;
definition
func RATPLUS -> non empty Subset of REAL+ equals
the set of all r where r is positive Rational;
coherence
proof
set X = the set of all r where r is positive Rational;
A1: the positive Rational in X;
X c= REAL+
proof
let x be object;
assume x in X;
then ex r be positive Rational st x = r;
hence x in REAL+ by REAL_1:1;
end;
hence thesis by A1;
end;
end;
theorem Th2:
for r being object holds r is Element of RATPLUS iff r is positive Rational
proof
let r be object;
hereby
assume r is Element of RATPLUS;
then r in the set of all r where r is positive Rational;
then ex s be positive Rational st r = s;
hence r is positive Rational;
end;
assume r is positive Rational;
then r in the set of all r where r is positive Rational;
hence r is Element of RATPLUS;
end;
theorem
RAT+ c= RAT
proof
not [0,0] in RAT+
proof
assume
A1: [0,0] in RAT+;
reconsider i = 0 as Element of omega by ORDINAL1:def 12;
i,i are_coprime & i <> {} & i <> 1 by A1,ARYTM_3:33;
hence contradiction;
end;
hence thesis by XBOOLE_1:7,ZFMISC_1:34,NUMBERS:def 3;
end;
definition
func REALPLUS -> non empty Subset of REAL+ equals REAL+ \ {0};
coherence
proof
1 in REAL+ & not 1 in {0} by REAL_1:1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 5;
end;
end;
theorem Th3:
NATPLUS c= RATPLUS
proof
let x be object;
assume
A1: x in NATPLUS;
then reconsider y = x as Nat;
0 < y by A1,NAT_LAT:def 6;
hence thesis;
end;
theorem Th4:
NATPLUS c= REALPLUS
proof
let x be object;
assume
A1: x in NATPLUS;
then reconsider y = x as Nat;
0 < y by A1,NAT_LAT:def 6;
hence thesis by Th1;
end;
theorem Th5:
RATPLUS c= REALPLUS
proof
let x be object;
assume x in RATPLUS;
then reconsider y = x as positive Rational by Th2;
0 < y;
hence thesis by Th1;
end;
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
[[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 :Def01:
ex r,s be positive Real st x = r & s = y & it = s / r;
existence
proof
reconsider r = x,s = y as positive Real by Th1;
reconsider t = s / r as positive Real;
t is Element of REALPLUS by Th1;
hence thesis;
end;
uniqueness;
end;
theorem Th6:
for a,b,c,d being Element of REALPLUS holds
REAL_ratio(a,b) = REAL_ratio(c,d) iff REAL_ratio(b,a) = REAL_ratio(d,c)
proof
let a,b,c,d be Element of REALPLUS;
consider r,s be positive Real such that
A1: a = r & b = s & REAL_ratio(a,b) = s/r by Def01;
consider r9,s9 be positive Real such that
A2: c = r9 & d = s9 & REAL_ratio(c,d) = s9/r9 by Def01;
consider r99,s99 be positive Real such that
A3: b = r99 & a = s99 & REAL_ratio(b,a) = s99/r99 by Def01;
consider r999,s999 be positive Real such that
A4: d = r999 & c = s999 & REAL_ratio(d,c) = s999/r999 by Def01;
hereby
assume
A5: REAL_ratio(a,b) = REAL_ratio(c,d);
1 / (s / r) = r / s by XCMPLX_1:57;
then r / s = r9 / s9 by A5,A1,A2,XCMPLX_1:57;
hence REAL_ratio(b,a) = REAL_ratio(d,c) by A1,A2,A3,Def01;
end;
assume
A6: REAL_ratio(b,a) = REAL_ratio(d,c);
1 / (s99 / r99) = r99 / s99 by XCMPLX_1:57;
then r99 / s99 = r999 / s999 by A6,A3,A4,XCMPLX_1:57;
hence REAL_ratio(a,b) = REAL_ratio(c,d) by Def01,A2,A4,A3;
end;
definition
func REAL_ratio -> Function of [:REALPLUS,REALPLUS:],REALPLUS means
:Def02:
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);
existence
proof
defpred P[object,object] means
ex x,y be Element of REALPLUS st $1 = [x,y] & $2 = REAL_ratio(x,y);
A1: for x be object st x in [:REALPLUS,REALPLUS:]
ex y be object st y in REALPLUS & P[x,y]
proof
let x be object;
assume x in [:REALPLUS,REALPLUS:];
then consider y,z be object such that
A2: y in REALPLUS & z in REALPLUS & x = [y,z] by ZFMISC_1:def 2;
reconsider y,z as Element of REALPLUS by A2;
REAL_ratio(y,z) is Element of REALPLUS;
hence thesis by A2;
end;
consider f be Function of [:REALPLUS,REALPLUS:], REALPLUS such that
A3: for x be object st x in [:REALPLUS,REALPLUS:] holds P[x,f.x]
from FUNCT_2:sch 1(A1);
take f;
now
let x be Element of [:REALPLUS,REALPLUS:];
assume x is Element of [:REALPLUS,REALPLUS:];
consider y,z be object such that
A4: y in REALPLUS & z in REALPLUS & x = [y,z] by ZFMISC_1:def 2;
reconsider y,z as Element of REALPLUS by A4;
take y,z;
thus x = [y,z] by A4;
thus f.x = REAL_ratio(y,z)
proof
consider x9,y9 be Element of REALPLUS such that
A5: x = [x9,y9] & f.x = REAL_ratio(x9,y9) by A3;
x9 = y & y9 = z by A4,A5,XTUPLE_0:1;
hence thesis by A5;
end;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of [:REALPLUS,REALPLUS:],REALPLUS such that
A6: for x being Element of [:REALPLUS,REALPLUS:] holds
ex y,z being Element of REALPLUS st x = [y,z] &
f1.x = REAL_ratio(y,z) and
A7: for x being Element of [:REALPLUS,REALPLUS:] holds
ex y,z being Element of REALPLUS st x = [y,z] &
f2.x = REAL_ratio(y,z);
now
dom f1 = [:REALPLUS,REALPLUS:] by PARTFUN1:def 2;
hence dom f1 = dom f2 by PARTFUN1:def 2;
hereby
let x be object;
assume x in dom f1;
then reconsider y = x as Element of [:REALPLUS,REALPLUS:];
consider z,t be Element of REALPLUS such that
A8: y = [z,t] & f1.y = REAL_ratio(z,t) by A6;
consider z9,t9 be Element of REALPLUS such that
A9: y = [z9,t9] & f2.y = REAL_ratio(z9,t9) by A7;
z = z9 & t = t9 by A8,A9,XTUPLE_0:1;
hence f1.x = f2.x by A8,A9;
end;
end;
hence f1 = f2 by FUNCT_1:2;
end;
end;
definition
func EQUIV_REAL_ratio -> Relation of
[:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:] means
:Def03:
for x,y being Element of [:REALPLUS,REALPLUS:] holds [x,y] in it iff
ex a,b,c,d being Element of REALPLUS st x = [a,b] & y = [c,d] &
REAL_ratio(a,b) = REAL_ratio(c,d);
existence
proof
defpred P[object,object] means ex a,b,c,d be Element of REALPLUS st
$1 = [a,b] & $2 = [c,d] & REAL_ratio(a,b) = REAL_ratio(c,d);
consider R being Relation of
[:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:] such that
A1: for x,y be object holds
[x,y] in R iff x in [:REALPLUS,REALPLUS:] & y in [:REALPLUS,REALPLUS:] &
P[x,y] from RELSET_1:sch 1;
for x,y being Element of [:REALPLUS,REALPLUS:] holds [x,y] in R 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) by A1;
hence thesis;
end;
uniqueness
proof
let R1,R2 be Relation of [:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:]
such that
A2: for x,y being Element of [:REALPLUS,REALPLUS:] holds [x,y] in R1 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) and
A3: for x,y being Element of [:REALPLUS,REALPLUS:] holds [x,y] in R2 iff
ex a,b,c,d being Element of REALPLUS st x = [a,b] & y = [c,d] &
REAL_ratio(a,b) = REAL_ratio(c,d);
for x,y be object holds [x,y] in R1 iff [x,y] in R2
proof
let x,y be object;
hereby
assume
A4: [x,y] in R1;
then reconsider x9 = x,y9 = y as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:87;
ex a,b,c,d being Element of REALPLUS st x9 = [a,b] & y9 = [c,d] &
REAL_ratio(a,b) = REAL_ratio(c,d) by A4,A2;
hence [x,y] in R2 by A3;
end;
assume
A5: [x,y] in R2;
then reconsider x9 = x,y9 = y as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:87;
ex a,b,c,d being Element of REALPLUS st x9 = [a,b] & y9 = [c,d] &
REAL_ratio(a,b) = REAL_ratio(c,d) by A3,A5;
hence [x,y] in R1 by A2;
end;
hence thesis;
end;
end;
definition
func REAL_Music -> MusicStruct equals
MusicStruct(# REALPLUS,EQUIV_REAL_ratio,REAL_ratio #);
coherence;
end;
theorem Th7:
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)))
proof
set T = REAL_Music;
thus T is non empty;
thus the carrier of T c= REALPLUS;
thus for f1,f2,f3,f4 being Element of T holds
(f1,f2 equiv f3,f4 iff
(the Ratio of T).(f1,f2) = (the Ratio of T).(f3,f4))
proof
let f1,f2,f3,f4 be Element of T;
reconsider x = [f1,f2],y=[f3,f4] as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:def 2;
consider y9,z9 be Element of REALPLUS such that
A1: x = [y9,z9] and
A2: REAL_ratio.x = REAL_ratio(y9,z9) by Def02;
consider y99,z99 be Element of REALPLUS such that
A3: y = [y99,z99] and
A4: REAL_ratio.y = REAL_ratio(y99,z99) by Def02;
hereby
assume f1,f2 equiv f3,f4;
then consider a,b,c,d be Element of REALPLUS such that
A5: x = [a,b] & y = [c,d] and
A6: REAL_ratio(a,b) = REAL_ratio(c,d) by Def03;
y9 = a & z9 = b & y99 = c & z99 = d by A1,A3,A5,XTUPLE_0:1;
then a = f1 & b = f2 & c = f3 & d = f4 &
(the Ratio of T).(a,b) = REAL_ratio(a,b) &
(the Ratio of T).(c,d) = REAL_ratio(c,d)
by XTUPLE_0:1,A2,A4,A5,BINOP_1:def 1;
hence (the Ratio of T).(f1,f2) = (the Ratio of T).(f3,f4) by A6;
end;
assume
A7: (the Ratio of T).(f1,f2) = (the Ratio of T).(f3,f4);
REAL_ratio(y9,z9) = REAL_ratio.(f1,f2) by A2,BINOP_1:def 1
.= REAL_ratio(y99,z99) by A7,A4,BINOP_1:def 1;
hence f1,f2 equiv f3,f4 by A1,A3,Def03;
end;
end;
theorem Th8:
for f1,f2,f3 being Element of REAL_Music st
(the Ratio of REAL_Music).(f1,f2) = (the Ratio of REAL_Music).(f1,f3)
holds f2 = f3
proof
set S = REAL_Music;
let f1,f2,f3 be Element of S;
assume
A1: (the Ratio of S).(f1,f2) = (the Ratio of S).(f1,f3);
reconsider x = [f1,f2],y = [f1,f3] as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:def 2;
consider y9,z9 be Element of REALPLUS such that
A2: x = [y9,z9] and
A3: REAL_ratio.x = REAL_ratio(y9,z9) by Def02;
consider y99,z99 be Element of REALPLUS such that
A4: y = [y99,z99] and
A5: REAL_ratio.y = REAL_ratio(y99,z99) by Def02;
consider r,s be positive Real such that
A6: y9 = r & s = z9 & REAL_ratio(y9,z9) = s / r by Def01;
consider r9,s9 be positive Real such that
A7: y99 = r9 & s9 = z99 & REAL_ratio(y99,z99) = s9 / r9 by Def01;
A8: y9 = f1 & z9 = f2 & y99 = f1 & z99 = f3 by A2,A4,XTUPLE_0:1;
REAL_ratio.(f1,f2) = REAL_ratio(y9,z9) &
REAL_ratio.(f1,f3) = REAL_ratio(y99,z99) by A5,A3,BINOP_1:def 1;
hence thesis by A6,A7,A8,A1,XCMPLX_1:53;
end;
theorem
NATPLUS c= the carrier of REAL_Music by Th4;
theorem Th9:
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])
proof
set S = REAL_Music;
now
let frequency be Element of S;
let n be non zero Nat;
reconsider f = frequency as positive Real by Th1;
reconsider harmonique = n * f as Element of S by Th1;
take harmonique;
reconsider x = 1,y = n as Element of S by Th1;
reconsider z = [x,y] as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:def 2;
consider x9,y9 be Element of REALPLUS such that
A1: z = [x9,y9] and
A2: REAL_ratio.z = REAL_ratio(x9,y9) by Def02;
reconsider z9 = [frequency,harmonique] as
Element of [:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider x99,y99 be Element of REALPLUS such that
A3: z9 = [x99,y99] and
A4: REAL_ratio.z9 = REAL_ratio(x99,y99) by Def02;
consider r,s be positive Real such that
A5: x9 = r & s = y9 & REAL_ratio(x9,y9) = s / r by Def01;
A6: r = 1 & s = n by A5,A1,XTUPLE_0:1;
consider r9,s9 be positive Real such that
A7: x99 = r9 & s9 = y99 & REAL_ratio(x99,y99) = s9 / r9 by Def01;
A8: r9 = frequency & s9 = harmonique by A7,A3,XTUPLE_0:1;
now
thus (the Ratio of S).(x,y) = n by A5,A6,A2,BINOP_1:def 1;
thus (the Ratio of S).(frequency,harmonique) = REAL_ratio(x99,y99)
by A4,BINOP_1:def 1
.= n by A7,A8,XCMPLX_1:89;
end;
then x,y equiv frequency,harmonique by Th7;
hence [frequency,harmonique] in Class(the Equidistance of S,[1,n])
by EQREL_1:18;
end;
hence thesis;
end;
theorem Th10:
for f1,f2,f3 being Element of REAL_Music st
(the Ratio of REAL_Music).(f1,f1) = (the Ratio of REAL_Music).(f2,f3)
holds f2 = f3
proof
let f1,f2,f3 be Element of REAL_Music;
assume
A1: (the Ratio of REAL_Music).(f1,f1) =
(the Ratio of REAL_Music).(f2,f3);
reconsider x = [f1,f1],y = [f2,f3] as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:def 2;
consider y9,z9 be Element of REALPLUS such that
A2: x = [y9,z9] and
A3: REAL_ratio.x = REAL_ratio(y9,z9) by Def02;
consider y99,z99 be Element of REALPLUS such that
A4: y = [y99,z99] and
A5: REAL_ratio.y = REAL_ratio(y99,z99) by Def02;
consider r,s be positive Real such that
A6: y9 = r & s = z9 & REAL_ratio(y9,z9) = s / r by Def01;
consider r9,s9 be positive Real such that
A7: y99 = r9 & s9 = z99 & REAL_ratio(y99,z99) = s9 / r9 by Def01;
A8: y9 = f1 & z9 = f1 & y99 = f2 & z99 = f3 by A2,A4,XTUPLE_0:1;
REAL_ratio.(f1,f1) = REAL_ratio(y9,z9) &
REAL_ratio.(f2,f3) = REAL_ratio(y99,z99) by A5,A3,BINOP_1:def 1;
hence f2 = f3 by A7,A8,XCMPLX_1:58,XCMPLX_1:60,A6,A1;
end;
theorem Th11:
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
proof
let f1,f2,fn1,fm1,fn2,fm2 be Element of REAL_Music;
let r1,r2 be positive Real;
::: assume f1 = r1 & f2 = r2;
now
let n,m be non zero Nat;
assume
A0: fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2;
reconsider z = [fn1,fm1] as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:def 2;
consider x9,y9 be Element of REALPLUS such that
A1: z = [x9,y9] and
A2: REAL_ratio.z = REAL_ratio(x9,y9) by Def02;
consider r,s be positive Real such that
A3: x9 = r & s = y9 & REAL_ratio(x9,y9) = s / r by Def01;
reconsider z9 = [fn2,fm2] as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:def 2;
consider x99,y99 be Element of REALPLUS such that
A4: z9 = [x99,y99] and
A5: REAL_ratio.z9 = REAL_ratio(x99,y99) by Def02;
consider r9,s9 be positive Real such that
A6: x99 = r9 & s9 = y99 & REAL_ratio(x99,y99) = s9 / r9 by Def01;
now
thus REAL_ratio.(fn1,fm1) = s / r by A3,A2,BINOP_1:def 1;
thus REAL_ratio.(fn2,fm2) = s9 / r9 by A6,A5,BINOP_1:def 1;
r = n * r1 & s = m * r1 &
r9 = n * r2 & s9 = m * r2 by A4,A6,A1,A3,A0,XTUPLE_0:1;
then s / r = (m qua Real) / (n qua Real) &
s9 / r9 = (m qua Real) / (n qua Real) by XCMPLX_1:91;
hence s / r = s9 / r9;
end;
hence fn1,fm1 equiv fn2,fm2 by Th7;
end;
hence thesis;
end;
theorem Th12:
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)
proof
let f1,f2,f3,f4 be Element of REAL_Music;
set MS = REAL_Music;
reconsider x = [f1,f2],y = [f3,f4] as Element of [:REALPLUS,REALPLUS:]
by ZFMISC_1:def 2;
consider y9,z9 be Element of REALPLUS such that
A1: x = [y9,z9] and
A2: REAL_ratio.x = REAL_ratio(y9,z9) by Def02;
consider y99,z99 be Element of REALPLUS such that
A3: y = [y99,z99] and
A4: REAL_ratio.y = REAL_ratio(y99,z99) by Def02;
reconsider x1 = [z9,y9],y1 = [z99,y99] as Element of [:REALPLUS,REALPLUS:];
consider y19,z19 be Element of REALPLUS such that
A5: x1 = [y19,z19] and
A6: REAL_ratio.x1 = REAL_ratio(y19,z19) by Def02;
consider y199,z199 be Element of REALPLUS such that
A7: y1 = [y199,z199] and
A8: REAL_ratio.y1 = REAL_ratio(y199,z199) by Def02;
A9: f1 = y9 & f2 = z9 & f3 = y99 & f4 = z99 by A1,A3,XTUPLE_0:1;
then
A10: f1 = z19 & f2 = y19 & f3 = z199 & f4 = y199 by A5,A7,XTUPLE_0:1;
A11: ((the Ratio of MS).(f2,f1)) = REAL_ratio(y19,z19) &
((the Ratio of MS).(f4,f3)) = REAL_ratio(y199,z199)
by A9,BINOP_1:def 1,A6,A8;
hereby
assume
A12: ((the Ratio of MS).(f1,f2) = (the Ratio of MS).(f3,f4));
REAL_ratio(y9,z9) = REAL_ratio.(f1,f2) by A2,BINOP_1:def 1
.= REAL_ratio(y99,z99) by A12,A4,BINOP_1:def 1;
hence (the Ratio of MS).(f2,f1) = (the Ratio of MS).(f4,f3)
by A9,A10,A11,Th6;
end;
assume
A13: (the Ratio of MS).(f2,f1) = (the Ratio of MS).(f4,f3);
REAL_ratio.(f1,f2) = REAL_ratio(z19,y19)
by BINOP_1:def 1,A9,A10,A2
.= REAL_ratio(z199,y199) by A13,A11,Th6
.= REAL_ratio.(f3,f4) by BINOP_1:def 1,A9,A10,A4;
hence ((the Ratio of MS).(f1,f2) = (the Ratio of MS).(f3,f4));
end;
begin :: Definition of RATPLUS
definition
let x,y be Element of RATPLUS;
func RAT_ratio(x,y) -> Element of RATPLUS means :Def04:
ex r,s be positive Rational st x = r & s = y & it = s / r;
existence
proof
reconsider r = x,s = y as positive Rational by Th2;
reconsider t = s / r as positive Rational;
t is Element of RATPLUS by Th2;
hence thesis;
end;
uniqueness;
end;
theorem Th13:
for a,b,c,d being Element of RATPLUS holds
RAT_ratio(a,b) = RAT_ratio(c,d) iff RAT_ratio(b,a) = RAT_ratio(d,c)
proof
let a,b,c,d be Element of RATPLUS;
consider r,s be positive Rational such that
A1: a = r & b = s & RAT_ratio(a,b) = s/r by Def04;
consider r9,s9 be positive Rational such that
A2: c = r9 & d = s9 & RAT_ratio(c,d) = s9/r9 by Def04;
consider r99,s99 be positive Rational such that
A3: b = r99 & a = s99 & RAT_ratio(b,a) = s99/r99 by Def04;
consider r999,s999 be positive Rational such that
A4: d = r999 & c = s999 & RAT_ratio(d,c) = s999/r999 by Def04;
hereby
assume
A5: RAT_ratio(a,b) = RAT_ratio(c,d);
1 / (s / r) = r / s by XCMPLX_1:57;
hence RAT_ratio(b,a) = RAT_ratio(d,c) by A1,A2,A3,A4,A5,XCMPLX_1:57;
end;
assume
A6: RAT_ratio(b,a) = RAT_ratio(d,c);
1 / (s99 / r99) = r99 / s99 by XCMPLX_1:57;
hence RAT_ratio(a,b) = RAT_ratio(c,d) by A1,A2,A3,A4,A6,XCMPLX_1:57;
end;
definition
func RAT_ratio -> Function of [:RATPLUS,RATPLUS:],RATPLUS means
:Def05:
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);
existence
proof
defpred P[object,object] means
ex x,y be Element of RATPLUS st $1 = [x,y] & $2 = RAT_ratio(x,y);
A1: for x be object st x in [:RATPLUS,RATPLUS:]
ex y be object st y in RATPLUS & P[x,y]
proof
let x be object;
assume x in [:RATPLUS,RATPLUS:];
then consider y,z be object such that
A2: y in RATPLUS & z in RATPLUS & x = [y,z] by ZFMISC_1:def 2;
reconsider y,z as Element of RATPLUS by A2;
RAT_ratio(y,z) is Element of RATPLUS;
hence thesis by A2;
end;
consider f be Function of [:RATPLUS,RATPLUS:], RATPLUS such that
A3: for x be object st x in [:RATPLUS,RATPLUS:] holds P[x,f.x]
from FUNCT_2:sch 1(A1);
take f;
now
let x be Element of [:RATPLUS,RATPLUS:];
assume x is Element of [:RATPLUS,RATPLUS:];
consider y,z be object such that
A4: y in RATPLUS & z in RATPLUS & x = [y,z] by ZFMISC_1:def 2;
reconsider y,z as Element of RATPLUS by A4;
take y,z;
thus x = [y,z] by A4;
thus f.x = RAT_ratio(y,z)
proof
consider x9,y9 be Element of RATPLUS such that
A5: x = [x9,y9] & f.x = RAT_ratio(x9,y9) by A3;
x9 = y & y9 = z by A4,A5,XTUPLE_0:1;
hence thesis by A5;
end;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of [:RATPLUS,RATPLUS:],RATPLUS such that
A6: for x being Element of [:RATPLUS,RATPLUS:] holds
ex y,z being Element of RATPLUS st x = [y,z] &
f1.x = RAT_ratio(y,z) and
A7: for x being Element of [:RATPLUS,RATPLUS:] holds
ex y,z being Element of RATPLUS st x = [y,z] &
f2.x = RAT_ratio(y,z);
now
dom f1 = [:RATPLUS,RATPLUS:] by PARTFUN1:def 2;
hence dom f1 = dom f2 by PARTFUN1:def 2;
hereby
let x be object;
assume x in dom f1;
then reconsider y = x as Element of [:RATPLUS,RATPLUS:];
consider z,t be Element of RATPLUS such that
A8: y = [z,t] & f1.y = RAT_ratio(z,t) by A6;
consider z9,t9 be Element of RATPLUS such that
A9: y = [z9,t9] & f2.y = RAT_ratio(z9,t9) by A7;
z = z9 & t = t9 by A8,A9,XTUPLE_0:1;
hence f1.x = f2.x by A8,A9;
end;
end;
hence f1 = f2 by FUNCT_1:2;
end;
end;
definition
func EQUIV_RAT_ratio ->
Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] means :Def06:
for x,y being Element of [:RATPLUS,RATPLUS:] holds [x,y] in it iff
ex a,b,c,d being Element of RATPLUS st x = [a,b] & y = [c,d] &
RAT_ratio(a,b) = RAT_ratio(c,d);
existence
proof
defpred P[object,object] means ex a,b,c,d be Element of RATPLUS st
$1 = [a,b] & $2 = [c,d] & RAT_ratio(a,b) = RAT_ratio(c,d);
consider R being Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:]
such that
A1: for x,y be object holds
[x,y] in R iff x in [:RATPLUS,RATPLUS:] & y in [:RATPLUS,RATPLUS:] &
P[x,y] from RELSET_1:sch 1;
for x,y being Element of [:RATPLUS,RATPLUS:] holds [x,y] in R 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) by A1;
hence thesis;
end;
uniqueness
proof
let R1,R2 be Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] such that
A2: for x,y being Element of [:RATPLUS,RATPLUS:] holds [x,y] in R1 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) and
A3: for x,y being Element of [:RATPLUS,RATPLUS:] holds [x,y] in R2 iff
ex a,b,c,d being Element of RATPLUS st x = [a,b] & y = [c,d] &
RAT_ratio(a,b) = RAT_ratio(c,d);
for x,y be object holds [x,y] in R1 iff [x,y] in R2
proof
let x,y be object;
hereby
assume
A4: [x,y] in R1;
then reconsider x9 = x,y9 = y as Element of [:RATPLUS,RATPLUS:]
by ZFMISC_1:87;
ex a,b,c,d being Element of RATPLUS st x9 = [a,b] & y9 = [c,d] &
RAT_ratio(a,b) = RAT_ratio(c,d) by A4,A2;
hence [x,y] in R2 by A3;
end;
assume
A5: [x,y] in R2;
then reconsider x9 = x,y9 = y as Element of [:RATPLUS,RATPLUS:]
by ZFMISC_1:87;
ex a,b,c,d being Element of RATPLUS st x9 = [a,b] & y9 = [c,d] &
RAT_ratio(a,b) = RAT_ratio(c,d) by A3,A5;
hence [x,y] in R1 by A2;
end;
hence thesis;
end;
end;
definition
func RAT_Music -> MusicStruct equals
MusicStruct(# RATPLUS,EQUIV_RAT_ratio,RAT_ratio #);
coherence;
end;
theorem Th14:
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)))
proof
set T = RAT_Music;
thus T is non empty;
thus the carrier of T c= REALPLUS by Th5;
thus for f1,f2,f3,f4 being Element of T holds
(f1,f2 equiv f3,f4 iff
(the Ratio of T).(f1,f2) = (the Ratio of T).(f3,f4))
proof
let f1,f2,f3,f4 be Element of T;
reconsider x = [f1,f2],y=[f3,f4] as Element of [:RATPLUS,RATPLUS:]
by ZFMISC_1:def 2;
consider y9,z9 be Element of RATPLUS such that
A1: x = [y9,z9] and
A2: RAT_ratio.x = RAT_ratio(y9,z9) by Def05;
consider y99,z99 be Element of RATPLUS such that
A3: y = [y99,z99] and
A4: RAT_ratio.y = RAT_ratio(y99,z99) by Def05;
hereby
assume f1,f2 equiv f3,f4;
then consider a,b,c,d be Element of RATPLUS such that
A5: x = [a,b] & y = [c,d] and
A6: RAT_ratio(a,b) = RAT_ratio(c,d) by Def06;
y9 = a & z9 = b & y99 = c & z99 = d by A1,A3,A5,XTUPLE_0:1;
then a = f1 & b = f2 & c = f3 & d = f4 &
(the Ratio of T).(a,b) = RAT_ratio(a,b) &
(the Ratio of T).(c,d) = RAT_ratio(c,d)
by XTUPLE_0:1,A2,A4,A5,BINOP_1:def 1;
hence (the Ratio of T).(f1,f2) = (the Ratio of T).(f3,f4) by A6;
end;
assume
A7: (the Ratio of T).(f1,f2) = (the Ratio of T).(f3,f4);
RAT_ratio(y9,z9) = RAT_ratio.(f1,f2) by A2,BINOP_1:def 1
.= RAT_ratio(y99,z99) by A7,A4,BINOP_1:def 1;
hence f1,f2 equiv f3,f4 by A1,A3,Def06;
end;
end;
theorem Th15:
for f1,f2,f3 being Element of RAT_Music st
(the Ratio of RAT_Music).(f1,f2) = (the Ratio of RAT_Music).(f1,f3)
holds f2 = f3
proof
set S = RAT_Music;
let f1,f2,f3 be Element of S;
assume
A1: (the Ratio of S).(f1,f2) = (the Ratio of S).(f1,f3);
reconsider x = [f1,f2],y = [f1,f3] as Element of [:RATPLUS,RATPLUS:]
by ZFMISC_1:def 2;
consider y9,z9 be Element of RATPLUS such that
A2: x = [y9,z9] and
A3: RAT_ratio.x = RAT_ratio(y9,z9) by Def05;
consider y99,z99 be Element of RATPLUS such that
A4: y = [y99,z99] and
A5: RAT_ratio.y = RAT_ratio(y99,z99) by Def05;
consider r,s be positive Rational such that
A6: y9 = r & s = z9 & RAT_ratio(y9,z9) = s / r by Def04;
consider r9,s9 be positive Rational such that
A7: y99 = r9 & s9 = z99 & RAT_ratio(y99,z99) = s9 / r9 by Def04;
A8: y9 = f1 & z9 = f2 & y99 = f1 & z99 = f3 by A2,A4,XTUPLE_0:1;
RAT_ratio.(f1,f2) = RAT_ratio(y9,z9) &
RAT_ratio.(f1,f3) = RAT_ratio(y99,z99) by A5,A3,BINOP_1:def 1;
hence thesis by A6,A7,A8,A1,XCMPLX_1:53;
end;
theorem
NATPLUS c= the carrier of RAT_Music by Th3;
theorem Th16:
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])
proof
set S = RAT_Music;
now
let frequency be Element of S;
let n be non zero Nat;
reconsider f = frequency as positive Rational by Th2;
reconsider harmonique = n * f as Element of S by Th2;
take harmonique;
reconsider x = 1,y = n as Element of S by Th2;
reconsider z = [x,y] as Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider x9,y9 be Element of RATPLUS such that
A1: z = [x9,y9] and
A2: RAT_ratio.z = RAT_ratio(x9,y9) by Def05;
reconsider z9 = [frequency,harmonique] as
Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider x99,y99 be Element of RATPLUS such that
A3: z9 = [x99,y99] and
A4: RAT_ratio.z9 = RAT_ratio(x99,y99) by Def05;
consider r,s be positive Rational such that
A5: x9 = r & s = y9 & RAT_ratio(x9,y9) = s / r by Def04;
A6: r = 1 & s = n by A5,A1,XTUPLE_0:1;
consider r9,s9 be positive Rational such that
A7: x99 = r9 & s9 = y99 & RAT_ratio(x99,y99) = s9 / r9 by Def04;
A8: r9 = frequency & s9 = harmonique by A7,A3,XTUPLE_0:1;
now
thus (the Ratio of S).(x,y) = n by A5,A6,A2,BINOP_1:def 1;
thus (the Ratio of S).(frequency,harmonique) = RAT_ratio(x99,y99)
by A4,BINOP_1:def 1
.= n by A7,A8,XCMPLX_1:89;
end;
then x,y equiv frequency,harmonique by Th14;
hence [frequency,harmonique] in Class(the Equidistance of S,[1,n])
by EQREL_1:18;
end;
hence thesis;
end;
theorem Th17:
for f1,f2,f3 being Element of RAT_Music st
(the Ratio of RAT_Music).(f1,f1) = (the Ratio of RAT_Music).(f2,f3) holds
f2 = f3
proof
let f1,f2,f3 be Element of RAT_Music;
assume
A1: (the Ratio of RAT_Music).(f1,f1) =
(the Ratio of RAT_Music).(f2,f3);
set S = RAT_Music;
reconsider x = [f1,f1],y = [f2,f3] as Element of [:RATPLUS,RATPLUS:]
by ZFMISC_1:def 2;
consider y9,z9 be Element of RATPLUS such that
A2: x = [y9,z9] and
A3: RAT_ratio.x = RAT_ratio(y9,z9) by Def05;
consider y99,z99 be Element of RATPLUS such that
A4: y = [y99,z99] and
A5: RAT_ratio.y = RAT_ratio(y99,z99) by Def05;
consider r,s be positive Rational such that
A6: y9 = r & s = z9 & RAT_ratio(y9,z9) = s / r by Def04;
consider r9,s9 be positive Rational such that
A7: y99 = r9 & s9 = z99 & RAT_ratio(y99,z99) = s9 / r9 by Def04;
A8: y9 = f1 & z9 = f1 & y99 = f2 & z99 = f3 by A2,A4,XTUPLE_0:1;
RAT_ratio.(f1,f1) = RAT_ratio(y9,z9) &
RAT_ratio.(f2,f3) = RAT_ratio(y99,z99) by A5,A3,BINOP_1:def 1;
hence f2 = f3 by A7,A8,XCMPLX_1:58,XCMPLX_1:60,A6,A1;
end;
theorem
for frequency being Element of RAT_Music
ex r being positive Real st frequency = r &
(for n being non zero Nat holds n * r is Element of RAT_Music)
proof
let frequency be Element of RAT_Music;
reconsider r = frequency as positive Rational by Th2;
take r;
now
let n be non zero Nat;
n * r in RATPLUS;
hence n * r is Element of RAT_Music;
end;
hence thesis;
end;
theorem Th18:
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
proof
let f1,f2,fn1,fm1,fn2,fm2 be Element of RAT_Music;
let r1,r2 be positive Rational;
::: assume f1 = r1 & f2 = r2;
now
let n,m be non zero Nat;
assume
A1: fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2;
reconsider z = [fn1,fm1] as Element of [:RATPLUS,RATPLUS:]
by ZFMISC_1:def 2;
consider x9,y9 be Element of RATPLUS such that
A2: z = [x9,y9] and
A3: RAT_ratio.z = RAT_ratio(x9,y9) by Def05;
consider r,s be positive Rational such that
A4: x9 = r & s = y9 & RAT_ratio(x9,y9) = s / r by Def04;
reconsider z9 = [fn2,fm2] as Element of [:RATPLUS,RATPLUS:]
by ZFMISC_1:def 2;
consider x99,y99 be Element of RATPLUS such that
A5: z9 = [x99,y99] and
A6: RAT_ratio.z9 = RAT_ratio(x99,y99) by Def05;
consider r9,s9 be positive Rational such that
A7: x99 = r9 & s9 = y99 & RAT_ratio(x99,y99) = s9 / r9 by Def04;
now
thus RAT_ratio.(fn1,fm1) = s / r by A3,A4,BINOP_1:def 1;
thus RAT_ratio.(fn2,fm2) = s9 / r9
by A6,A7,BINOP_1:def 1;
r = n * r1 & s = m * r1 &
r9 = n * r2 & s9 = m * r2 by A1,A2,A4,A5,A7,XTUPLE_0:1;
then s / r = (m qua Real) / (n qua Real) &
s9 / r9 = (m qua Real) / (n qua Real) by XCMPLX_1:91;
hence s / r = s9 / r9;
end;
hence fn1,fm1 equiv fn2,fm2 by Th14;
end;
hence thesis;
end;
theorem Th19:
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)
proof
let f1,f2,f3,f4 be Element of RAT_Music;
set MS = RAT_Music;
reconsider x = [f1,f2],y = [f3,f4] as Element of [:RATPLUS,RATPLUS:]
by ZFMISC_1:def 2;
consider y9,z9 be Element of RATPLUS such that
A1: x = [y9,z9] and
A2: RAT_ratio.x = RAT_ratio(y9,z9) by Def05;
consider y99,z99 be Element of RATPLUS such that
A3: y = [y99,z99] and
A4: RAT_ratio.y = RAT_ratio(y99,z99) by Def05;
reconsider x1 = [z9,y9],y1 = [z99,y99] as Element of [:RATPLUS,RATPLUS:];
consider y19,z19 be Element of RATPLUS such that
A5: x1 = [y19,z19] and
A6: RAT_ratio.x1 = RAT_ratio(y19,z19) by Def05;
consider y199,z199 be Element of RATPLUS such that
A7: y1 = [y199,z199] and
A8: RAT_ratio.y1 = RAT_ratio(y199,z199) by Def05;
A9: f1 = y9 & f2 = z9 & f3 = y99 & f4 = z99 by A1,A3,XTUPLE_0:1;
then
A10: f1 = z19 & f2 = y19 & f3 = z199 & f4 = y199 by A5,A7,XTUPLE_0:1;
A11: ((the Ratio of MS).(f2,f1)) = RAT_ratio(y19,z19) &
((the Ratio of MS).(f4,f3)) = RAT_ratio(y199,z199)
by A9,BINOP_1:def 1,A6,A8;
hereby
assume
A12: ((the Ratio of MS).(f1,f2) = (the Ratio of MS).(f3,f4));
RAT_ratio(y9,z9) = RAT_ratio.(f1,f2) by A2,BINOP_1:def 1
.= RAT_ratio(y99,z99) by A12,A4,BINOP_1:def 1;
hence (the Ratio of MS).(f2,f1) = (the Ratio of MS).(f4,f3)
by A9,A10,A11,Th13;
end;
assume
A13: (the Ratio of MS).(f2,f1) = (the Ratio of MS).(f4,f3);
RAT_ratio.(f1,f2) = RAT_ratio(z19,y19) by BINOP_1:def 1,A9,A10,A2
.= RAT_ratio(z199,y199) by A13,A11,Th13
.= RAT_ratio.(f3,f4) by BINOP_1:def 1,A9,A10,A4;
hence ((the Ratio of MS).(f1,f2) = (the Ratio of MS).(f3,f4));
end;
begin :: Musical structure and somes axioms
definition
let S be MusicStruct;
attr S is satisfying_Real means
:Def07a:
the carrier of S c= REALPLUS;
attr S is satisfying_equiv means
:Def08a:
for f1,f2,f3,f4 being Element of S holds
(f1,f2 equiv f3,f4 iff (the Ratio of S).(f1,f2) = (the Ratio of S).(f3,f4));
attr S is satisfying_interval means
:Def09a:
for f1,f2,f3 being Element of S st
(the Ratio of S).(f1,f2) = (the Ratio of S).(f1,f3) holds f2 = f3;
attr S is satisfying_tonic means
:Def10a:
for f1,f2,f3 being Element of S st
(the Ratio of S).(f1,f1) = (the Ratio of S).(f2,f3) holds f2 = f3;
attr S is satisfying_commutativity means
:Def11a:
for f1,f2,f3,f4 being Element of S holds
(the Ratio of S).(f1,f2) = (the Ratio of S).(f3,f4) iff
(the Ratio of S).(f2,f1) = (the Ratio of S).(f4,f3);
attr S is satisfying_Nat means
:Def12a:
NATPLUS c= the carrier of S;
attr S is satisfying_harmonic_closed means
:Def13a:
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;
existence
proof
set MS = REAL_Music;
take MS;
thus thesis by Th7,Th8,Th9,Th4,Th10,Th12;
end;
end;
definition
redefine func REAL_Music -> satisfying_harmonic_closed :: redefines REAL_Music (MUSIC_S1, definition)
satisfying_Nat satisfying_commutativity satisfying_tonic
satisfying_interval satisfying_equiv satisfying_Real
non empty MusicStruct;
coherence
proof
REAL_Music is satisfying_harmonic_closed &
REAL_Music is satisfying_Nat &
REAL_Music is satisfying_commutativity &
REAL_Music is satisfying_tonic &
REAL_Music is satisfying_interval &
REAL_Music is satisfying_equiv &
REAL_Music is satisfying_Real by Th9,Th4,Th12,Th10,Th8,Th7;
hence thesis;
end;
end;
definition
redefine func RAT_Music -> satisfying_harmonic_closed :: redefines RAT_Music (MUSIC_S1, definition)
satisfying_Nat satisfying_commutativity
satisfying_tonic satisfying_interval satisfying_equiv
satisfying_Real non empty MusicStruct;
coherence
proof
RAT_Music is satisfying_harmonic_closed &
RAT_Music is satisfying_Nat &
RAT_Music is satisfying_commutativity &
RAT_Music is satisfying_tonic &
RAT_Music is satisfying_interval &
RAT_Music is satisfying_equiv &
RAT_Music is satisfying_Real
by Th14,Th16,Th3,Th19,Th17,Th15;
hence thesis;
end;
end;
theorem Th20:
for S being satisfying_Nat MusicStruct
for n being non zero Nat holds n is Element of S
proof
let S be satisfying_Nat MusicStruct;
let n be non zero Nat;
A1: NATPLUS c= the carrier of S by Def12a;
n in NATPLUS by NAT_LAT:def 6;
hence thesis by A1;
end;
theorem Th21:
for MS being satisfying_equiv MusicStruct
for a,b being Element of MS holds
a,b equiv a,b
proof
let MS be satisfying_equiv MusicStruct;
let a,b be Element of MS;
(the Ratio of MS).(a,b) = (the Ratio of MS).(a,b);
hence thesis by Def08a;
end;
theorem Th22:
for MS being satisfying_equiv MusicStruct
for a,b,c,d being Element of MS holds
a,b equiv c,d iff c,d equiv a,b
proof
let MS be satisfying_equiv MusicStruct;
let a,b,c,d be Element of MS;
hereby
assume a,b equiv c,d;
then (the Ratio of MS).(a,b) = (the Ratio of MS).(c,d) by Def08a;
hence c,d equiv a,b by Def08a;
end;
assume c,d equiv a,b;
then (the Ratio of MS).(a,b) = (the Ratio of MS).(c,d) by Def08a;
hence a,b equiv c,d by Def08a;
end;
theorem Th23:
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
proof
let MS be satisfying_equiv MusicStruct;
let a,b,c,d,e,f be Element of MS;
assume a,b equiv c,d & c,d equiv e,f;
then (the Ratio of MS).(a,b) = (the Ratio of MS).(c,d) &
(the Ratio of MS).(c,d) = (the Ratio of MS).(e,f) by Def08a;
hence thesis by Def08a;
end;
theorem Th24:
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)
proof
let S be satisfying_interval satisfying_equiv MusicStruct;
let a,b,c be Element of S;
now
assume a,b equiv a,c;
then (the Ratio of S).(a,b) = (the Ratio of S).(a,c) by Def08a;
hence b = c by Def09a;
end;
hence thesis by Th21;
end;
reserve MS for satisfying_equiv MusicStruct;
reserve a,b,c,d,e,f for Element of MS;
theorem
a,a equiv a,a
proof
(the Ratio of MS).(a,a) = (the Ratio of MS).(a,a);
hence thesis by Def08a;
end;
theorem Th25:
the Equidistance of MS is_reflexive_in
[:the carrier of MS,the carrier of MS:]
proof
set R = the Equidistance of MS,
C = [:the carrier of MS,the carrier of MS:];
now
let x be object;
assume x in C;
then consider y,z be object such that
A1: y in the carrier of MS and
A2: z in the carrier of MS and
A3: x = [y,z] by ZFMISC_1:def 2;
reconsider y,z as Element of MS by A1,A2;
y,z equiv y,z by Th21;
hence [x,x] in R by A3;
end;
hence thesis by RELAT_2:def 1;
end;
theorem
MS is non empty implies
the Equidistance of MS is reflexive &
field the Equidistance of MS = [:the carrier of MS,the carrier of MS:]
proof
assume
A1: MS is non empty;
the Equidistance of MS is_reflexive_in
[:the carrier of MS,the carrier of MS:] by Th25;
hence thesis by A1,PARTIT_2:21;
end;
theorem Th26:
the Equidistance of MS is_symmetric_in
[:the carrier of MS,the carrier of MS:]
proof
set R = the Equidistance of MS,
C = [:the carrier of MS,the carrier of MS:];
now
let x,y be object;
assume that
A1: x in C and
A2: y in C and
A3: [x,y] in R;
consider x1,x2 be object such that
A4: x1 in the carrier of MS and
A5: x2 in the carrier of MS and
A6: x = [x1,x2] by A1,ZFMISC_1:def 2;
consider y1,y2 be object such that
A7: y1 in the carrier of MS and
A8: y2 in the carrier of MS and
A9: y = [y1,y2] by A2,ZFMISC_1:def 2;
reconsider x1,x2,y1,y2 as Element of MS by A4,A5,A7,A8;
x1,x2 equiv y1,y2 by A3,A6,A9;
then y1,y2 equiv x1,x2 by Th22;
hence [y,x] in R by A6,A9;
end;
hence thesis by RELAT_2:def 3;
end;
theorem Th27:
the Equidistance of MS is_transitive_in
[:the carrier of MS,the carrier of MS:]
proof
set R = the Equidistance of MS,
C = [:the carrier of MS,the carrier of MS:];
now
let x,y,z be object;
assume that
A1: x in C and
A2: y in C and
A3: z in C and
A4: [x,y] in R and
A5: [y,z] in R;
consider x1,x2 be object such that
A6: x1 in the carrier of MS and
A7: x2 in the carrier of MS and
A8: x = [x1,x2] by A1,ZFMISC_1:def 2;
consider y1,y2 be object such that
A9: y1 in the carrier of MS and
A10: y2 in the carrier of MS and
A11: y = [y1,y2] by A2,ZFMISC_1:def 2;
consider z1,z2 be object such that
A12: z1 in the carrier of MS and
A13: z2 in the carrier of MS and
A14: z = [z1,z2] by A3,ZFMISC_1:def 2;
reconsider x1,x2,y1,y2,z1,z2 as Element of MS
by A6,A7,A9,A10,A12,A13;
x1,x2 equiv y1,y2 & y1,y2 equiv z1,z2 by A4,A5,A8,A11,A14;
then x1,x2 equiv z1,z2 by Th23;
hence [x,z] in R by A8,A14;
end;
hence thesis by RELAT_2:def 8;
end;
theorem
the Equidistance of MS is Equivalence_Relation of
[:the carrier of MS,the carrier of MS:]
proof
set R = the Equidistance of MS,
C = [:the carrier of MS,the carrier of MS:];
now
dom R = C by Th25,TAXONOM1:3;
hence R is total by PARTFUN1:def 2;
field R = C & R is_symmetric_in C by Th25,Th26,PARTIT_2:9;
hence R is symmetric by RELAT_2:def 11;
field R = C & R is_transitive_in C by Th25,Th27,PARTIT_2:9;
hence R is transitive by RELAT_2:def 16;
end;
hence thesis;
end;
theorem Th28:
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
proof
let MS be satisfying_commutativity satisfying_equiv MusicStruct;
let a,b,c,d be Element of MS;
hereby
assume a,b equiv c,d;
then (the Ratio of MS).(a,b) = (the Ratio of MS).(c,d) by Def08a;
then (the Ratio of MS).(b,a) = (the Ratio of MS).(d,c) by Def11a;
hence b,a equiv d,c by Def08a;
end;
assume b,a equiv d,c;
then (the Ratio of MS).(b,a) = (the Ratio of MS).(d,c) by Def08a;
then (the Ratio of MS).(a,b) = (the Ratio of MS).(c,d) by Def11a;
hence a,b equiv c,d by Def08a;
end;
theorem Th29:
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
proof
let S be satisfying_tonic satisfying_equiv MusicStruct;
let a,b,c be Element of S;
assume a,a equiv b,c;
then (the Ratio of S).(a,a) = (the Ratio of S).(b,c) by Def08a;
hence thesis by Def10a;
end;
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 :Def08b:
[frequency,it] in Class(the Equidistance of S,[1,n]);
existence by Def13a;
uniqueness
proof
let h1,h2 be Element of S such that
A1: [frequency,h1] in Class(the Equidistance of S,[1,n]) and
A2: [frequency,h2] in Class(the Equidistance of S,[1,n]);
reconsider x = 1,y = n as Element of S by Th20;
now
x,y equiv frequency,h1 by A1,EQREL_1:18;
hence (the Ratio of S).(x,y) = (the Ratio of S).(frequency,h1) by Def08a;
x,y equiv frequency,h2 by A2,EQREL_1:18;
hence (the Ratio of S).(x,y) = (the Ratio of S).(frequency,h2) by Def08a;
end;
then frequency,h1 equiv frequency,h2 by Def08a;
hence thesis by Th24;
end;
end;
definition
let S be satisfying_Nat satisfying_interval
satisfying_harmonic_closed satisfying_equiv MusicStruct;
attr S is satisfying_linearite_harmonique means :Def09:
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 Th30:
REAL_Music is satisfying_linearite_harmonique
proof
set MS = REAL_Music;
now
let frequency be Element of MS;
let n be non zero Nat;
reconsider fr = frequency as positive Real by Th1;
take fr;
thus frequency = fr;
reconsider n1 = 1, n2 = n as Element of MS by Th20;
reconsider f2 = n * fr as Element of MS by Th1;
reconsider x = [n1,n2], y= [frequency,f2] as
Element of [:REALPLUS,REALPLUS:];
now
thus [frequency,n-harmonique(MS,frequency)] in
Class(the Equidistance of MS,[1,n]) by Def08b;
now
thus (the Ratio of MS).(n1,n2) = REAL_ratio.(n1,n2);
thus (the Ratio of MS).(frequency,f2) = REAL_ratio.(frequency,f2);
now
reconsider n19 = n1,n29 = n2,fr9 = fr, f29 = f2 as
Element of REALPLUS;
consider r,s be positive Real such that
A1: n19 = r & n29 = s & REAL_ratio(n19,n29) = s / r by Def01;
consider r9,s9 be positive Real such that
A2: fr9 = r9 & f29 = s9 & REAL_ratio(fr9,f29) = s9 / r9 by Def01;
consider y9,z9 be Element of REALPLUS such that
A3: x = [y9,z9] and
A4: REAL_ratio.x = REAL_ratio(y9,z9) by Def02;
consider y99,z99 be Element of REALPLUS such that
A5: y = [y99,z99] and
A6: REAL_ratio.y = REAL_ratio(y99,z99) by Def02;
A7: y9 = n1 & z9 = n2 & y99 = frequency & z99 = f2
by A3,A5,XTUPLE_0:1;
hence REAL_ratio.(n1,n2) = n by A1,A4,BINOP_1:def 1;
thus REAL_ratio.(frequency,f2) = s9 / r9 by A2,A7,A6,BINOP_1:def 1
.= n by A2,XCMPLX_1:89;
end;
hence REAL_ratio.(n1,n2) = REAL_ratio.(frequency,f2);
end;
then n1,n2 equiv frequency,f2 by Def08a;
hence [frequency,f2] in Class(the Equidistance of MS,[1,n])
by EQREL_1:18;
end;
hence n-harmonique(MS,frequency) = n * fr by Def08b;
end;
hence thesis;
end;
theorem Th31:
RAT_Music is satisfying_linearite_harmonique
proof
set MS = RAT_Music;
now
let frequency be Element of MS;
let n be non zero Nat;
reconsider fr = frequency as positive Rational by Th2;
reconsider fr2 = fr as positive Real;
take fr2;
thus frequency = fr2;
reconsider n1 = 1, n2 = n as Element of MS by Th20;
reconsider f2 = n * fr as Element of MS by Th2;
reconsider x = [n1,n2],y= [frequency,f2] as
Element of [:RATPLUS,RATPLUS:];
now
thus [frequency,n-harmonique(MS,frequency)] in
Class(the Equidistance of MS,[1,n]) by Def08b;
now
thus (the Ratio of MS).(n1,n2) = RAT_ratio.(n1,n2);
thus (the Ratio of MS).(frequency,f2) = RAT_ratio.(frequency,f2);
now
reconsider n19 = n1,n29 = n2,fr9 = fr, f29 = f2 as
Element of RATPLUS;
consider r,s be positive Rational such that
A1: n19 = r & n29 = s & RAT_ratio(n19,n29) = s/r by Def04;
consider r9,s9 be positive Rational such that
A2: fr9 = r9 & f29 = s9 & RAT_ratio(fr9,f29) = s9/r9 by Def04;
consider y9,z9 be Element of RATPLUS such that
A3: x = [y9,z9] and
A4: RAT_ratio.x = RAT_ratio(y9,z9) by Def05;
consider y99,z99 be Element of RATPLUS such that
A5: y = [y99,z99] and
A6: RAT_ratio.y = RAT_ratio(y99,z99) by Def05;
A7: y9 = n1 & z9 = n2 & y99 = frequency & z99 = f2
by A3,A5,XTUPLE_0:1;
hence RAT_ratio.(n1,n2) = n by A1,A4,BINOP_1:def 1;
thus RAT_ratio.(frequency,f2)
= s9 / r9 by A2,A7,A6,BINOP_1:def 1
.= n by A2,XCMPLX_1:89;
end;
hence RAT_ratio.(n1,n2) = RAT_ratio.(frequency,f2);
end;
then n1,n2 equiv frequency,f2 by Def08a;
hence [frequency,f2] in Class(the Equidistance of MS,[1,n])
by EQREL_1:18;
end;
hence n-harmonique(MS,frequency) = n * fr2 by Def08b;
end;
hence thesis;
end;
registration
cluster satisfying_linearite_harmonique for
satisfying_harmonic_closed satisfying_Nat
satisfying_commutativity satisfying_tonic
satisfying_interval satisfying_equiv satisfying_Real
non empty MusicStruct;
existence by Th30;
end;
definition
redefine func REAL_Music -> satisfying_linearite_harmonique :: redefines REAL_Music (MUSIC_S1, definition)
satisfying_harmonic_closed satisfying_Nat
satisfying_commutativity satisfying_tonic
satisfying_interval satisfying_equiv satisfying_Real
non empty MusicStruct;
coherence by Th30;
end;
definition
redefine func RAT_Music -> satisfying_linearite_harmonique :: redefines RAT_Music (MUSIC_S1, definition)
satisfying_harmonic_closed satisfying_Nat
satisfying_commutativity satisfying_tonic satisfying_interval
satisfying_equiv satisfying_Real non empty MusicStruct;
coherence by Th31;
end;
definition
let MS be satisfying_harmonic_closed satisfying_Nat satisfying_interval
satisfying_equiv MusicStruct;
attr MS is satisfying_harmonique_stable means :Def10:
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 Th32:
REAL_Music is satisfying_harmonique_stable
proof
set MS = REAL_Music;
let f1,f2 be Element of MS;
let n,m be non zero Nat;
reconsider r1 = f1,r2 = f2 as positive Real by Th1;
(ex fr1 be positive Real st fr1 = f1 &
n-harmonique(MS,f1) = n * fr1) &
(ex fr2 be positive Real st fr2 = f1 &
m-harmonique(MS,f1) = m * fr2) &
(ex fr3 be positive Real st fr3 = f2 &
n-harmonique(MS,f2) = n * fr3) &
(ex fr4 be positive Real st fr4 = f2 &
m-harmonique(MS,f2) = m * fr4) by Def09;
hence n-harmonique(MS,f1),m-harmonique(MS,f1) equiv
n-harmonique(MS,f2),m-harmonique(MS,f2) by Th11;
end;
theorem Th33:
RAT_Music is satisfying_harmonique_stable
proof
set MS = RAT_Music;
now
let f1,f2 be Element of MS;
let n,m be non zero Nat;
set fn1 = n-harmonique(MS,f1), fm1 = m-harmonique(MS,f1),
fn2 = n-harmonique(MS,f2), fm2 = m-harmonique(MS,f2);
reconsider r1 = f1,r2 = f2 as positive Rational by Th2;
consider fr1 be positive Real such that
A1: fr1 = f1 and
A2: n-harmonique(MS,f1) = n * fr1 by Def09;
consider fr2 be positive Real such that
A3: fr2 = f1 and
A4: m-harmonique(MS,f1) = m * fr2 by Def09;
consider fr3 be positive Real such that
A5: fr3 = f2 and
A6: n-harmonique(MS,f2) = n * fr3 by Def09;
consider fr4 be positive Real such that
A7: fr4 = f2 and
A8: m-harmonique(MS,f2) = m * fr4 by Def09;
fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2
by A1,A2,A3,A4,A5,A6,A7,A8;
hence n-harmonique(MS,f1),m-harmonique(MS,f1) equiv
n-harmonique(MS,f2),m-harmonique(MS,f2) by Th18;
end;
hence thesis;
end;
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;
existence by Th32;
end;
definition
redefine func REAL_Music -> satisfying_harmonique_stable :: redefines REAL_Music (MUSIC_S1, definition)
satisfying_linearite_harmonique satisfying_harmonic_closed
satisfying_Nat satisfying_commutativity
satisfying_tonic satisfying_interval
satisfying_equiv satisfying_Real non empty MusicStruct;
coherence by Th32;
end;
definition
redefine func RAT_Music -> satisfying_harmonique_stable :: redefines RAT_Music (MUSIC_S1, definition)
satisfying_linearite_harmonique satisfying_harmonic_closed
satisfying_Nat satisfying_commutativity satisfying_tonic
satisfying_interval satisfying_equiv satisfying_Real
non empty MusicStruct;
coherence by Th33;
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
Class(the Equidistance of MS,
[1-harmonique(MS,frequency),1-harmonique(MS,frequency)]);
coherence;
func octave(MS,frequency) ->
Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,
[1-harmonique(MS,frequency),2-harmonique(MS,frequency)]);
coherence;
func fifth(MS,frequency) ->
Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,
[2-harmonique(MS,frequency),3-harmonique(MS,frequency)]);
coherence;
func fourth(MS,frequency)->
Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,
[3-harmonique(MS,frequency),4-harmonique(MS,frequency)]);
coherence;
func major_sixth(MS,frequency)->
Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,
[3-harmonique(MS,frequency),5-harmonique(MS,frequency)]);
coherence;
func major_third(MS,frequency)->
Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,
[4-harmonique(MS,frequency),5-harmonique(MS,frequency)]);
coherence;
func minor_third(MS,frequency)->
Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,
[5-harmonique(MS,frequency),6-harmonique(MS,frequency)]);
coherence;
func minor_sixth(MS,frequency)->
Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,
[5-harmonique(MS,frequency),8-harmonique(MS,frequency)]);
coherence;
func major_tone(MS,frequency)->
Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,
[8-harmonique(MS,frequency),9-harmonique(MS,frequency)]);
coherence;
func minor_tone(MS,frequency)->
Subset of [:the carrier of MS,the carrier of MS:]equals
Class(the Equidistance of MS,
[9-harmonique(MS,frequency),10-harmonique(MS,frequency)]);
coherence;
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
Class(the Equidistance of MS,[1,1]);
coherence;
func octave(MS) -> Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,[1,2]);
coherence;
func fifth(MS) -> Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,[2,3]);
coherence;
func fourth(MS)-> Subset of [:the carrier of MS,the carrier of MS:] equals
Class(the Equidistance of MS,[3,4]);
coherence;
func major_sixth(MS)-> Subset of [:the carrier of MS,the carrier of MS:]
equals Class(the Equidistance of MS,[3,5]);
coherence;
func major_third(MS)-> Subset of [:the carrier of MS,the carrier of MS:]
equals Class(the Equidistance of MS,[4,5]);
coherence;
func minor_third(MS)-> Subset of [:the carrier of MS,the carrier of MS:]
equals Class(the Equidistance of MS,[5,6]);
coherence;
func minor_sixth(MS)-> Subset of [:the carrier of MS,the carrier of MS:]
equals Class(the Equidistance of MS,[5,8]);
coherence;
func major_tone(MS)-> Subset of [:the carrier of MS,the carrier of MS:]
equals Class(the Equidistance of MS,[8,9]);
coherence;
func minor_tone(MS)-> Subset of [:the carrier of MS,the carrier of MS:]
equals Class(the Equidistance of MS,[9,10]);
coherence;
end;
definition
let S be satisfying_harmonic_closed satisfying_Nat
satisfying_interval satisfying_equiv MusicStruct;
attr S is satisfying_fifth_constructible means :Def11:
for frequency being Element of S holds ex q being Element of S st
[frequency,q] in fifth(S);
end;
theorem Th34:
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)
proof
set MS = REAL_Music;
now
let frequency be Element of MS;
reconsider f = frequency as positive Real by Th1;
reconsider qr = (3 qua Real) / 2 * f as positive Real;
reconsider q = qr as Element of MS by Th1;
take f,qr;
thus f = frequency;
thus qr = (3 qua Real) / 2 * f;
reconsider n2 = 2,n3 = 3 as Element of MS by Th20;
reconsider x = [n2,n3],y = [frequency,q] as
Element of [:REALPLUS,REALPLUS:];
reconsider z = [frequency,q] as Element of [:REALPLUS,REALPLUS:];
consider x9,y9 be Element of REALPLUS such that
A1: z = [x9,y9] and
A2: REAL_ratio.z = REAL_ratio(x9,y9) by Def02;
consider r,s be positive Real such that
A3: x9 = r & s = y9 & REAL_ratio(x9,y9) = s / r by Def01;
consider x99,y99 be Element of REALPLUS such that
A4: x = [x99,y99] and
A5: REAL_ratio.x = REAL_ratio(x99,y99) by Def02;
consider r9,s9 be positive Real such that
A6: x99 = r9 & s9 = y99 & REAL_ratio(x99,y99) = s9 / r9 by Def01;
A7: n2 = r9 & n3 = s9 & r = frequency & s = q
by A3,A1,A4,A6,XTUPLE_0:1;
now
thus REAL_ratio.(n2,n3) = (3 qua Real) / (2 qua Real)
by A6,A7,A5,BINOP_1:def 1;
thus REAL_ratio.(frequency,q) = s / r by A2,A3,BINOP_1:def 1
.= (3 qua Real) / 2 by A7,XCMPLX_1:89;
end;
then n2,n3 equiv frequency,q by Def08a;
hence [f,qr] in fifth(MS) by EQREL_1:18;
end;
hence thesis;
end;
theorem Th35:
REAL_Music is satisfying_fifth_constructible
proof
set MS = REAL_Music;
let frequency be Element of MS;
consider fr,qr be positive Real such that
A1: fr = frequency and
qr = (3 qua Real) / 2 * fr and
A2: [fr,qr] in fifth(MS) by Th34;
fr is Element of MS & qr is Element of MS by Th1;
hence thesis by A1,A2;
end;
theorem Th36:
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)
proof
set MS = RAT_Music;
now
let frequency be Element of MS;
reconsider f = frequency as positive Rational by Th2;
reconsider qr = (3 qua Rational) / 2 * f as positive Rational;
reconsider q = qr as Element of MS by Th2;
take f,qr;
thus f = frequency;
thus qr = (3 qua Rational) / 2 * f;
reconsider n2 = 2,n3 = 3 as Element of MS by Th20;
reconsider x = [n2,n3],y = [frequency,q] as
Element of [:RATPLUS,RATPLUS:];
reconsider z = [frequency,q] as Element of [:RATPLUS,RATPLUS:];
consider x9,y9 be Element of RATPLUS such that
A1: z = [x9,y9] and
A2: RAT_ratio.z = RAT_ratio(x9,y9) by Def05;
consider r,s be positive Rational such that
A3: x9 = r & s = y9 & RAT_ratio(x9,y9) = s / r by Def04;
consider x99,y99 be Element of RATPLUS such that
A4: x = [x99,y99] and
A5: RAT_ratio.x = RAT_ratio(x99,y99) by Def05;
consider r9,s9 be positive Rational such that
A6: x99 = r9 & s9 = y99 & RAT_ratio(x99,y99) = s9 / r9 by Def04;
A7: n2 = r9 & n3 = s9 & r = frequency & s = q
by A3,A1,A4,A6,XTUPLE_0:1;
now
thus RAT_ratio.(n2,n3) = (3 qua Real) / (2 qua Real)
by A5,A6,A7,BINOP_1:def 1;
thus RAT_ratio.(frequency,q) = RAT_ratio(x9,y9)
by A2,BINOP_1:def 1
.= (3 qua Rational) / 2
by A3,A7,XCMPLX_1:89;
end;
then n2,n3 equiv frequency,q by Def08a;
hence [f,qr] in fifth(MS) by EQREL_1:18;
end;
hence thesis;
end;
theorem Th37:
RAT_Music is satisfying_fifth_constructible
proof
set MS = RAT_Music;
let frequency be Element of MS;
consider fr,qr be positive Rational such that
A1: fr = frequency and
qr = (3 qua Rational) / 2 * fr and
A2: [fr,qr] in fifth(MS) by Th36;
fr is Element of MS & qr is Element of MS by Th2;
hence thesis by A1,A2;
end;
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;
existence by Th35;
end;
definition
redefine func REAL_Music -> satisfying_fifth_constructible :: redefines REAL_Music (MUSIC_S1, definition)
satisfying_harmonique_stable satisfying_linearite_harmonique
satisfying_harmonic_closed satisfying_Nat satisfying_commutativity
satisfying_tonic satisfying_interval satisfying_equiv
satisfying_Real non empty MusicStruct;
coherence by Th35;
end;
definition
redefine func RAT_Music -> satisfying_fifth_constructible :: redefines RAT_Music (MUSIC_S1, definition)
satisfying_harmonique_stable satisfying_linearite_harmonique
satisfying_harmonic_closed satisfying_Nat satisfying_commutativity
satisfying_tonic satisfying_interval satisfying_equiv
satisfying_Real non empty MusicStruct;
coherence by Th37;
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
:Def11bis:
[frequency,it] in fifth(MS);
existence by Def11;
uniqueness
proof
let q1,q2 be Element of MS such that
A1: [frequency,q1] in fifth(MS) and
A2: [frequency,q2] in fifth(MS);
reconsider n2 = 2,n3 = 3 as Element of MS by Th20;
A3: n2,n3 equiv frequency,q1 by A1,EQREL_1:18;
n2,n3 equiv frequency,q2 by A2,EQREL_1:18;
then frequency,q2 equiv n2,n3 by Th22;
hence thesis by A3,Th23,Th24;
end;
end;
theorem
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)
proof
let MS be satisfying_fifth_constructible satisfying_harmonique_stable
satisfying_linearite_harmonique satisfying_harmonic_closed satisfying_Nat
satisfying_interval satisfying_equiv MusicStruct;
let frequency be Element of MS;
A0: now
let x be object;
assume
A1: x in fifth(MS,frequency);
then consider x1,x2 be object such that
A2: x1 in the carrier of MS and
A3: x2 in the carrier of MS and
A4: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1,x2 as Element of MS by A2,A3;
reconsider y = 1, y1 = 2,y2 = 3 as Element of MS by Th20;
set z = 2-harmonique(MS,frequency),
t = 3-harmonique(MS,frequency);
reconsider n = 2,m = 3 as non zero Nat;
consider r1 be positive Real such that
A5: y = r1 and
A6: n-harmonique(MS,y) = n * r1 by Def09;
consider r2 be positive Real such that
A7: y = r2 and
A8: m-harmonique(MS,y) = m * r2 by Def09;
set a = n-harmonique(MS,frequency), b = m-harmonique(MS,frequency);
A9: a,b equiv x1,x2 by A1,A4,EQREL_1:18;
y1,y2 equiv a,b by A5,A6,A7,A8,Def10;
then y1,y2 equiv x1,x2 by A9,Th23;
hence x in fifth(MS) by A4,EQREL_1:18;
end;
now
let x be object;
assume
A11: x in fifth(MS);
then consider x1,x2 be object such that
A12: x1 in the carrier of MS and
A13: x2 in the carrier of MS and
A14: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1,x2 as Element of MS by A12,A13;
reconsider y = 2,z = 3 as Element of MS by Th20;
reconsider y9 = y as positive Real;
reconsider n = 2,m = 3 as non zero Nat;
set a = n-harmonique(MS,frequency), b = m-harmonique(MS,frequency),
c = n-harmonique(MS,y), d = m-harmonique(MS,y);
A15: a,b equiv c,d by Def10;
reconsider n0 = 1,n1 = 2,n2 = 3 as Element of MS by Th20;
consider r1 be positive Real such that
A16: n0 = r1 and
A17: n-harmonique(MS,n0) = n * r1 by Def09;
consider r2 be positive Real such that
A18: n0 = r2 and
A19: m-harmonique(MS,n0) = m * r2 by Def09;
A20: n-harmonique(MS,n0),m-harmonique(MS,n0) equiv x1,x2
by A16,A17,A18,A19,A11,A14,EQREL_1:18;
c,d equiv n-harmonique(MS,n0),m-harmonique(MS,n0) by Def10;
then c,d equiv x1,x2 by A20,Th23;
then a,b equiv x1,x2 by A15,Th23;
hence x in fifth(MS,frequency) by A14,EQREL_1:18;
end;
hence thesis by A0;
end;
theorem Th38:
for frequency being Element of REAL_Music
ex fr being positive Real st frequency = fr &
Fifth(REAL_Music,frequency) = (3 qua Real) / 2 * fr
proof
set MS = REAL_Music;
let frequency be Element of MS;
reconsider fr = frequency as positive Real by Th1;
take fr;
thus frequency = fr;
consider fr9,qr9 be positive Real such that
A1: fr9 = frequency and
A2: qr9 = (3 qua Real) / 2 * fr9 and
A3: [fr9,qr9] in fifth(MS) by Th34;
reconsider qr9 as Element of MS by Th1;
qr9 = Fifth(MS,frequency) by A1,A3,Def11bis;
hence thesis by A1,A2;
end;
theorem Th39:
for frequency being Element of RAT_Music ex fr being positive Rational st
frequency = fr & Fifth(RAT_Music,frequency) = (3 qua Rational) / 2 * fr
proof
set MS = RAT_Music;
let frequency be Element of MS;
reconsider fr = frequency as positive Rational by Th2;
take fr;
thus frequency = fr;
consider fr9,qr9 be positive Rational such that
A1: fr9 = frequency and
A2: qr9 = (3 qua Rational) / 2 * fr9 and
A3: [fr9,qr9] in fifth(MS) by Th36;
reconsider qr9 as Element of MS by Th2;
qr9 = Fifth(MS,frequency) by A1,A3,Def11bis;
hence thesis by A1,A2;
end;
definition
let MS be satisfying_fifth_constructible satisfying_harmonic_closed
satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;
attr MS is classical_fifth means :Def12:
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;
existence
proof
take REAL_Music;
thus thesis by Th38;
end;
end;
definition
redefine func REAL_Music -> classical_fifth satisfying_fifth_constructible :: redefines REAL_Music (MUSIC_S1, definition)
satisfying_harmonique_stable satisfying_linearite_harmonique
satisfying_harmonic_closed satisfying_Nat satisfying_commutativity
satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real
non empty MusicStruct;
coherence by Def12,Th38;
end;
definition
redefine func RAT_Music -> classical_fifth satisfying_fifth_constructible :: redefines RAT_Music (MUSIC_S1, definition)
satisfying_harmonique_stable satisfying_linearite_harmonique
satisfying_harmonic_closed satisfying_Nat satisfying_commutativity
satisfying_tonic satisfying_interval satisfying_equiv satisfying_Real
non empty MusicStruct;
coherence
proof
now
thus RAT_Music is 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;
for frequency being Element of RAT_Music ex fr be positive Real st
frequency = fr & Fifth(RAT_Music,frequency) = (3 qua Real) / 2 * fr
proof
let frequency be Element of RAT_Music;
ex fr be positive Rational st frequency = fr &
Fifth(RAT_Music,frequency) = (3 qua Rational) / 2 * fr by Th39;
hence thesis;
end;
hence thesis by Def12;
end;
hence thesis;
end;
end;
begin :: Harmonic
theorem Th40:
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
proof
let MS be satisfying_harmonic_closed satisfying_Nat
satisfying_tonic satisfying_interval satisfying_equiv MusicStruct;
let frequency be Element of MS;
A1: NATPLUS c= the carrier of MS by Def12a;
1 in NATPLUS by NAT_LAT:def 6;
then reconsider x = 1 as Element of MS by A1;
[frequency,1-harmonique(MS,frequency)] in
Class(the Equidistance of MS,[1,1]) by Def08b;
then x,x equiv frequency,1-harmonique(MS,frequency) by EQREL_1:18;
hence thesis by Th29;
end;
theorem
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
proof
let MS be satisfying_harmonique_stable satisfying_harmonic_closed
satisfying_Nat satisfying_tonic satisfying_interval
satisfying_equiv MusicStruct;
let a,b be Element of MS;
1-harmonique(MS,a) = a & 1-harmonique(MS,b) = b by Th40;
hence thesis by Def10;
end;
theorem
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)
proof
let MS be satisfying_harmonique_stable satisfying_linearite_harmonique
satisfying_harmonic_closed satisfying_Nat satisfying_tonic
satisfying_interval satisfying_equiv MusicStruct;
let frequency be Element of MS;
A1: now
let x be object;
assume
A2: x in octave(MS,frequency);
then consider x1,x2 be object such that
A3: x1 in the carrier of MS and
A4: x2 in the carrier of MS and
A5: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1,x2 as Element of MS by A3,A4;
A6: NATPLUS c= the carrier of MS by Def12a;
1 in NATPLUS & 2 in NATPLUS by NAT_LAT:def 6;
then reconsider y1 = 1,y2 = 2 as Element of MS by A6;
set z = 1-harmonique(MS,frequency),
t = 2-harmonique(MS,frequency);
reconsider n = 1,m = 2 as non zero Nat;
consider r2 be positive Real such that
A7: y1 = r2 and
A8: m-harmonique(MS,y1) = m * r2 by Def09;
set a = n-harmonique(MS,frequency), b = m-harmonique(MS,frequency);
A9: y1 = n-harmonique(MS,y1) by Th40;
A10: a,b equiv x1,x2 by A2,A5,EQREL_1:18;
y1,y2 equiv a,b by A9,A7,A8,Def10;
then y1,y2 equiv x1,x2 by A10,Th23;
hence x in octave(MS) by A5,EQREL_1:18;
end;
now
let x be object;
assume
A11: x in octave(MS);
then consider x1,x2 be object such that
A12: x1 in the carrier of MS and
A13: x2 in the carrier of MS and
A14: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1,x2 as Element of MS by A12,A13;
A15: NATPLUS c= the carrier of MS by Def12a;
1 in NATPLUS & 2 in NATPLUS by NAT_LAT:def 6;
then reconsider y = 1,z = 2 as Element of MS by A15;
reconsider y9 = y as positive Real;
reconsider n = 1,m = 2 as non zero Nat;
set a = n-harmonique(MS,frequency), b = m-harmonique(MS,frequency),
c = n-harmonique(MS,y), d = m-harmonique(MS,y);
A16: a,b equiv c,d by Def10;
reconsider n1 = 1,n2 = 2 as Element of MS by Th20;
consider r1 be positive Real such that
A17: n1 = r1 and
A18: n-harmonique(MS,n1) = n * r1 by Def09;
consider r2 be positive Real such that
A19: n1 = r2 and
A20: m-harmonique(MS,n1) = m * r2 by Def09;
n1,n2 equiv x1,x2 by A11,A14,EQREL_1:18;
then a,b equiv x1,x2 by A16,A17,A18,A19,A20,Th23;
hence x in octave(MS,frequency) by A14,EQREL_1:18;
end;
hence thesis by A1;
end;
theorem
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)))
proof
let MS be satisfying_fifth_constructible satisfying_harmonic_closed
satisfying_Nat satisfying_interval satisfying_equiv non empty
MusicStruct;
let frequency be Element of MS;
defpred P[set,set,set] means
ex x,y be positive Real st [$2,$3] in fifth(MS);
A1: for n be Nat for x be Element of MS ex y being Element of MS
st P[n,x,y]
proof
let n be Nat;
let x be Element of MS;
ex q be Element of MS st [x,q] in fifth(MS) by Def11;
hence thesis;
end;
consider seq be sequence of MS such that
A2: seq.0 = frequency and
A3: for n be Nat holds P[n,seq.n,seq.(n+1)]
from RECDEF_1:sch 2(A1);
take seq;
now
thus seq.0 = frequency by A2;
hereby
let n be Nat;
P[n,seq.n,seq.(n+1)] by A3;
hence [seq.n,seq.(n+1)] in fifth(MS);
end;
end;
hence thesis;
end;
definition
let MS be MusicStruct;
let a,b,c be Element of MS;
pred b is_Between a,c means
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 :Def13:
for frequency being Element of S holds ex o being Element of S st
[frequency,o] in octave(S);
end;
theorem Th41:
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)
proof
set MS = REAL_Music;
now
let frequency be Element of MS;
reconsider f = frequency as positive Real by Th1;
reconsider qr = 2 * f as positive Real;
reconsider q = qr as Element of MS by Th1;
take f,qr;
thus f = frequency;
thus qr = 2 * f;
reconsider n2 = 1,n3 = 2 as Element of MS by Th20;
reconsider x = [n2,n3],y = [frequency,q] as
Element of [:REALPLUS,REALPLUS:];
reconsider z = [frequency,q] as Element of [:REALPLUS,REALPLUS:];
consider x9,y9 be Element of REALPLUS such that
A1: z = [x9,y9] and
A2: REAL_ratio.z = REAL_ratio(x9,y9) by Def02;
consider r,s be positive Real such that
A3: x9 = r & s = y9 & REAL_ratio(x9,y9) = s / r by Def01;
consider x99,y99 be Element of REALPLUS such that
A4: x = [x99,y99] and
A5: REAL_ratio.x = REAL_ratio(x99,y99) by Def02;
consider r9,s9 be positive Real such that
A6: x99 = r9 & s9 = y99 & REAL_ratio(x99,y99) = s9 / r9 by Def01;
A7: n2 = r9 & n3 = s9 & r = frequency & s = q
by A3,A1,A4,A6,XTUPLE_0:1;
now
thus REAL_ratio.(n2,n3) = (2 qua Real) / (1 qua Real)
by A7,A6,A5,BINOP_1:def 1;
thus REAL_ratio.(frequency,q) = REAL_ratio.z by BINOP_1:def 1
.= 2 by A2,A3,A7,XCMPLX_1:89;
end;
then n2,n3 equiv frequency,q by Def08a;
hence [f,qr] in octave(MS) by EQREL_1:18;
end;
hence thesis;
end;
theorem Th42:
REAL_Music is satisfying_octave_constructible
proof
let frequency be Element of REAL_Music;
consider fr,qr be positive Real such that
A1: fr = frequency and qr = 2 * fr and
A2: [fr,qr] in octave(REAL_Music) by Th41;
fr is Element of REAL_Music & qr is Element of REAL_Music by Th1;
hence thesis by A1,A2;
end;
theorem Th43:
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)
proof
now
let frequency be Element of RAT_Music;
reconsider f = frequency as positive Rational by Th2;
reconsider qr = 2 * f as positive Rational;
reconsider q = qr as Element of RAT_Music by Th2;
take f,qr;
thus f = frequency;
thus qr = 2 * f;
reconsider n2 = 1,n3 = 2 as Element of RAT_Music by Th20;
reconsider x = [n2,n3],y = [frequency,q] as
Element of [:RATPLUS,RATPLUS:];
reconsider z = [frequency,q] as Element of [:RATPLUS,RATPLUS:];
consider x9,y9 be Element of RATPLUS such that
A1: z = [x9,y9] and
A2: RAT_ratio.z = RAT_ratio(x9,y9) by Def05;
consider r,s be positive Rational such that
A3: x9 = r & s = y9 & RAT_ratio(x9,y9) = s / r by Def04;
consider x99,y99 be Element of RATPLUS such that
A4: x = [x99,y99] and
A5: RAT_ratio.x = RAT_ratio(x99,y99) by Def05;
consider r9,s9 be positive Rational such that
A6: x99 = r9 & s9 = y99 & RAT_ratio(x99,y99) = s9 / r9 by Def04;
A7: n2 = r9 & n3 = s9 & r = frequency & s = q
by A3,A1,A4,A6,XTUPLE_0:1;
now
thus RAT_ratio.(n2,n3) = (2 qua Rational) / 1
by BINOP_1:def 1,A7,A5,A6;
thus RAT_ratio.(frequency,q) = RAT_ratio(x9,y9)
by A2,BINOP_1:def 1
.= 2 by A7,A3,XCMPLX_1:89;
end;
then n2,n3 equiv frequency,q by Def08a;
hence [f,qr] in octave(RAT_Music) by EQREL_1:18;
end;
hence thesis;
end;
theorem Th44:
RAT_Music is satisfying_octave_constructible
proof
let frequency be Element of RAT_Music;
consider fr,qr be positive Rational such that
A1: fr = frequency and
qr = 2 * fr and
A2: [fr,qr] in octave(RAT_Music) by Th43;
fr is Element of RAT_Music & qr is Element of RAT_Music by Th2;
hence thesis by A1,A2;
end;
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;
existence by Th42;
end;
definition
redefine func REAL_Music -> satisfying_octave_constructible classical_fifth :: redefines REAL_Music (MUSIC_S1, definition)
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;
coherence by Th42;
end;
definition
redefine func RAT_Music -> satisfying_octave_constructible classical_fifth :: redefines RAT_Music (MUSIC_S1, definition)
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;
coherence by Th44;
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
:Def14:
[frequency,it] in octave(MS);
existence by Def13;
uniqueness
proof
let q1,q2 be Element of MS such that
A1: [frequency,q1] in octave(MS) and
A2: [frequency,q2] in octave(MS);
reconsider n1 = 1,n2 = 2 as Element of MS by Th20;
A3: n1,n2 equiv frequency,q1 by A1,EQREL_1:18;
n1,n2 equiv frequency,q2 by A2,EQREL_1:18;
then frequency,q2 equiv n1,n2 by Th22;
hence thesis by A3,Th23,Th24;
end;
end;
definition
let MS be satisfying_Real non empty MusicStruct;
let r be Element of MS;
func @r -> positive Real equals r;
coherence
proof
the carrier of MS c= REALPLUS by Def07a;
hence thesis by Th1;
end;
end;
definition
let MS be satisfying_octave_constructible satisfying_harmonic_closed
satisfying_Nat satisfying_interval satisfying_equiv MusicStruct;
attr MS is classical_octave means :Def15:
for frequency being Element of MS
ex fr being positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr;
end;
theorem Th45:
REAL_Music is classical_octave
proof
set MS = REAL_Music;
for frequency being Element of MS
ex fr be positive Real st
frequency = fr & Octave(MS,frequency) = 2 * fr
proof
let frequency be Element of MS;
consider fr,qr be positive Real such that
A1: fr = frequency and
A2: qr = 2 * fr and
A3: [fr,qr] in octave(MS) by Th41;
reconsider qr as Element of MS by Th1;
[frequency,qr] in octave(MS) by A1,A3;
then Octave(MS,frequency) = 2 * fr by Def14,A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th46:
RAT_Music is classical_octave
proof
set MS = RAT_Music;
for frequency being Element of MS
ex fr be positive Real st
frequency = fr & Octave(MS,frequency) = 2 * fr
proof
let frequency be Element of MS;
consider fr,qr be positive Rational such that
A1: fr = frequency and
A2: qr = 2 * fr and
A3: [fr,qr] in octave(MS) by Th43;
reconsider qr as Element of MS by Th2;
[frequency,qr] in octave(MS) by A1,A3;
then Octave(MS,frequency) = 2 * fr by Def14,A2;
hence thesis by A1;
end;
hence thesis;
end;
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;
existence by Th45;
end;
definition
redefine func REAL_Music -> classical_octave satisfying_octave_constructible :: redefines REAL_Music (MUSIC_S1, definition)
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;
coherence by Th45;
end;
definition
redefine func RAT_Music -> classical_octave satisfying_octave_constructible :: redefines RAT_Music (MUSIC_S1, definition)
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;
coherence by Th46;
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 :Def16:
for frequency being Element of MS holds ex o being Element of MS st
[o,frequency] in octave(MS);
end;
theorem Th47:
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)
proof
set MS = REAL_Music;
now
let frequency be Element of MS;
reconsider f = frequency as positive Real by Th1;
reconsider qr = (1 qua Real) / 2 * f as positive Real;
reconsider q = qr as Element of MS by Th1;
take f,qr;
thus f = frequency;
thus qr = (1 qua Real) / 2 * f;
reconsider n2 = 2,n3 = 1 as Element of MS by Th20;
reconsider x = [n2,n3],y = [frequency,q] as
Element of [:REALPLUS,REALPLUS:];
reconsider z = [frequency,q] as Element of [:REALPLUS,REALPLUS:];
consider x9,y9 be Element of REALPLUS such that
A1: z = [x9,y9] and
A2: REAL_ratio.z = REAL_ratio(x9,y9) by Def02;
consider r,s be positive Real such that
A3: x9 = r & s = y9 & REAL_ratio(x9,y9) = s / r by Def01;
consider x99,y99 be Element of REALPLUS such that
A4: x = [x99,y99] and
A5: REAL_ratio.x = REAL_ratio(x99,y99) by Def02;
consider r9,s9 be positive Real such that
A6: x99 = r9 & s9 = y99 & REAL_ratio(x99,y99) = s9 / r9 by Def01;
A7: n2 = r9 & n3 = s9 & r = frequency & s = q
by A3,A1,A4,A6,XTUPLE_0:1;
now
thus REAL_ratio.(n2,n3) = (1 qua Real) / (2 qua Real)
by A6,A7,A5,BINOP_1:def 1;
thus REAL_ratio.(frequency,q) = s / r by A3,A2,BINOP_1:def 1
.= (1 qua Real) / 2 by A7,XCMPLX_1:89;
end;
then n2,n3 equiv frequency,q by Def08a;
then n3,n2 equiv q,frequency by Th28;
hence [qr,f] in octave(MS) by EQREL_1:18;
end;
hence thesis;
end;
theorem Th48:
REAL_Music is satisfying_octave_descendent_constructible
proof
let frequency be Element of REAL_Music;
consider fr,qr be positive Real such that
A2: fr = frequency and
qr = (1 qua Real) / 2 * fr and
A4: [qr,fr] in octave(REAL_Music) by Th47;
fr is Element of REAL_Music & qr is Element of REAL_Music by Th1;
hence thesis by A2,A4;
end;
theorem Th49:
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)
proof
set MS = RAT_Music;
now
let frequency be Element of MS;
reconsider f = frequency as positive Rational by Th2;
reconsider qr = (1 qua Rational) / 2 * f as positive Rational;
reconsider q = qr as Element of MS by Th2;
take f,qr;
thus f = frequency;
thus qr = (1 qua Rational) / 2 * f;
reconsider n2 = 2,n3 = 1 as Element of MS by Th20;
reconsider x = [n2,n3],y = [frequency,q] as
Element of [:RATPLUS,RATPLUS:];
reconsider z = [frequency,q] as Element of [:RATPLUS,RATPLUS:];
consider x9,y9 be Element of RATPLUS such that
A1: z = [x9,y9] and
A2: RAT_ratio.z = RAT_ratio(x9,y9) by Def05;
consider r,s be positive Rational such that
A3: x9 = r & s = y9 & RAT_ratio(x9,y9) = s / r by Def04;
consider x99,y99 be Element of RATPLUS such that
A4: x = [x99,y99] and
A5: RAT_ratio.x = RAT_ratio(x99,y99) by Def05;
consider r9,s9 be positive Rational such that
A6: x99 = r9 & s9 = y99 & RAT_ratio(x99,y99) = s9 / r9 by Def04;
A7: n2 = r9 & n3 = s9 & r = frequency & s = q
by A3,A1,A4,A6,XTUPLE_0:1;
now
thus RAT_ratio.(n2,n3) = (1 qua Real) / (2 qua Real)
by A6,A7,A5,BINOP_1:def 1;
thus RAT_ratio.(frequency,q) = s / r by A2,A3,BINOP_1:def 1
.= (1 qua Rational) / 2 by A7,XCMPLX_1:89;
end;
then n2,n3 equiv frequency,q by Def08a;
then n3,n2 equiv q,frequency by Th28;
hence [qr,f] in octave(MS) by EQREL_1:18;
end;
hence thesis;
end;
theorem Th50:
RAT_Music is satisfying_octave_descendent_constructible
proof
let frequency be Element of RAT_Music;
consider fr,qr be positive Rational such that
A1: fr = frequency and
qr = (1 qua Rational) / 2 * fr and
A2: [qr,fr] in octave(RAT_Music) by Th49;
fr is Element of RAT_Music & qr is Element of RAT_Music by Th2;
hence thesis by A1,A2;
end;
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;
existence by Th48;
end;
definition
redefine func REAL_Music -> satisfying_octave_descendent_constructible :: redefines REAL_Music (MUSIC_S1, definition)
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;
coherence by Th48;
end;
definition
redefine func RAT_Music -> satisfying_octave_descendent_constructible :: redefines RAT_Music (MUSIC_S1, definition)
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;
coherence by Th50;
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
:Def17:
[it,frequency] in octave(MS);
existence by Def16;
uniqueness
proof
let q1,q2 be Element of MS such that
A1: [q1,frequency] in octave(MS) and
A2: [q2,frequency] in octave(MS);
reconsider n1 = 1,n2 = 2 as Element of MS by Th20;
A3: n1,n2 equiv q1,frequency by A1,EQREL_1:18;
n1,n2 equiv q2,frequency by A2,EQREL_1:18;
then q2,frequency equiv n1,n2 by Th22;
then q2,frequency equiv q1,frequency by A3,Th23;
hence thesis by Th24,Th28;
end;
end;
theorem Th51:
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
proof
let MS be 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;
let frequency be Element of MS;
A1: the carrier of MS c= REALPLUS by Def07a;
then reconsider r = frequency as positive Real by Th1;
reconsider r2 = r/2 as positive Real;
set ff = Octave_descendent(MS,frequency);
reconsider rff = ff as positive Real by A1,Th1;
A2: [ff,frequency] in octave(MS) &
[ff,Octave(MS,ff)] in octave(MS) by Def14,Def17;
ex fr be positive Real st
ff = fr & Octave(MS,ff) = 2 * fr by Def15;
then frequency = 2 * rff by A2,Def14;
then rff = r / 2;
hence thesis;
end;
theorem Th52:
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)
proof
let MS1,MS2 be classical_octave satisfying_octave_constructible
classical_fifth satisfying_fifth_constructible
satisfying_harmonic_closed satisfying_Nat satisfying_interval
satisfying_equiv MusicStruct;
let f1 be Element of MS1;
let f2 be Element of MS2;
assume
A1: f1 = f2;
consider fr1 be positive Real such that
A2: f1 = fr1 & Fifth(MS1,f1) = (3 qua Real) / 2 * fr1 by Def12;
consider fr2 be positive Real such that
A3: f2 = fr2 & Fifth(MS2,f2) = (3 qua Real) / 2 * fr2 by Def12;
thus Fifth(MS1,f1) = Fifth(MS2,f2) by A1,A2,A3;
(ex fr be positive Real st f1 = fr & Octave(MS1,f1) = 2 * fr) &
(ex fr be positive Real st f2 = fr & Octave(MS2,f2) = 2 * fr)
by Def15;
hence thesis by A1;
end;
theorem Th53:
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)
proof
let MS1,MS2 be 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;
let frequency1 be Element of MS1;
let frequency2 be Element of MS2;
assume
A1: frequency1 = frequency2;
consider r1 be positive Real such that
A2: frequency1 = r1 & Octave_descendent(MS1,frequency1) = r1 / 2 by Th51;
consider r2 be positive Real such that
A3: frequency2 = r2 & Octave_descendent(MS2,frequency2) = r2 / 2 by Th51;
thus thesis by A1,A2,A3;
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 fondamentale,frequency be Element of MS;
func Fifth_reduct(MS,fondamentale,frequency) -> Element of MS
equals
:Def18:
Fifth(MS,frequency) if Fifth(MS,frequency) is_Between
fondamentale,Octave(MS,fondamentale) otherwise
Octave_descendent(MS,Fifth(MS,frequency));
correctness;
end;
theorem
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)
proof
let MS1,MS2 be 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;
let frequency1,fondamentale1 be Element of MS1;
let frequency2,fondamentale2 be Element of MS2;
assume that
A1: frequency1 = frequency2 and
A2: fondamentale1 = fondamentale2;
per cases;
suppose
A3: Fifth(MS1,frequency1) is_Between
fondamentale1,Octave(MS1,fondamentale1); then
A4: Fifth_reduct(MS1,fondamentale1,frequency1) = Fifth(MS1,frequency1)
by Def18;
Fifth(MS1,frequency1) = Fifth(MS2,frequency2) &
fondamentale1 = fondamentale2 &
Octave(MS2,fondamentale2)=Octave(MS1,fondamentale1) by A1,A2,Th52;
then Fifth(MS2,frequency2) is_Between
fondamentale2,Octave(MS2,fondamentale2) by A3;
then Fifth(MS2,frequency2)
= Fifth_reduct(MS2,fondamentale2,frequency2)
by Def18;
hence thesis by A4,A1,Th52;
end;
suppose
A5: not Fifth(MS1,frequency1) is_Between
fondamentale1,Octave(MS1,fondamentale1);
then
A6: Fifth_reduct(MS1,fondamentale1,frequency1)
= Octave_descendent(MS1,Fifth(MS1,frequency1))
by Def18;
Fifth(MS1,frequency1) = Fifth(MS2,frequency2) &
fondamentale1 = fondamentale2 &
Octave(MS2,fondamentale2)=Octave(MS1,fondamentale1) by A1,A2,Th52;
then not Fifth(MS2,frequency2) is_Between
fondamentale2,Octave(MS2,fondamentale2) by A5; then
A7: Fifth_reduct(MS2,fondamentale2,frequency2)
= Octave_descendent(MS2,Fifth(MS2,frequency2)) by Def18;
Fifth(MS1,frequency1) = Fifth(MS2,frequency2) by A1,Th52;
hence thesis by A6,A7,Th53;
end;
end;
theorem Th54:
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
proof
let MS be classical_fifth satisfying_fifth_constructible
satisfying_harmonic_closed satisfying_Nat satisfying_interval
satisfying_equiv MusicStruct;
let frequency be Element of MS;
consider fr be positive Real such that
A1: frequency = fr & Fifth(MS,frequency) = (3 qua Real) / 2 * fr
by Def12;
reconsider s = (3 qua Real) / 2 * fr as positive Real;
take fr,s;
thus thesis by A1;
end;
theorem Th55:
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
proof
let MS be satisfying_octave_descendent_constructible classical_octave
satisfying_octave_constructible classical_fifth
satisfying_fifth_constructible satisfying_harmonic_closed satisfying_Nat
satisfying_interval satisfying_equiv MusicStruct;
let fondamentale,frequency be Element of MS;
assume
A1: frequency is_Between fondamentale,Octave(MS,fondamentale);
ex r9 be positive Real st fondamentale = r9 &
Octave(MS,fondamentale) = 2 * r9 by Def15;
hence thesis by A1;
end;
theorem Th56:
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)
proof
let MS be 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;
let fondamentale,frequency be Element of MS;
assume frequency is_Between fondamentale,Octave(MS,fondamentale);
then consider r1,r2,r3 be positive Real such that
A1: fondamentale = r1 & frequency = r2 &
Octave(MS,fondamentale) = 2 * r1 &
r1 <= r2 <= 2 * r1 by Th55;
consider fr be positive Real such that
A2: frequency = fr & Fifth(MS,frequency) = (3 qua Real) / 2 * fr
by Def12;
per cases;
suppose Fifth(MS,frequency) is_Between
fondamentale,Octave(MS,fondamentale);
hence thesis by Def18;
end;
suppose
A3: not Fifth(MS,frequency) is_Between
fondamentale,Octave(MS,fondamentale);
A4: ex r being positive Real st Fifth(MS,frequency) = r &
Octave_descendent(MS,Fifth(MS,frequency)) = r / 2 by Th51;
per cases by A2,A1,A3;
suppose
A5: (3 qua Real) / 2 * r2 < r1;
reconsider r32 = (3 qua Real) / 2 as non zero positive Real;
r1 * (1 / r32) < 1 * r1 by XREAL_1:68;
then
A6: r1 / r32 < r1 by XCMPLX_1:99;
r32 * r2 / r32 < r1 / r32 by A5,XREAL_1:74;
then r2 < r1 / r32 by XCMPLX_1:89;
hence thesis by A1,A6,XXREAL_0:2;
end;
suppose 2 * r1 <= (3 qua Real) / 2 * r2;
then
A7: 2 * r1 / 2 <= (3 qua Real) / 2 * r2 / 2 by XREAL_1:72;
reconsider r34 = (3 qua Real) / 4 as positive Real;
A8: (3 qua Real) / 2 * r1 < 2 * r1 by XREAL_1:68;
((3 qua Real) / 4) * r2 <= ((3 qua Real) / 4) * (2 * r1)
by A1,XREAL_1:66;
then ((3 qua Real) / 4) * r2 < 2 * r1 by A8,XXREAL_0:2;
hence thesis by A2,A7,A1,A4,A3,Def18;
end;
end;
end;
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
REAL_Music is MusicSpace;
theorem
RAT_Music is MusicSpace;
begin :: Spiral of fifths
theorem Th56BIS:
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))))
proof
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;
defpred P[set,set,set] means
ex x,y be Element of MS st
x = $2 & y = $3 & y = Fifth_reduct(MS,fondamentale,x);
A1: for n be Nat for x being Element of MS ex y being Element of MS
st P[n,x,y]
proof
let n be Nat;
let x be Element of MS;
reconsider y = Fifth_reduct(MS,fondamentale,x) as Element of MS;
take y;
thus thesis;
end;
consider seq be sequence of MS such that
A2: seq.0 = frequency and
A3: for n be Nat holds P[n,seq.n,seq.(n+1)] from RECDEF_1:sch 2(A1);
reconsider seq as sequence of MS;
now
thus seq.0 = frequency by A2;
hereby
let n be Nat;
consider x,y be Element of MS such that
A4: x = seq.n and
A5: y = seq.(n+1) and
A6: y = Fifth_reduct(MS,fondamentale,x) by A3;
reconsider m = n+1 as non zero Nat;
reconsider m9 = m - 1 as Nat;
thus seq.(n+1)=Fifth_reduct(MS,fondamentale,seq.n) by A4,A5,A6;
end;
end;
hence thesis;
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 non empty MusicStruct;
let fondamentale,frequency be Element of MS;
func spiral_of_fifths(MS,fondamentale,frequency) -> sequence of MS means
:Def19:
it.0 = frequency &
for n being Nat holds it.(n+1) = Fifth_reduct (MS,fondamentale,it.n);
existence by Th56BIS;
uniqueness
proof
let seq1,seq2 be sequence of MS such that
A1: seq1.0 = frequency & for n be Nat holds seq1.(n+1)
= Fifth_reduct(MS,fondamentale,seq1.n) and
A2: seq2.0 = frequency & for n be Nat holds seq2.(n+1)
= Fifth_reduct(MS,fondamentale,seq2.n);
defpred P[Nat] means seq1.$1 = seq2.$1;
A3: P[0] by A1,A2;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: P[k];
seq1.(k+1) = Fifth_reduct(MS,fondamentale,seq1.k) by A1
.= seq2.(k+1) by A2,A5;
hence thesis;
end;
A6: for k be Nat holds P[k] from NAT_1:sch 2(A3,A4);
now
dom seq1 = NAT by PARTFUN1:def 2;
hence dom seq1 = dom seq2 by PARTFUN1:def 2;
thus for x be object st x in dom seq1 holds seq1.x = seq2.x by A6;
end;
hence thesis by FUNCT_1:def 11;
end;
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 Th57:
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)
proof
assume
A1: frequency is_Between fondamentale,Octave(MS,fondamentale);
let n be Nat;
defpred P[Nat] means
spiral_of_fifths(MS,fondamentale,frequency).$1
is_Between fondamentale,Octave(MS,fondamentale);
A2: P[0] by Def19,A1;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
spiral_of_fifths(MS,fondamentale,frequency).(k+1)
= Fifth_reduct(MS,fondamentale,
spiral_of_fifths(MS,fondamentale,frequency).k)
by Def19;
hence thesis by A4,Th56;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th58:
spiral_of_fifths(MS,fondamentale,fondamentale).1
= (3 qua Real) / 2 * @fondamentale
proof
reconsider n1 = 1,n0 = 0 as Nat;
A1: spiral_of_fifths(MS,fondamentale,fondamentale).1
= spiral_of_fifths(MS,fondamentale,fondamentale).(n0 + 1)
.= Fifth_reduct(MS,fondamentale,
spiral_of_fifths(MS,fondamentale,fondamentale).n0) by Def19
.= Fifth_reduct(MS,fondamentale,fondamentale) by Def19;
consider r,s be positive Real such that
A2: r = fondamentale & s = (3 qua Real) / 2 * r &
Fifth(MS,fondamentale) = s by Th54;
A3: ex fr be positive Real st fondamentale = fr &
Octave(MS,fondamentale) = 2 * fr by Def15;
1 * r <= ((3 qua Real) / 2) * r & ((3 qua Real) / 2) * r < 2 * r
by XREAL_1:68;
then Fifth(MS,fondamentale)
is_Between fondamentale,Octave(MS,fondamentale) by A2,A3;
hence thesis by A1,A2,Def18;
end;
theorem Th59:
spiral_of_fifths(MS,fondamentale,fondamentale).2
= (9 qua Real) / 8 * @fondamentale
proof
reconsider n2 = 2,n1 = 1,n0 = 0 as Nat;
spiral_of_fifths(MS,fondamentale,fondamentale).n1 is Element of MS;
then reconsider r32 = (3 qua Real) / 2 * @fondamentale as Element of MS
by Th58;
A1: spiral_of_fifths(MS,fondamentale,fondamentale).2
= spiral_of_fifths(MS,fondamentale,fondamentale).(n1 + 1)
.= Fifth_reduct(MS,fondamentale,
spiral_of_fifths(MS,fondamentale,fondamentale).n1) by Def19
.= Fifth_reduct(MS,fondamentale,r32) by Th58;
consider r,s be positive Real such that
A2: r = r32 & s = (3 qua Real) / 2 * r & Fifth(MS,r32) = s by Th54;
A3: Fifth(MS,r32) = (9 qua Real) / 4 * @fondamentale by A2;
A4: ex r being positive Real st Fifth(MS,r32) = r &
Octave_descendent(MS,Fifth(MS,r32)) = r / 2 by Th51;
not Fifth(MS,r32) is_Between fondamentale,Octave(MS,fondamentale)
proof
assume
A5: Fifth(MS,r32) is_Between fondamentale,Octave(MS,fondamentale);
A6: ex fr be positive Real st fondamentale = fr &
Octave(MS,fondamentale) = 2 * fr by Def15;
thus contradiction by A5,A6,A3,XREAL_1:68;
end;
hence thesis by A1,A2,A4,Def18;
end;
theorem Th60:
spiral_of_fifths(MS,fondamentale,fondamentale).3
= (27 qua Real) / 16 * @fondamentale
proof
reconsider n3=3,n2 = 2,n1 = 1,n0 = 0 as Nat;
spiral_of_fifths(MS,fondamentale,fondamentale).n2 is Element of MS;
then reconsider r32 = (9 qua Real) / 8 * @fondamentale as Element of MS
by Th59;
A1: spiral_of_fifths(MS,fondamentale,fondamentale).3
= spiral_of_fifths(MS,fondamentale,fondamentale).(n2 + 1)
.= Fifth_reduct(MS,fondamentale,
spiral_of_fifths(MS,fondamentale,fondamentale).n2) by Def19
.= Fifth_reduct(MS,fondamentale,r32) by Th59;
consider r,s be positive Real such that
A2: r = r32 & s = (3 qua Real) / 2 * r &
Fifth(MS,r32) = s by Th54;
A3: ex fr be positive Real st fondamentale = fr &
Octave(MS,fondamentale) = 2 * fr by Def15;
((27 qua Real) / 16) * @fondamentale < 2 * @fondamentale &
1 * @fondamentale < ((27 qua Real)/16) * @fondamentale
by XREAL_1:68;
then Fifth(MS,r32) is_Between fondamentale,Octave(MS,fondamentale)
by A2,A3;
hence thesis by A2,A1,Def18;
end;
theorem Th61:
spiral_of_fifths(MS,fondamentale,fondamentale).4
= (81 qua Real) / 64 * @fondamentale
proof
reconsider n4=4,n3=3,n2 = 2,n1 = 1,n0 = 0 as Nat;
spiral_of_fifths(MS,fondamentale,fondamentale).n3 is Element of MS;
then reconsider r32 = (27 qua Real) / 16 * @fondamentale as Element of MS
by Th60;
A1: spiral_of_fifths(MS,fondamentale,fondamentale).4
= spiral_of_fifths(MS,fondamentale,fondamentale).(n3 + 1)
.= Fifth_reduct(MS,fondamentale,
spiral_of_fifths(MS,fondamentale,fondamentale).n3) by Def19
.= Fifth_reduct(MS,fondamentale,r32) by Th60;
consider r,s be positive Real such that
A2: r = r32 & s = (3 qua Real) / 2 * r & Fifth(MS,r32) = s by Th54;
A3: Fifth(MS,r32) = (81 qua Real) / 32 * @fondamentale by A2;
A4: ex fr be positive Real st fondamentale = fr &
Octave(MS,fondamentale) = 2 * fr by Def15;
A5: ex r being positive Real st Fifth(MS,r32) = r &
Octave_descendent(MS,Fifth(MS,r32)) = r / 2 by Th51;
not Fifth(MS,r32) is_Between fondamentale,Octave(MS,fondamentale)
by A3,A4,XREAL_1:68;
hence thesis by A1,A2,A5,Def18;
end;
theorem
spiral_of_fifths(MS,fondamentale,fondamentale).5
= (243 qua Real) / 128 * @fondamentale
proof
reconsider n5=5,n4=4,n3=3,n2 = 2,n1 = 1,n0 = 0 as Nat;
spiral_of_fifths(MS,fondamentale,fondamentale).n4 is Element of MS;
then reconsider r32 = (81 qua Real) / 64 * @fondamentale as Element of MS
by Th61;
A1: spiral_of_fifths(MS,fondamentale,fondamentale).5
= spiral_of_fifths(MS,fondamentale,fondamentale).(n4 + 1)
.= Fifth_reduct(MS,fondamentale,
spiral_of_fifths(MS,fondamentale,fondamentale).n4) by Def19
.= Fifth_reduct(MS,fondamentale,r32) by Th61;
consider r,s be positive Real such that
A2: r = r32 & s = (3 qua Real) / 2 * r &
Fifth(MS,r32) = s by Th54;
A3: ex fr be positive Real st fondamentale = fr &
Octave(MS,fondamentale) = 2 * fr by Def15;
((243 qua Real) / 128) * @fondamentale < 2 * @fondamentale &
1 * @fondamentale < ((243 qua Real) / 128) * @fondamentale
by XREAL_1:68;
then Fifth(MS,r32) is_Between fondamentale,Octave(MS,fondamentale)
by A2,A3;
hence thesis by A2,A1,Def18;
end;
theorem Th62:
@(spiral_of_fifths(MS,frequency,frequency).2) /
@frequency = (3 * 3 qua Real) / (2 * 2 * 2)
proof
@(spiral_of_fifths(MS,frequency,frequency).2) /
@frequency = ((9 qua Real) / 8 * @frequency) / @frequency by Th59
.= (3 * 3 qua Real) / (2 * 2 * 2) by XCMPLX_1:89;
hence thesis;
end;
theorem Th63:
@(spiral_of_fifths(MS,frequency,frequency).4) /
@(spiral_of_fifths(MS,frequency,frequency).2)
= (3 * 3 qua Real) / (2 * 2 * 2)
proof
spiral_of_fifths(MS,frequency,frequency).4
= (81 qua Real) / 64 * @frequency &
spiral_of_fifths(MS,frequency,frequency).2
= (9 qua Real) / 8 * @frequency by Th59,Th61;
then @(spiral_of_fifths(MS,frequency,frequency).4) /
@(spiral_of_fifths(MS,frequency,frequency).2)
= ((81 qua Real) / 64)/((9 qua Real) / 8) by XCMPLX_1:91;
hence thesis;
end;
theorem Th64:
@(spiral_of_fifths(MS,frequency,frequency).1) /
@(spiral_of_fifths(MS,frequency,frequency).4)
= ((32 qua Real) / 27)
proof
spiral_of_fifths(MS,frequency,frequency).4
= (81 qua Real) / 64 * @frequency &
spiral_of_fifths(MS,frequency,frequency).1
= (3 qua Real) / 2 * @frequency
by Th58,Th61;
then @(spiral_of_fifths(MS,frequency,frequency).1) /
@(spiral_of_fifths(MS,frequency,frequency).4)
= ((3 qua Real) / 2)/((81 qua Real) / 64) by XCMPLX_1:91
.= ((32 qua Real) / 27);
hence thesis;
end;
theorem Th65:
@(spiral_of_fifths(MS,frequency,frequency).3) /
@(spiral_of_fifths(MS,frequency,frequency).1)
= ((9 qua Real) / 8)
proof
spiral_of_fifths(MS,frequency,frequency).3
= (27 qua Real) / 16 * @frequency &
spiral_of_fifths(MS,frequency,frequency).1 = (3 qua Real) / 2 * @frequency
by Th58,Th60;
then @(spiral_of_fifths(MS,frequency,frequency).3) /
@(spiral_of_fifths(MS,frequency,frequency).1)
= ((27 qua Real) / 16)/((3 qua Real) / 2) by XCMPLX_1:91
.= ((9 qua Real) / 8);
hence thesis;
end;
theorem Th66:
@Octave(MS,frequency) /
@(spiral_of_fifths(MS,frequency,frequency).3)
= ((32 qua Real) / 27)
proof
now
thus spiral_of_fifths(MS,frequency,frequency).3
= (27 qua Real) / 16 * @frequency by Th60;
ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
hence @Octave(MS,frequency) = 2 * @frequency;
end;
then @Octave(MS,frequency) /
@(spiral_of_fifths(MS,frequency,frequency).3)
= ((4 qua Real) / 2)/((27 qua Real) / 16) by XCMPLX_1:91
.= ((32 qua Real) / 27);
hence thesis;
end;
definition
let MS be MusicSpace;
let scale be Element of 2-tuples_on the carrier of MS;
attr scale is monotonic means
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
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
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
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
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
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
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
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 :Def20:
it.1 = frequency &
it.2 = spiral_of_fifths(MS,frequency,frequency).2 &
it.3 = spiral_of_fifths(MS,frequency,frequency).4 &
it.4 = spiral_of_fifths(MS,frequency,frequency).1 &
it.5 = spiral_of_fifths(MS,frequency,frequency).3 &
it.6 = Octave(MS,frequency);
existence
proof
defpred P[set,set] means
($1 = 1 implies $2 = frequency) &
($1 = 2 implies $2 = spiral_of_fifths(MS,frequency,frequency).2) &
($1 = 3 implies $2 = spiral_of_fifths(MS,frequency,frequency).4) &
($1 = 4 implies $2 = spiral_of_fifths(MS,frequency,frequency).1) &
($1 = 5 implies $2 = spiral_of_fifths(MS,frequency,frequency).3) &
($1 = 6 implies $2 = Octave(MS,frequency));
A1: for k be Nat st k in Seg 6 holds ex x be Element of MS st P[k,x]
proof
let k be Nat;
assume k in Seg 6;
then 1 <= k <= 6 by FINSEQ_1:1;
then k = 1 or ... or k = 6;
hence thesis;
end;
consider p be FinSequence of the carrier of MS such that
A2: dom p = Seg 6 and
A3: for k be Nat st k in Seg 6 holds P[k,p.k] from FINSEQ_1:sch 5(A1);
len p = 6 by A2,FINSEQ_1:def 3;
then reconsider p as Element of 6-tuples_on the carrier of MS
by FINSEQ_2:92;
take p;
1 in Seg 6 & 2 in Seg 6 & 3 in Seg 6 & 4 in Seg 6 &
5 in Seg 6 & 6 in Seg 6 by FINSEQ_1:1;
hence thesis by A3;
end;
uniqueness
proof
let p1,p2 be Element of 6-tuples_on the carrier of MS such that
A4: p1.1 = frequency & p1.2 = spiral_of_fifths(MS,frequency,frequency).2 &
p1.3 = spiral_of_fifths(MS,frequency,frequency).4 &
p1.4 = spiral_of_fifths(MS,frequency,frequency).1 &
p1.5 = spiral_of_fifths(MS,frequency,frequency).3 &
p1.6 = Octave(MS,frequency) and
A5: p2.1 = frequency & p2.2 = spiral_of_fifths(MS,frequency,frequency).2 &
p2.3 = spiral_of_fifths(MS,frequency,frequency).4 &
p2.4 = spiral_of_fifths(MS,frequency,frequency).1 &
p2.5 = spiral_of_fifths(MS,frequency,frequency).3 &
p2.6 = Octave(MS,frequency);
now
len p1 = 6 & len p2 = 6 by FINSEQ_2:132;
then dom p1 = Seg 6 & dom p2 = Seg 6 by FINSEQ_1:def 3;
hence dom p1 = dom p2;
hereby
let i be object;
assume
A6: i in dom p1;
then reconsider j = i as Nat;
j in Seg len p1 by A6,FINSEQ_1:def 3;
then j in Seg 6 by FINSEQ_2:132;
then 1 <= j <= 6 by FINSEQ_1:1;
then j = 1 or ... or j = 6;
hence p1.i = p2.i by A4,A5;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
end;
reserve MS for MusicSpace,
fondamentale, frequency, f1, f2 for Element of MS;
theorem Th67:
pentatonic_pythagorean_scale(MS,frequency) is pentatonic
proof
set scale = pentatonic_pythagorean_scale(MS,frequency);
A1: scale.1 = frequency &
scale.2 = spiral_of_fifths(MS,frequency,frequency).2 &
scale.3 = spiral_of_fifths(MS,frequency,frequency).4 &
scale.4 = spiral_of_fifths(MS,frequency,frequency).1 &
scale.5 = spiral_of_fifths(MS,frequency,frequency).3 &
scale.6 = Octave(MS,frequency) by Def20;
scale in 6-tuples_on the carrier of MS;
then scale in {s where s is Element of (the carrier of MS)*: len s = 6}
by FINSEQ_2:def 4;
then consider s be Element of (the carrier of MS)* such that
A2: s = scale and
A3: len s = 6;
dom s = Seg 6 by A3,FINSEQ_1:def 3;
then reconsider g1 = scale.1, g2 = scale.2, g3 = scale.3,
g4 = scale.4,g5 = scale.5, g6 = scale.6
as Element of the carrier of MS by A2,FINSEQ_1:1,FINSEQ_2:11;
now
reconsider frequency = g1 as Element of MS;
take frequency;
reconsider r1 = @frequency, r2 = @g2, r3 = @g3,
r4 = @g4, r5 = @g5, r6 = @g6 as positive Real;
take r1,r2,r3,r4,r5,r6;
thus scale.1 = frequency & scale.1 = r1 &
scale.2 = r2 & scale.3 = r3 & scale.4 = r4 & scale.5 = r5 &
scale.6 = r6;
now
thus r1 = 1 * @frequency;
thus r2 = (9 qua Real) / 8 * @frequency by Th59,A1;
thus r3 = (81 qua Real) / 64 * @frequency by A1,Th61;
thus r4 = (3 qua Real) / 2 * @frequency by A1,Th58;
thus r5 = (27 qua Real) / 16 * @frequency by A1,Th60;
ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
hence r6 = 2 * @frequency by A1;
end;
hence r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 by XREAL_1:68;
thus scale.6 = Octave(MS,frequency) by A1;
end;
hence thesis;
end;
definition
let MS be MusicSpace;
let f1,f2 be Element of MS;
func intrval(f1,f2) -> positive Real means :Def21:
ex r1,r2 being positive Real
st r1 = f1 & r2 = f2 & it = r2 / r1;
existence
proof
reconsider r = (@f2) / (@f1) as positive Real;
take r;
thus thesis;
end;
uniqueness;
end;
definition
func pythagorean_tone -> positive Real equals (9 qua Real) / 8;
coherence;
end;
definition
func pentatonic_pythagorean_semiditone -> positive Real equals
(32 qua Real) / 27;
coherence;
end;
definition
func major_third_pythagorean_tone -> positive Real equals
pythagorean_tone * pythagorean_tone;
coherence;
end;
definition
func pure_major_third -> positive Real equals (5 qua Real) / 4;
coherence;
end;
definition
func syntonic_comma -> positive Real equals
major_third_pythagorean_tone / pure_major_third;
coherence;
end;
theorem
syntonic_comma = (81 qua Real) / 80;
theorem
pythagorean_tone < pentatonic_pythagorean_semiditone;
theorem
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
pentatonic_pythagorean_scale(MS,frequency).1;
coherence by Def20;
func penta_1(MS,frequency) -> Element of MS equals
pentatonic_pythagorean_scale(MS,frequency).2;
coherence
proof
pentatonic_pythagorean_scale(MS,frequency).2
= spiral_of_fifths(MS,frequency,frequency).2 by Def20;
hence thesis;
end;
func penta_2(MS,frequency) -> Element of MS equals
pentatonic_pythagorean_scale(MS,frequency).3;
coherence
proof
pentatonic_pythagorean_scale(MS,frequency).3
= spiral_of_fifths(MS,frequency,frequency).4
by Def20;
hence thesis;
end;
func penta_3(MS,frequency) -> Element of MS equals
pentatonic_pythagorean_scale(MS,frequency).4;
coherence
proof
pentatonic_pythagorean_scale(MS,frequency).4
= spiral_of_fifths(MS,frequency,frequency).1
by Def20;
hence thesis;
end;
func penta_4(MS,frequency) -> Element of MS equals
pentatonic_pythagorean_scale(MS,frequency).5;
coherence
proof
pentatonic_pythagorean_scale(MS,frequency).5
= spiral_of_fifths(MS,frequency,frequency).3
by Def20;
hence thesis;
end;
func penta_octave(MS,frequency) -> Element of MS equals
Octave(MS,frequency);
coherence;
end;
theorem
ex r1,r2 being Element of REALPLUS st
intrval(f1,f2) = REAL_ratio(r1,r2)
proof
the carrier of MS c= REALPLUS by Def07a;
then reconsider r1 = f1,r2 = f2 as Element of REALPLUS;
consider r,s be positive Real such that
A1: r1 = r & r2 = s & REAL_ratio(r1,r2) = s / r by Def01;
intrval(f1,f2) = s / r & REAL_ratio(r1,r2) = s / r by A1,Def21;
hence thesis;
end;
theorem Th68:
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
proof
let r1,r2,r3,r4,r5,r6 be positive Real;
assume
A1: 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;
set gamme = pentatonic_pythagorean_scale(MS,frequency);
A2: gamme.1 = frequency &
gamme.2 = spiral_of_fifths(MS,frequency,frequency).2 &
gamme.3 = spiral_of_fifths(MS,frequency,frequency).4 &
gamme.4 = spiral_of_fifths(MS,frequency,frequency).1 &
gamme.5 = spiral_of_fifths(MS,frequency,frequency).3 &
gamme.6 = Octave(MS,frequency) by Def20;
gamme is pentatonic by Th67;
then consider frequency be Element of MS,
r1,r2,r3,r4,r5,r6 be positive Real such that
A3: gamme.1 = frequency & gamme.1 = r1 &
gamme.2 = r2 & gamme.3 = r3 & gamme.4 = r4 & gamme.5 = r5 & gamme.6 = r6 &
r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 & gamme.6 = Octave(MS,frequency);
@(spiral_of_fifths(MS,frequency,frequency).2) /
@frequency = (3 * 3 qua Real) / (2 * 2 * 2) &
@(spiral_of_fifths(MS,frequency,frequency).4) /
@(spiral_of_fifths(MS,frequency,frequency).2)
= (3 * 3 qua Real) / (2 * 2 * 2) &
@(spiral_of_fifths(MS,frequency,frequency).1) /
@(spiral_of_fifths(MS,frequency,frequency).4) = ((32 qua Real) / 27) &
@(spiral_of_fifths(MS,frequency,frequency).3) /
@(spiral_of_fifths(MS,frequency,frequency).1) = ((9 qua Real) / 8) &
@Octave(MS,frequency) /
@(spiral_of_fifths(MS,frequency,frequency).3)
= ((32 qua Real) / 27) by Th62,Th63,Th64,Th65,Th66;
hence thesis by A1,A2,A3;
end;
theorem Th69:
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
proof
set r1 = penta_fondamentale(MS,frequency),
r2 = penta_1(MS,frequency), r3 = penta_2(MS,frequency),
r4 = penta_3(MS,frequency), r5 = penta_4(MS,frequency),
r6 = penta_octave(MS,frequency);
the carrier of MS c= REALPLUS by Def07a;
then reconsider r91 = r1,r92 = r2,r93 = r3,
r94 = r4,r95 = r5,r96 = r6 as positive Real by Th1;
A1: pentatonic_pythagorean_scale(MS,frequency).1 = r91 &
pentatonic_pythagorean_scale(MS,frequency).2 = r92 &
pentatonic_pythagorean_scale(MS,frequency).3 = r93 &
pentatonic_pythagorean_scale(MS,frequency).4 = r94 &
pentatonic_pythagorean_scale(MS,frequency).5 = r95 &
pentatonic_pythagorean_scale(MS,frequency).6 = r96 by Def20;
then r92 / r91 = (9 qua Real) / 8 &
r93 / r92 = (9 qua Real) / 8 &
r94 / r93 = (32 qua Real) / 27 &
r95 / r94 = (9 qua Real) / 8 &
r96 / r95 = (32 qua Real) / 27 by Th68;
hence thesis by A1;
end;
theorem
(9 qua Real) / 8 = (9 qua Rational) / 8;
theorem
intrval(penta_fondamentale(MS,frequency),penta_1(MS,frequency))
= pythagorean_tone &
intrval(penta_1(MS,frequency),penta_2(MS,frequency))
= pythagorean_tone &
intrval(penta_2(MS,frequency),penta_3(MS,frequency))
= pentatonic_pythagorean_semiditone &
intrval(penta_3(MS,frequency),penta_4(MS,frequency))
= pythagorean_tone &
intrval(penta_4(MS,frequency),penta_octave(MS,frequency))
= pentatonic_pythagorean_semiditone
proof
consider r1,r2 be positive Real
such that
A1: r1 = penta_fondamentale(MS,frequency) & r2 = penta_1(MS,frequency) &
intrval(penta_fondamentale(MS,frequency),penta_1(MS,frequency))= r2 / r1
by Def21;
consider r3,r4 be positive Real
such that
A2: r3 = penta_1(MS,frequency) & r4 = penta_2(MS,frequency) &
intrval(penta_1(MS,frequency),penta_2(MS,frequency))= r4 / r3
by Def21;
consider r5,r6 be positive Real such that
A3: r5 = penta_2(MS,frequency) & r6 = penta_3(MS,frequency) &
intrval(penta_2(MS,frequency),penta_3(MS,frequency))= r6 / r5
by Def21;
consider r7,r8 be positive Real such that
A4: r7 = penta_3(MS,frequency) & r8 = penta_4(MS,frequency) &
intrval(penta_3(MS,frequency),penta_4(MS,frequency))= r8 / r7
by Def21;
consider r9,r10 be positive Real such that
A5: r9 = penta_4(MS,frequency) & r10 = penta_octave(MS,frequency) &
intrval(penta_4(MS,frequency),penta_octave(MS,frequency))= r10 / r9
by Def21;
ex s1,s2,s3,s4,s5,s6 be positive Real st
pentatonic_pythagorean_scale(MS,frequency).1 = s1 &
pentatonic_pythagorean_scale(MS,frequency).2 = s2 &
pentatonic_pythagorean_scale(MS,frequency).3 = s3 &
pentatonic_pythagorean_scale(MS,frequency).4 = s4 &
pentatonic_pythagorean_scale(MS,frequency).5 = s5 &
pentatonic_pythagorean_scale(MS,frequency).6 = s6 &
s2 / s1 = (9 qua Real) / 8 & s3 / s2 = (9 qua Real) / 8 &
s4 / s3 = (32 qua Real) / 27 & s5 / s4 = (9 qua Real) / 8 &
s6 / s5 = (32 qua Real) / 27 by Th69;
hence 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
by A1,A2,A3,A4,A5,Def20;
end;
theorem
Fifth(MS,frequency) is_Between frequency,Octave(MS,frequency)
proof
consider fr be positive Real such that
A1: frequency = fr & Fifth(MS,frequency) = (3 qua Real) / 2 * fr by Def12;
A2: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
reconsider x = (3 qua Real) / 2 * fr as positive Real;
1 * fr <= x < 2 * fr by XREAL_1:68;
hence thesis by A2,A1;
end;
theorem Th70:
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)
proof
let r1,r2 be positive Real;
assume that
A1: f1 = r1 and
A2: f2 = r2 and
A3: r2 = (4 qua Real) / 3 * r1;
A4: ex fr be positive Real st f2 = fr &
Fifth(MS,f2) = (3 qua Real) / 2 * fr by Def12;
hence Fifth(MS,f2) = 2 * r1 by A2,A3;
ex fr be positive Real st f1 = fr & Octave(MS,f1) = 2 * fr by Def15;
hence not Fifth(MS,f2) is_Between f1,Octave(MS,f1) by A4,A3,A2,A1;
end;
theorem Th71:
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)
proof
let r1,r2 be positive Real;
assume that
A1: f1 = r1 & f2 = r2 and
A2: r2 = (4 qua Real) / 3 * r1;
thus Fifth(MS,f2) is_Between fondamentale,Octave(MS,fondamentale) implies
Octave_descendent(MS,Fifth_reduct(MS,fondamentale,f2)) = f1
proof
assume
A3: Fifth(MS,f2) is_Between fondamentale,Octave(MS,fondamentale);
A4: ex fr be positive Real st f2 = fr &
Fifth(MS,f2) = (3 qua Real) / 2 * fr by Def12;
ex r being positive Real st Fifth_reduct(MS,fondamentale,f2) = r &
Octave_descendent(MS,Fifth_reduct(MS,fondamentale,f2)) = r / 2
by Th51;
then Octave_descendent(MS,Fifth_reduct(MS,fondamentale,f2))
= ((2 qua Real) * r1) / 2 by A3,A4,Def18,A1,A2
.= f1 by A1;
hence thesis;
end;
thus not Fifth(MS,f2) is_Between fondamentale,Octave(MS,fondamentale)
implies Fifth_reduct(MS,fondamentale,f2) = f1
proof
assume
A5: not Fifth(MS,f2) is_Between fondamentale,Octave(MS,fondamentale);
consider fr be positive Real such that
A6: f2 = fr & Fifth(MS,f2) = (3 qua Real) / 2 * fr by Def12;
ex r being positive Real st Fifth(MS,f2) = r &
Octave_descendent(MS,Fifth(MS,f2)) = r / 2 by Th51;
hence thesis by A1,A2,A6,A5,Def18;
end;
end;
theorem
for r1,r2 being positive Real st f1 = r1 & f2 = r2 &
r2 = (4 qua Real) / 3 * r1 holds
Fifth_reduct(MS,f1,f2) = f1
proof
let r1,r2 be positive Real;
assume
A1: f1 = r1 & f2 = r2 & r2 = (4 qua Real) / 3 * r1;
then (Fifth(MS,f2) is_Between f1,Octave(MS,f1) implies
Octave_descendent(MS,Fifth_reduct(MS,f1,f2)) = f1) &
(not Fifth(MS,f2) is_Between f1,Octave(MS,f1) implies
Fifth_reduct(MS,f1,f2) = f1) by Th71;
hence thesis by A1,Th70;
end;
begin :: Heptatonic pythagorean scale
definition
let S be MusicSpace;
attr S is satisfying_fourth_constructible means :Def22:
for frequency being Element of S holds ex q being Element of S st
[frequency,q] in fourth(S);
end;
theorem Th78:
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)
proof
let MS be MusicSpace;
assume
A1: MS = REAL_Music;
now
let frequency be Element of MS;
reconsider f = frequency as positive Real by A1,Th1;
reconsider qr = (4 qua Real) / 3 * f as positive Real;
reconsider q = qr as Element of MS by A1,Th1;
take f,qr;
thus f = frequency;
thus qr = (4 qua Real) / 3 * f;
reconsider n2 = 3,n3 = 4 as Element of MS by Th20;
reconsider x = [n2,n3],y = [frequency,q] as
Element of [:REALPLUS,REALPLUS:] by A1;
reconsider z = [frequency,q] as Element of [:REALPLUS,REALPLUS:]
by A1;
consider x9,y9 be Element of REALPLUS such that
A2: z = [x9,y9] and
A3: REAL_ratio.z = REAL_ratio(x9,y9) by Def02;
consider r,s be positive Real such that
A4: x9 = r & s = y9 & REAL_ratio(x9,y9) = s / r by Def01;
consider x99,y99 be Element of REALPLUS such that
A5: x = [x99,y99] and
A6: REAL_ratio.x = REAL_ratio(x99,y99) by Def02;
consider r9,s9 be positive Real such that
A7: x99 = r9 & s9 = y99 & REAL_ratio(x99,y99) = s9 / r9 by Def01;
A8: n2 = r9 & n3 = s9 & r = frequency & s = q
by A4,A2,A5,A7,XTUPLE_0:1;
now
thus REAL_ratio.(n2,n3) = (4 qua Real) / (3 qua Real)
by A7,A8,A6,BINOP_1:def 1;
thus REAL_ratio.(frequency,q) = s / r by A3,A4,BINOP_1:def 1
.= (4 qua Real) / 3 by A8,XCMPLX_1:89;
end;
then n2,n3 equiv frequency,q by A1,Def08a;
hence [f,qr] in fourth(MS) by EQREL_1:18;
end;
hence thesis;
end;
theorem Th79:
REAL_Music is satisfying_fourth_constructible
proof
set MS = REAL_Music;
let frequency be Element of MS;
consider fr,qr be positive Real such that
A1: fr = frequency and
qr = (4 qua Real) / 3 * fr and
A2: [fr,qr] in fourth(MS) by Th78;
fr is Element of MS & qr is Element of MS by Th1;
hence thesis by A1,A2;
end;
registration
cluster satisfying_fourth_constructible for MusicSpace;
existence by Th79;
end;
definition
let MS be satisfying_fourth_constructible MusicSpace;
let frequency be Element of MS;
func Fourth(MS,frequency) -> Element of MS means :Def23:
[frequency,it] in fourth(MS);
existence by Def22;
uniqueness
proof
let q1,q2 be Element of MS such that
A1: [frequency,q1] in fourth(MS) and
A2: [frequency,q2] in fourth(MS);
reconsider n2 = 3,n3 = 4 as Element of MS by Th20;
A3: n2,n3 equiv frequency,q1 by A1,EQREL_1:18;
n2,n3 equiv frequency,q2 by A2,EQREL_1:18;
then frequency,q2 equiv n2,n3 by Th22;
hence thesis by Th24,A3,Th23;
end;
end;
definition
let MS be satisfying_fourth_constructible MusicSpace;
attr MS is classical_fourth means :Def24:
for frequency being Element of MS
ex fr being positive Real st frequency = fr &
Fourth(MS,frequency) = (4 qua Real) / 3 * fr;
end;
theorem Th80:
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
proof
let MS be satisfying_fourth_constructible MusicSpace;
assume
A1: MS = REAL_Music;
let frequency be Element of MS;
reconsider fr = frequency as positive Real by A1,Th1;
take fr;
thus frequency = fr;
consider fr9,qr9 be positive Real such that
A2: fr9 = frequency and
A3: qr9 = (4 qua Real) / 3 * fr9 and
A4: [fr9,qr9] in fourth(MS) by A1,Th78;
reconsider qr9 as Element of MS by A1,Th1;
qr9 = Fourth(MS,frequency) by A2,A4,Def23;
hence thesis by A2,A3;
end;
registration
cluster classical_fourth for satisfying_fourth_constructible MusicSpace;
existence
proof
reconsider MS = REAL_Music as
satisfying_fourth_constructible MusicSpace by Th79;
take MS;
thus thesis by Th80;
end;
end;
definition
let MS be satisfying_Real non empty MusicStruct;
attr MS is satisfying_euclidean means :Def25:
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;
existence
proof
reconsider MS = REAL_Music as MusicSpace;
now
let f1,f2 be Element of REAL_Music;
reconsider x = [f1,f2] as Element of [:REALPLUS,REALPLUS:];
consider y9,z9 be Element of REALPLUS such that
A1: x = [y9,z9] and
A2: REAL_ratio.x = REAL_ratio(y9,z9) by Def02;
consider y99,z99 be Element of REALPLUS such that
A3: x = [y99,z99] and
REAL_ratio.x = REAL_ratio(y99,z99) by Def02;
consider r,s be positive Real such that
A4: y99 = r & s = z99 & REAL_ratio(y99,z99) = s / r by Def01;
A5: s = @f2 & r = @f1 by A4,A3,XTUPLE_0:1;
A6: y99 = y9 & z99 = z9 by A1,A3,XTUPLE_0:1;
thus (the Ratio of REAL_Music).(f1,f2)
= @f2 / @f1 by A2,BINOP_1:def 1,A5,A6,A4;
end;
then MS is satisfying_euclidean;
hence thesis;
end;
end;
registration
cluster satisfying_euclidean -> satisfying_interval for
satisfying_Real non empty MusicStruct;
coherence
proof
let S be satisfying_Real non empty MusicStruct;
assume
A1: S is satisfying_euclidean;
now
let f1,f2,f3 be Element of S;
assume (the Ratio of S).(f1,f2) = (the Ratio of S).(f1,f3);
then @f2 / @f1 = (the Ratio of S).(f1,f3) by A1;
then @f2 / @f1 = @f3 / @f1 by A1;
hence f2 = f3 by XCMPLX_1:53;
end;
hence thesis;
end;
end;
registration
cluster satisfying_euclidean -> satisfying_tonic for satisfying_Real
non empty MusicStruct;
coherence
proof
let S be satisfying_Real non empty MusicStruct;
assume
A1: S is satisfying_euclidean;
now
let f1,f2,f3 be Element of S;
assume (the Ratio of S).(f1,f1) = (the Ratio of S).(f2,f3);
then @f1 / @f1 = (the Ratio of S).(f2,f3) by A1;
then @f1 / @f1 = @f3 / @f2 by A1;
hence f2 = f3 by XCMPLX_1:58,60;
end;
hence thesis;
end;
end;
registration
cluster satisfying_euclidean -> satisfying_commutativity for
satisfying_Real non empty MusicStruct;
coherence
proof
let S be satisfying_Real non empty MusicStruct;
assume
A1: S is satisfying_euclidean;
now
let f1,f2,f3,f4 be Element of S;
assume (the Ratio of S).(f2,f1) = (the Ratio of S).(f4,f3);
then
A2: @f1 / @f2 = (the Ratio of S).(f4,f3) by A1
.= @f3 / @f4 by A1;
thus (the Ratio of S).(f1,f2) = @f2 / @f1 by A1
.= 1 / (@f1 / @f2) by XCMPLX_1:57
.= @f4 / @f3 by A2,XCMPLX_1:57
.= (the Ratio of S).(f3,f4) by A1;
end;
hence thesis;
end;
end;
registration
cluster satisfying_euclidean for classical_fourth
satisfying_fourth_constructible MusicSpace;
existence
proof
reconsider MS = REAL_Music as
satisfying_fourth_constructible MusicSpace by Th79;
A1: MS is classical_fourth by Th80;
now
let f1,f2 be Element of REAL_Music;
reconsider x = [f1,f2] as Element of [:REALPLUS,REALPLUS:];
consider y9,z9 be Element of REALPLUS such that
A2: x = [y9,z9] and
A3: REAL_ratio.x = REAL_ratio(y9,z9) by Def02;
consider y99,z99 be Element of REALPLUS such that
A4: x = [y99,z99] and
REAL_ratio.x = REAL_ratio(y99,z99) by Def02;
consider r,s be positive Real such that
A5: y99 = r & s = z99 & REAL_ratio(y99,z99) = s / r by Def01;
A6: s = @f2 & r = @f1 by A5,A4,XTUPLE_0:1;
A7: y99 = y9 & z99 = z9 by A2,A4,XTUPLE_0:1;
thus (the Ratio of REAL_Music).(f1,f2) = @f2 / @f1
by A7,A5,A3,BINOP_1:def 1,A6;
end;
then MS is satisfying_euclidean;
hence thesis by A1;
end;
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 :Def26:
it.1 = spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).1 &
it.2 = spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).3 &
it.3 = spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).5 &
it.4 = Fourth(HPS,frequency) &
it.5 = spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).2 &
it.6 = spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).4 &
it.7 = spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).6 &
it.8 = Octave(HPS,spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).1);
existence
proof
set MS = HPS;
defpred P[set,set] means
($1 = 1 implies
$2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1) &
($1 = 2 implies
$2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).3) &
($1 = 3 implies
$2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).5) &
($1 = 4 implies $2 = Fourth(MS,frequency)) &
($1 = 5 implies
$2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).2) &
($1 = 6 implies
$2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).4) &
($1 = 7 implies
$2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).6) &
($1 = 8 implies
$2 = Octave(MS,spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1));
A1: for k be Nat st k in Seg 8 holds ex x be Element of MS st P[k,x]
proof
let k be Nat;
assume k in Seg 8;
then 1 <= k <= 8 by FINSEQ_1:1;
then k = 1 or ... or k = 8;
hence thesis;
end;
consider p be FinSequence of the carrier of MS such that
A2: dom p = Seg 8 and
A3: for k be Nat st k in Seg 8 holds P[k,p.k] from FINSEQ_1:sch 5(A1);
len p = 8 by A2,FINSEQ_1:def 3;
then reconsider p as Element of 8-tuples_on the carrier of MS
by FINSEQ_2:92;
take p;
1 in Seg 8 & 2 in Seg 8 & 3 in Seg 8 & 4 in Seg 8 &
5 in Seg 8 & 6 in Seg 8 & 7 in Seg 8 & 8 in Seg 8 by FINSEQ_1:1;
hence thesis by A3;
end;
uniqueness
proof
set MS = HPS;
let p1,p2 be Element of 8-tuples_on the carrier of MS such that
A4: p1.1 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1 &
p1.2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).3 &
p1.3 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).5 &
p1.4 = Fourth(MS,frequency) &
p1.5 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).2 &
p1.6 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).4 &
p1.7 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).6 &
p1.8 = Octave(MS,spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1)
and
A5: p2.1 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1 &
p2.2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).3 &
p2.3 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).5 &
p2.4 = Fourth(MS,frequency) &
p2.5 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).2 &
p2.6 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).4 &
p2.7 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).6 &
p2.8 = Octave(MS,spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1);
now
len p1 = 8 & len p2 = 8 by FINSEQ_2:132;
then dom p1 = Seg 8 & dom p2 = Seg 8 by FINSEQ_1:def 3;
hence dom p1 = dom p2;
hereby
let i be object;
assume
A6: i in dom p1;
then reconsider j = i as Nat;
j in Seg len p1 by A6,FINSEQ_1:def 3;
then j in Seg 8 by FINSEQ_2:132;
then 1 <= j <= 8 by FINSEQ_1:1;
then j = 1 or ... or j = 8;
hence p1.i = p2.i by A4,A5;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
end;
theorem Th81:
Fourth(HPS,frequency) is_Between frequency,Octave(HPS,frequency)
proof
set MS = HPS;
consider fr be positive Real such that
A1: frequency = fr and
A2: Fourth(MS,frequency) = (4 qua Real) / 3 * fr by Def24;
consider fr2 be positive Real such that
A3: frequency = fr2 and
A4: Octave(MS,frequency) = 2 * fr2 by Def15;
1 * fr <= (4 qua Real) / 3 * fr < 2 * fr by XREAL_1:68;
hence thesis by A3,A4,A1,A2;
end;
theorem
for n being Nat holds
spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).n
is_Between frequency,Octave(HPS,frequency) by Th57,Th81;
theorem Th82:
spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).1
= frequency
proof
set MS = HPS;
set q = Fourth(MS,frequency),
f1 = spiral_of_fifths(MS,frequency,q).1;
consider frq be positive Real such that
A1: frequency = frq & Fourth(MS,frequency) = (4 qua Real) / 3 * frq
by Def24;
reconsider n1 = 1, n0 = 0 as Nat;
A2: spiral_of_fifths(MS,frequency,q).1
= spiral_of_fifths(MS,frequency,q).(n0 + 1)
.= Fifth_reduct(MS,frequency,
spiral_of_fifths(MS,frequency,q).n0) by Def19
.= Fifth_reduct(MS,frequency,q) by Def19;
consider r,s be positive Real such that
A3: r = q & s = (3 qua Real) / 2 * r &
Fifth(MS,q) = s by Th54;
consider fr2 be positive Real such that
A4: frequency = fr2 and
A5: Octave(MS,frequency) = 2 * fr2 by Def15;
consider ro be positive Real such that
A6: Fifth(MS,q) = ro and
A7: Octave_descendent(MS,Fifth(MS,q)) = ro / 2 by Th51;
not Fifth(MS,q) is_Between frequency,Octave(MS,frequency)
by A3,A1,A4,A5;
hence thesis by A2,A6,A7,A3,A1,Def18;
end;
theorem Th83:
spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).2
= (3 qua Real) / 2 * @frequency
proof
set MS = HPS;
set q = Fourth(MS,frequency);
reconsider n1 = 1 as Nat;
A1: spiral_of_fifths(MS,frequency,q).2
= spiral_of_fifths(MS,frequency,q).(n1 + 1)
.= Fifth_reduct(MS,frequency,
spiral_of_fifths(MS,frequency,q).n1) by Def19
.= Fifth_reduct(MS,frequency,frequency) by Th82;
consider r,s be positive Real such that
A2: r = frequency & s = (3 qua Real) / 2 * r &
Fifth(MS,frequency) = s by Th54;
A3: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
1 * r <= ((3 qua Real) / 2) * r & ((3 qua Real) / 2) * r < 2 * r
by XREAL_1:68;
then Fifth(MS,frequency) is_Between frequency,Octave(MS,frequency)
by A2,A3;
hence thesis by A1,A2,Def18;
end;
theorem Th84:
spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).3
= (9 qua Real) / 8 * @(frequency)
proof
set MS = HPS;
set q = Fourth(MS,frequency);
reconsider n1 = 2 as Nat;
spiral_of_fifths(MS,frequency,q).n1 is Element of MS;
then reconsider r32 = (3 qua Real) / 2 * @frequency as Element of MS
by Th83;
A1: spiral_of_fifths(MS,frequency,q).3
= spiral_of_fifths(MS,frequency,q).(n1 + 1)
.= Fifth_reduct(MS,frequency,
spiral_of_fifths(MS,frequency,q).n1) by Def19
.= Fifth_reduct(MS,frequency,r32) by Th83;
consider r,s be positive Real such that
A2: r = r32 & s = (3 qua Real) / 2 * r &
Fifth(MS,r32) = s by Th54;
A3: 2 * @frequency < ((9 qua Real) / 4) * @frequency
by XREAL_1:68;
A4: ex r being positive Real st Fifth(MS,r32) = r &
Octave_descendent(MS,Fifth(MS,r32)) = r / 2 by Th51;
not Fifth(MS,r32) is_Between frequency,Octave(MS,frequency)
proof
assume
A5: Fifth(MS,r32) is_Between frequency,Octave(MS,frequency);
ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
hence contradiction by A5,A2,A3;
end;
hence thesis by A1,A2,A4,Def18;
end;
theorem Th85:
spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).4
= (27 qua Real) / 16 * @frequency
proof
set MS = HPS;
reconsider n2 = 3 as Nat;
set q = Fourth(MS,frequency);
spiral_of_fifths(MS,frequency,q).n2 is Element of MS;
then reconsider r32 = (9 qua Real) / 8 * @frequency as Element of MS
by Th84;
A1: spiral_of_fifths(MS,frequency,q).4
= spiral_of_fifths(MS,frequency,q).(n2 + 1)
.= Fifth_reduct(MS,frequency,
spiral_of_fifths(MS,frequency,q).n2) by Def19
.= Fifth_reduct(MS,frequency,r32) by Th84;
consider r,s be positive Real such that
A2: r = r32 & s = (3 qua Real) / 2 * r &
Fifth(MS,r32) = s by Th54;
A3: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
((27 qua Real) / 16) * @frequency < 2 * @frequency &
1 * @frequency < ((27 qua Real)/16) * @frequency by XREAL_1:68;
then Fifth(MS,r32) is_Between frequency,Octave(MS,frequency)
by A2,A3;
hence thesis by A2,A1,Def18;
end;
theorem Th86:
spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).5
= (81 qua Real) / 64 * @frequency
proof
set MS = HPS;
set q = Fourth(MS,frequency);
reconsider n3 = 4 as Nat;
spiral_of_fifths(MS,frequency,q).n3 is Element of MS;
then reconsider r32 = (27 qua Real) / 16 * @frequency as Element of MS
by Th85;
A1: spiral_of_fifths(MS,frequency,q).5
= spiral_of_fifths(MS,frequency,q).(n3 + 1)
.= Fifth_reduct(MS,frequency,
spiral_of_fifths(MS,frequency,q).n3) by Def19
.= Fifth_reduct(MS,frequency,r32) by Th85;
consider r,s be positive Real such that
A2: r = r32 & s = (3 qua Real) / 2 * r &
Fifth(MS,r32) = s by Th54;
A3: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
A4: not @frequency <= ((81 qua Real)/32) * @frequency
<= 2 * @frequency by XREAL_1:68;
A5: ex r being positive Real st Fifth(MS,r32) = r &
Octave_descendent(MS,Fifth(MS,r32)) = r / 2 by Th51;
not Fifth(MS,r32) is_Between frequency,Octave(MS,frequency) by A4,A2,A3;
hence thesis by A1,A2,A5,Def18;
end;
theorem Th87:
spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).6
= (243 qua Real) / 128 * @frequency
proof
set MS = HPS;
reconsider n4 = 5 as Nat;
set q = Fourth(MS,frequency);
spiral_of_fifths(MS,frequency,q).n4 is Element of MS;
then reconsider r32 = (81 qua Real) / 64 * @frequency as Element of MS
by Th86;
A1: spiral_of_fifths(MS,frequency,q).6
= spiral_of_fifths(MS,frequency,q).(n4 + 1)
.= Fifth_reduct(MS,frequency,
spiral_of_fifths(MS,frequency,q).n4) by Def19
.= Fifth_reduct(MS,frequency,r32) by Th86;
consider r,s be positive Real such that
A2: r = r32 & s = (3 qua Real) / 2 * r &
Fifth(MS,r32) = s by Th54;
A3: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
((243 qua Real) / 128) * @frequency < 2 * @frequency &
1 * @frequency < ((243 qua Real) / 128) * @frequency
by XREAL_1:68;
then Fifth(MS,r32) is_Between frequency,Octave(MS,frequency) by A2,A3;
hence thesis by A2,A1,Def18;
end;
theorem Th88:
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
proof
set MS = HPS;
set gamme = heptatonic_pythagorean_scale(MS,frequency);
A1: gamme.1 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1 &
gamme.2 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).3 &
gamme.3 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).5 &
gamme.4 = Fourth(MS,frequency) &
gamme.5 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).2 &
gamme.6 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).4 &
gamme.7 = spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).6 &
gamme.8
= Octave(MS,spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1)
by Def26;
gamme in 8-tuples_on the carrier of MS;
then gamme in {s where s is Element of (the carrier of MS)*: len s = 8}
by FINSEQ_2:def 4;
then consider s be Element of (the carrier of MS)* such that
A2: s = gamme and
A3: len s = 8;
dom s = Seg 8 by A3,FINSEQ_1:def 3;
then reconsider g1 = gamme.4, g2 = gamme.1, g3 = gamme.5,
g4 = gamme.2, g5 = gamme.6, g6 = gamme.3, g7 = gamme.7,
g8 = gamme.8 as Element of the carrier of MS by A2,FINSEQ_1:1,FINSEQ_2:11;
reconsider frequency2 = g1 as Element of MS;
reconsider r1 = @frequency2, r2 = @g2, r3 = @g3, r4 = @g4,
r5 = @g5, r6 = @g6, r7 = @g7, r8 =@g8 as positive Real;
A4: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
A5: r8 = Octave(MS,spiral_of_fifths(MS,frequency,Fourth(MS,frequency)).1)
by Def26
.= 2 * @frequency by A4,Th82;
ex fr be positive Real st frequency = fr &
Fourth(MS,frequency) = (4 qua Real) / 3 * fr by Def24;
hence thesis by A5,A1,Th82,Th84,Th86,Th83,Th85,Th87;
end;
theorem Th88BIS:
heptatonic_pythagorean_scale(HPS,frequency) is heptatonic
proof
set MS = HPS;
set gamme = heptatonic_pythagorean_scale(MS,frequency);
now
now
reconsider r1 = 1 * @frequency,
r2 = (9 qua Real) / 8 * @frequency,
r3 = (81 qua Real) / 64 * @frequency,
r4 = (4 qua Real) / 3 * @frequency,
r5 = (3 qua Real) / 2 * @frequency,
r6 = (27 qua Real) / 16 * @frequency,
r7 = (243 qua Real) / 128 * @frequency,
r8 = 2 * @frequency as positive Real;
take r1,r2,r3,r4,r5,r6,r7,r8;
heptatonic_pythagorean_scale(MS,frequency).1 = 1 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).2
= (9 qua Real) / 8 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).3
= (81 qua Real) / 64 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).4
= (4 qua Real) / 3 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).5
= (3 qua Real) / 2 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).6
= (27 qua Real) / 16 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).7
= (243 qua Real) / 128 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).8
= 2 * @frequency by Th88;
hence gamme.1 = frequency & gamme.1 = r1 &
gamme.2 = r2 & gamme.3 = r3 & gamme.4 = r4 & gamme.5 = r5 &
gamme.6 = r6 & gamme.7 = r7 & gamme.8 = r8;
thus r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 &
r6 < r7 & r7 < r8 by XREAL_1:98;
end;
hence ex frequency be Element of MS,
r1,r2,r3,r4,r5,r6,r7,r8 be positive Real st
gamme.1 = r1 & gamme.2 = r2 & gamme.3 = r3 & gamme.4 = r4 &
gamme.5 = r5 & gamme.6 = r6 & gamme.7 = r7 & gamme.8 = r8 &
r1 < r2 < r3 & r3 < r4 < r5 & r5 < r6 & r6 < r7 & r7 < r8;
A1: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
heptatonic_pythagorean_scale(MS,frequency).1 = 1 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).2
= (9 qua Real) / 8 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).3
= (81 qua Real) / 64 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).4
= (4 qua Real) / 3 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).5
= (3 qua Real) / 2 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).6
= (27 qua Real) / 16 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).7
= (243 qua Real) / 128 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).8
= 2 * @frequency by Th88;
hence gamme.8 = Octave(MS,frequency) &
gamme.1 = frequency by A1;
end;
hence thesis;
end;
definition
func heptatonic_pythagorean_semitone -> positive Real equals
(256 qua Real) / 243;
coherence;
end;
notation
synonym limma_pythagoricien for heptatonic_pythagorean_semitone;
end;
notation
synonym diatonic_tone for pythagorean_tone;
end;
theorem
pythagorean_tone / 2 < heptatonic_pythagorean_semitone;
theorem
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
heptatonic_pythagorean_scale(HPS,frequency).1;
coherence
proof
heptatonic_pythagorean_scale(HPS,frequency).1
= spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).1
by Def26;
hence thesis;
end;
func hepta_1(HPS,frequency) -> Element of HPS equals
heptatonic_pythagorean_scale(HPS,frequency).2;
coherence
proof
heptatonic_pythagorean_scale(HPS,frequency).2
= spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).3
by Def26;
hence thesis;
end;
func hepta_2(HPS,frequency) -> Element of HPS equals
heptatonic_pythagorean_scale(HPS,frequency).3;
coherence
proof
heptatonic_pythagorean_scale(HPS,frequency).3
= spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).5
by Def26;
hence thesis;
end;
func hepta_3(HPS,frequency) -> Element of HPS equals
heptatonic_pythagorean_scale(HPS,frequency).4;
coherence
proof
heptatonic_pythagorean_scale(HPS,frequency).4 = Fourth(HPS,frequency)
by Def26;
hence thesis;
end;
func hepta_4(HPS,frequency) -> Element of HPS equals
heptatonic_pythagorean_scale(HPS,frequency).5;
coherence
proof
heptatonic_pythagorean_scale(HPS,frequency).5
= spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).2
by Def26;
hence thesis;
end;
func hepta_5(HPS,frequency) -> Element of HPS equals
heptatonic_pythagorean_scale(HPS,frequency).6;
coherence
proof
heptatonic_pythagorean_scale(HPS,frequency).6
= spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).4
by Def26;
hence thesis;
end;
func hepta_6(HPS,frequency) -> Element of HPS equals
heptatonic_pythagorean_scale(HPS,frequency).7;
coherence
proof
heptatonic_pythagorean_scale(HPS,frequency).7
= spiral_of_fifths(HPS,frequency,Fourth(HPS,frequency)).6
by Def26;
hence thesis;
end;
func hepta_octave(HPS,frequency) -> Element of HPS equals
Octave(HPS,frequency);
coherence;
end;
Lem89:
for r1,r2,r3,r4,r5,r6,r7,r8 being positive Real st
heptatonic_pythagorean_scale(HPS,frequency).1 = r1 &
heptatonic_pythagorean_scale(HPS,frequency).2 = r2 &
heptatonic_pythagorean_scale(HPS,frequency).3 = r3 &
heptatonic_pythagorean_scale(HPS,frequency).4 = r4 &
heptatonic_pythagorean_scale(HPS,frequency).5 = r5 &
heptatonic_pythagorean_scale(HPS,frequency).6 = r6 &
heptatonic_pythagorean_scale(HPS,frequency).7 = r7 &
heptatonic_pythagorean_scale(HPS,frequency).8 = r8
holds r2 / r1 = (9 qua Real) / 8 & r3 / r2 = (9 qua Real) / 8 &
r4 / r3 = (256 qua Real) / 243 & r5 / r4 = (9 qua Real) / 8 &
r6 / r5 = (9 qua Real) / 8 & r7 / r6 = (9 qua Real) / 8 &
r8 / r7 = (256 qua Real) / 243
proof
set MS = HPS;
let r1,r2,r3,r4,r5,r6,r7,r8 be positive Real;
assume heptatonic_pythagorean_scale(MS,frequency).1 = r1 &
heptatonic_pythagorean_scale(MS,frequency).2 = r2 &
heptatonic_pythagorean_scale(MS,frequency).3 = r3 &
heptatonic_pythagorean_scale(MS,frequency).4 = r4 &
heptatonic_pythagorean_scale(MS,frequency).5 = r5 &
heptatonic_pythagorean_scale(MS,frequency).6 = r6 &
heptatonic_pythagorean_scale(MS,frequency).7 = r7 &
heptatonic_pythagorean_scale(MS,frequency).8 = r8; then
r1 = 1 * @frequency & r2 = (9 qua Real) / 8 * @frequency &
r3 = (81 qua Real) / 64 * @frequency &
r4 = (4 qua Real) / 3 * @frequency &
r5 = (3 qua Real) / 2 * @frequency &
r6 = (27 qua Real) / 16 * @frequency &
r7 = (243 qua Real) / 128 * @frequency & r8 = 2 * @frequency by Th88;
then r2 / r1 = ((9 qua Real) / 8 * @frequency) / (1 * @frequency) &
r3 / r2 = ((81 qua Real) / 64) / ((9 qua Real) / 8) &
r4 / r3 = ((4 qua Real) / 3) / ((81 qua Real) / 64) &
r5 / r4 = ((3 qua Real) / 2) / ((4 qua Real) / 3) &
r6 / r5 = ((27 qua Real) / 16) / ((3 qua Real) / 2) &
r7 / r6 = ((243 qua Real) / 128) / ((27 qua Real) / 16) &
r8 / r7 = (2 qua Real) / ((243 qua Real) / 128)
by XCMPLX_1:91;
hence thesis by XCMPLX_1:89;
end;
Lem90:
ex r1,r2,r3,r4,r5,r6,r7,r8 being positive Real st
heptatonic_pythagorean_scale(HPS,frequency).1 = r1 &
heptatonic_pythagorean_scale(HPS,frequency).2 = r2 &
heptatonic_pythagorean_scale(HPS,frequency).3 = r3 &
heptatonic_pythagorean_scale(HPS,frequency).4 = r4 &
heptatonic_pythagorean_scale(HPS,frequency).5 = r5 &
heptatonic_pythagorean_scale(HPS,frequency).6 = r6 &
heptatonic_pythagorean_scale(HPS,frequency).7 = r7 &
heptatonic_pythagorean_scale(HPS,frequency).8 = r8 &
r2 / r1 = (9 qua Real) / 8 & r3 / r2 = (9 qua Real) / 8 &
r4 / r3 = (256 qua Real) / 243 & r5 / r4 = (9 qua Real) / 8 &
r6 / r5 = (9 qua Real) / 8 & r7 / r6 = (9 qua Real) / 8 &
r8 / r7 = (256 qua Real) / 243
proof
set MS = HPS;
set r1 = hepta_fondamental(MS,frequency), r2 = hepta_1(MS,frequency),
r3 = hepta_2(MS,frequency), r4 = hepta_3(MS,frequency),
r5 = hepta_4(MS,frequency), r6 = hepta_5(MS,frequency),
r7 = hepta_6(MS,frequency), r8 = hepta_octave(MS,frequency);
the carrier of MS c= REALPLUS by Def07a;
then reconsider r91 = r1,r92 = r2,r93 = r3,
r94 = r4,r95 = r5,r96 = r6,r97 = r7,r98 = r8 as positive Real by Th1;
take r91,r92,r93,r94,r95,r96,r97;
A1: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
A2: heptatonic_pythagorean_scale(MS,frequency).1 = 1 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).2
= (9 qua Real) / 8 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).3
= (81 qua Real) / 64 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).4
= (4 qua Real) / 3 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).5
= (3 qua Real) / 2 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).6
= (27 qua Real) / 16 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).7
= (243 qua Real) / 128 * @frequency &
heptatonic_pythagorean_scale(MS,frequency).8 = 2 * @frequency by Th88;
r1 = 1 * @frequency & r2 = (9 qua Real) / 8 * @frequency &
r3 = (81 qua Real) / 64 * @frequency &
r4 = (4 qua Real) / 3 * @frequency &
r5 = (3 qua Real) / 2 * @frequency &
r6 = (27 qua Real) / 16 * @frequency &
r7 = (243 qua Real) / 128 * @frequency &
r8 = 2 * @frequency by Th88,A1;
then heptatonic_pythagorean_scale(MS,frequency).1 = r91 &
heptatonic_pythagorean_scale(MS,frequency).2 = r92 &
heptatonic_pythagorean_scale(MS,frequency).3 = r93 &
heptatonic_pythagorean_scale(MS,frequency).4 = r94 &
heptatonic_pythagorean_scale(MS,frequency).5 = r95 &
heptatonic_pythagorean_scale(MS,frequency).6 = r96 &
heptatonic_pythagorean_scale(MS,frequency).7 = r97 &
heptatonic_pythagorean_scale(MS,frequency).8 = r98 by Th88;
then r92 / r91 = (9 qua Real) / 8 & r93 / r92 = (9 qua Real) / 8 &
r94 / r93 = (256 qua Real) / 243 & r95 / r94 = (9 qua Real) / 8 &
r96 / r95 = (9 qua Real) / 8 & r97 / r96 = (9 qua Real) / 8 &
r98 / r97 = (256 qua Real) / 243 by Lem89;
hence thesis by A1,A2;
end;
theorem Th90:
intrval(hepta_fondamental(HPS,frequency),hepta_1(HPS,frequency))
= pythagorean_tone &
intrval(hepta_1(HPS,frequency),hepta_2(HPS,frequency))
= pythagorean_tone &
intrval(hepta_2(HPS,frequency),hepta_3(HPS,frequency))
= heptatonic_pythagorean_semitone &
intrval(hepta_3(HPS,frequency),hepta_4(HPS,frequency))
= pythagorean_tone &
intrval(hepta_4(HPS,frequency),hepta_5(HPS,frequency))
= pythagorean_tone &
intrval(hepta_5(HPS,frequency),hepta_6(HPS,frequency))
= pythagorean_tone &
intrval(hepta_6(HPS,frequency),hepta_octave(HPS,frequency))
= heptatonic_pythagorean_semitone
proof
set MS = HPS;
A1: ex fr be positive Real st frequency = fr &
Octave(MS,frequency) = 2 * fr by Def15;
A2: heptatonic_pythagorean_scale(MS,frequency).8 = 2 * @frequency by Th88;
ex r1,r2,r3,r4,r5,r6,r7,r8 be positive Real st
heptatonic_pythagorean_scale(MS,frequency).1 = r1 &
heptatonic_pythagorean_scale(MS,frequency).2 = r2 &
heptatonic_pythagorean_scale(MS,frequency).3 = r3 &
heptatonic_pythagorean_scale(MS,frequency).4 = r4 &
heptatonic_pythagorean_scale(MS,frequency).5 = r5 &
heptatonic_pythagorean_scale(MS,frequency).6 = r6 &
heptatonic_pythagorean_scale(MS,frequency).7 = r7 &
heptatonic_pythagorean_scale(MS,frequency).8 = r8 &
r2 / r1 = (9 qua Real) / 8 & r3 / r2 = (9 qua Real) / 8 &
r4 / r3 = (256 qua Real) / 243 & r5 / r4 = (9 qua Real) / 8 &
r6 / r5 = (9 qua Real) / 8 & r7 / r6 = (9 qua Real) / 8 &
r8 / r7 = (256 qua Real) / 243 by Lem90;
hence thesis by A1,A2,Def21;
end;
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 :Def27:
[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
for HPS being satisfying_euclidean Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
heptatonic_pythagorean_scale(HPS,frequency) is perfect_fifth
proof
let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;
A1: heptatonic_pythagorean_scale(HPS,frequency) is heptatonic by Th88BIS;
set gamme = heptatonic_pythagorean_scale(HPS,frequency);
A2: hepta_fondamental(HPS,frequency) = 1 * @frequency &
hepta_1(HPS,frequency) = (9 qua Real) / 8 * @frequency &
hepta_2(HPS,frequency) = (81 qua Real) / 64 * @frequency &
hepta_3(HPS,frequency) = (4 qua Real) / 3 * @frequency &
hepta_4(HPS,frequency) = (3 qua Real) / 2 * @frequency &
hepta_5(HPS,frequency) = (27 qua Real) / 16 * @frequency &
hepta_6(HPS,frequency) = (243 qua Real) / 128 * @frequency by Th88;
A3: ex fo be positive Real st frequency = fo &
Octave(HPS,frequency) = 2 * fo by Def15;
then hepta_octave(HPS,frequency) = 2 * @frequency;
then
A4: hepta_octave(HPS,frequency) = gamme.8 by Th88;
A5: (the Ratio of HPS).(hepta_fondamental(HPS,frequency),
hepta_4(HPS,frequency))
= @hepta_4(HPS,frequency) / @hepta_fondamental(HPS,frequency) by Def25
.= (3 qua Real) / 2 by A2,XCMPLX_1:89;
A6: (the Ratio of HPS).(hepta_1(HPS,frequency),
hepta_5(HPS,frequency))
= @hepta_5(HPS,frequency) / @hepta_1(HPS,frequency) by Def25
.= (((27 qua Real) / 16)/((9 qua Real) / 8)) * (@frequency / @frequency)
by A2,XCMPLX_1:76
.= (3 qua Real) / 2 by XCMPLX_1:88;
A7: (the Ratio of HPS).(hepta_2(HPS,frequency),
hepta_6(HPS,frequency))
= @hepta_6(HPS,frequency) / @hepta_2(HPS,frequency) by Def25
.= (((243 qua Real) / 128)/((81 qua Real) / 64)) *
(@frequency / @frequency) by A2,XCMPLX_1:76
.= (3 qua Real) / 2 by XCMPLX_1:88;
A8: (the Ratio of HPS).(hepta_3(HPS,frequency),
hepta_octave(HPS,frequency))
= @hepta_octave(HPS,frequency) / @hepta_3(HPS,frequency) by Def25
.= ((2 qua Real) * @frequency) / ((4 qua Real) / 3 * @frequency)
by Th88,A3
.= ((2 qua Real) /((4 qua Real) / 3)) * (@frequency / @frequency)
by XCMPLX_1:76
.= (3 qua Real) / 2 by XCMPLX_1:88;
reconsider n2 = 2,n3 = 3 as Element of HPS by Th20;
(the Ratio of HPS).(n2,n3) = @n3 / @n2 by Def25
.= (3 qua Real) / 2;
then n2,n3 equiv hepta_fondamental(HPS,frequency),hepta_4(HPS,frequency) &
n2,n3 equiv hepta_1(HPS,frequency),hepta_5(HPS,frequency) &
n2,n3 equiv hepta_2(HPS,frequency),hepta_6(HPS,frequency) &
n2,n3 equiv hepta_3(HPS,frequency),hepta_octave(HPS,frequency)
by A5,A6,A7,A8,Def08a;
then [hepta_fondamental(HPS,frequency),hepta_4(HPS,frequency)]
in fifth(HPS) &
[hepta_1(HPS,frequency),hepta_5(HPS,frequency)] in fifth(HPS) &
[hepta_2(HPS,frequency),hepta_6(HPS,frequency)] in fifth(HPS) &
[hepta_3(HPS,frequency),hepta_octave(HPS,frequency)] in fifth(HPS)
by EQREL_1:18;
hence thesis by A4,A1,Def27;
end;
definition
let HPS be Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;
func heptatonic_pythagorean_scale_ascending(HPS,frequency) ->
Element of 8-tuples_on the carrier of HPS equals
heptatonic_pythagorean_scale(HPS,Octave(HPS,frequency));
coherence;
end;
theorem Th91:
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
proof
set f2 = Octave(HPS,frequency);
consider fr be positive Real such that
A1: frequency = fr & Octave(HPS,frequency) = 2 * fr by Def15;
heptatonic_pythagorean_scale(HPS,f2).1 = 1 * @f2 &
heptatonic_pythagorean_scale(HPS,f2).2
= (9 qua Real) / 8 * @f2 &
heptatonic_pythagorean_scale(HPS,f2).3
= (81 qua Real) / 64 * @f2 &
heptatonic_pythagorean_scale(HPS,f2).4
= (4 qua Real) / 3 * @f2 &
heptatonic_pythagorean_scale(HPS,f2).5
= (3 qua Real) / 2 * @f2 &
heptatonic_pythagorean_scale(HPS,f2).6
= (27 qua Real) / 16 * @f2 &
heptatonic_pythagorean_scale(HPS,f2).7
= (243 qua Real) / 128 * @f2 &
heptatonic_pythagorean_scale(HPS,f2).8 = 2 * @f2
by Th88;
hence thesis by A1;
end;
theorem
heptatonic_pythagorean_scale(HPS,frequency).8
= heptatonic_pythagorean_scale_ascending(HPS,frequency).1
proof
heptatonic_pythagorean_scale(HPS,frequency).8 = 2 * @frequency &
heptatonic_pythagorean_scale_ascending(HPS,frequency).1 = 2 * @frequency
by Th88,Th91;
hence thesis;
end;
theorem Th92:
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
proof
set gamme = heptatonic_pythagorean_scale(HPS,frequency);
A1: hepta_fondamental(HPS,frequency) = 1 * @frequency &
hepta_1(HPS,frequency) = (9 qua Real) / 8 * @frequency &
hepta_2(HPS,frequency) = (81 qua Real) / 64 * @frequency &
hepta_3(HPS,frequency) = (4 qua Real) / 3 * @frequency &
hepta_4(HPS,frequency) = (3 qua Real) / 2 * @frequency &
hepta_5(HPS,frequency) = (27 qua Real) / 16 * @frequency &
hepta_6(HPS,frequency) = (243 qua Real) / 128 * @frequency by Th88;
set f2 = Octave(HPS,frequency);
set gamme2 = heptatonic_pythagorean_scale(HPS,f2);
A2: 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
by Th91;
A3: ex fo be positive Real st frequency = fo &
Octave(HPS,frequency) = 2 * fo by Def15;
now
thus intrval(hepta_4(HPS,frequency),
hepta_1(HPS,Octave(HPS,frequency)))
= (((9 qua Real) / 4) * @frequency) / (((3 qua Real) / 2) * @frequency)
by A2,A1,Def21
.=(((9 qua Real) / 4) / ((3 qua Real) / 2) * @frequency) / @frequency
by XCMPLX_1:83
.= (3 qua Real) / 2 by XCMPLX_1:89;
thus intrval(hepta_5(HPS,frequency),
hepta_2(HPS,Octave(HPS,frequency)))
= ((81 qua Real) / 32 * @frequency) / ((27 qua Real) / 16 * @frequency)
by A2,A1,Def21
.=(((81 qua Real) / 32) / ((27 qua Real) / 16) * @frequency) /
@frequency
by XCMPLX_1:83
.= (3 qua Real) / 2 by XCMPLX_1:89;
intrval(hepta_6(HPS,frequency),hepta_3(HPS,Octave(HPS,frequency)))
= ((8 qua Real) / 3 * @frequency) / ((243 qua Real) / 128 * @frequency)
by A2,A1,Def21
.=(((8 qua Real) / 3) / ((243 qua Real) / 128) * @frequency) /
@frequency
by XCMPLX_1:83;
hence intrval(hepta_6(HPS,frequency),
hepta_3(HPS,Octave(HPS,frequency))) <> (3 qua Real) / 2 by XCMPLX_1:89;
thus intrval(hepta_octave(HPS,frequency),
hepta_4(HPS,Octave(HPS,frequency)))
= ((3 qua Real) * @frequency) / (2 * @frequency) by A3,A2,Def21
.= (((3 qua Real) / 2) * @frequency) / @frequency by XCMPLX_1:83
.= (3 qua Real) / 2 by XCMPLX_1:89;
end;
hence thesis;
end;
theorem Th93:
for HPS being satisfying_euclidean Heptatonic_Pythagorean_Score
for f1,f2 being Element of HPS
holds intrval(f1,f2) = (the Ratio of HPS).(f1,f2)
proof
let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score;
let f1,f2 be Element of HPS;
(the Ratio of HPS).(f1,f2) = @f2 / @f1 by Def25;
hence thesis by Def21;
end;
theorem
for HPS being satisfying_euclidean Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
[heptatonic_pythagorean_scale(HPS,frequency).5,
heptatonic_pythagorean_scale_ascending(HPS,frequency).2]
in fifth(HPS) &
[heptatonic_pythagorean_scale(HPS,frequency).6,
heptatonic_pythagorean_scale_ascending(HPS,frequency).3]
in fifth(HPS) &
not [heptatonic_pythagorean_scale(HPS,frequency).7,
heptatonic_pythagorean_scale_ascending(HPS,frequency).4]
in fifth(HPS)
proof
let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score;
let frequency be Element of HPS;
A1: 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 by Th92;
reconsider n2 = 2,n3 = 3 as Element of HPS by Th20;
(the Ratio of HPS).(n2,n3) = @n3 / @n2 by Def25
.= (3 qua Real) / 2;
then (the Ratio of HPS).(hepta_4(HPS,frequency),
hepta_1(HPS,Octave(HPS,frequency)))
= (the Ratio of HPS).(n2,n3) &
(the Ratio of HPS).(hepta_5(HPS,frequency),
hepta_2(HPS,Octave(HPS,frequency)))
= (the Ratio of HPS).(n2,n3) &
(the Ratio of HPS).(hepta_6(HPS,frequency),
hepta_3(HPS,Octave(HPS,frequency)))
<> (the Ratio of HPS).(n2,n3) by A1,Th93;
then n2,n3 equiv hepta_4(HPS,frequency),
hepta_1(HPS,Octave(HPS,frequency)) &
n2,n3 equiv hepta_5(HPS,frequency),hepta_2(HPS,Octave(HPS,frequency)) &
not n2,n3 equiv hepta_6(HPS,frequency),hepta_3(HPS,Octave(HPS,frequency))
by Def08a;
hence thesis by EQREL_1:18;
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;
let i be Nat;
func #(scale,i) -> Element of HPS equals
:Def28: scale.i if
i in Seg n otherwise the Element of HPS;
correctness
proof
per cases;
suppose
A1: i in Seg n;
scale is Element of Funcs(Seg n,the carrier of HPS) by FINSEQ_2:93;
then dom scale = Seg n & rng scale c= the carrier of HPS by FUNCT_2:92;
then scale.i in rng scale by A1,FUNCT_1:def 3;
hence thesis;
end;
suppose not i in Seg n;
hence thesis;
end;
end;
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
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
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
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
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
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
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
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
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
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
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 :Def29:
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
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
heptatonic_pythagorean_scale(HPS,frequency) is ionan
proof
set scale = heptatonic_pythagorean_scale(HPS,frequency);
A1: scale is heptatonic by Th88BIS;
reconsider t1 = pythagorean_tone,
t2 = heptatonic_pythagorean_semitone as positive Real;
ex r be positive Real st r = frequency &
Octave(HPS,frequency) = 2 * r by Def15;
then
A2: hepta_octave(HPS,frequency) = 2 * @frequency;
1 in Seg 8 & 2 in Seg 8 & 3 in Seg 8 & 4 in Seg 8 &
5 in Seg 8 & 6 in Seg 8 & 7 in Seg 8 & 8 in Seg 8
by FINSEQ_1:1;
then scale.1 = #(scale,1) & scale.2 = #(scale,2) &
scale.3 = #(scale,3) & scale.4 = #(scale,4) &
scale.5 = #(scale,5) & scale.6 = #(scale,6) &
scale.7 = #(scale,7) & scale.8 = #(scale,8)
by Def28;
then hepta_fondamental(HPS,frequency) = #(scale,1) &
hepta_1(HPS,frequency) = #(scale,2) &
hepta_2(HPS,frequency) = #(scale,3) &
hepta_3(HPS,frequency) = #(scale,4) &
hepta_4(HPS,frequency) = #(scale,5) &
hepta_5(HPS,frequency) = #(scale,6) &
hepta_6(HPS,frequency) = #(scale,7) &
hepta_octave(HPS,frequency) = #(scale,8)
by A2,Th88;
then 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 by Th90;
hence thesis by A1,Def29;
end;