ModalPreferenceCert

formal source

 115
 116/-! ## §3. Master certificate -/
 117
 118structure ModalPreferenceCert where
 119  modes_count : GreekMode.all.length = 7
 120  modes_distinct : GreekMode.all.Nodup
 121  ionian_lowest : GreekMode.costRank .Ionian = 0
 122  aeolian_second : GreekMode.costRank .Aeolian = 1
 123  locrian_highest : GreekMode.costRank .Locrian = 6
 124  ionian_aeolian_dominant :
 125    GreekMode.costRank .Ionian ≤ 1 ∧ GreekMode.costRank .Aeolian ≤ 1
 126  locrian_uniquely_worst :
 127    ∀ m : GreekMode, m ≠ .Locrian → GreekMode.costRank m < GreekMode.costRank .Locrian
 128
 129def modalPreferenceCert : ModalPreferenceCert where
 130  modes_count := GreekMode.all_length
 131  modes_distinct := GreekMode.all_nodup
 132  ionian_lowest := GreekMode.ionian_lowest
 133  aeolian_second := GreekMode.aeolian_second
 134  locrian_highest := GreekMode.locrian_highest
 135  ionian_aeolian_dominant := GreekMode.ionian_aeolian_dominant
 136  locrian_uniquely_worst := GreekMode.locrian_uniquely_worst
 137
 138/-- **MUSICOLOGY ONE-STATEMENT.** Seven Greek modes, pairwise distinct.
 139Ionian (0) and Aeolian (1) have the two lowest cost ranks (most
 140preferred); Locrian (6) is uniquely worst. -/
 141theorem musicology_one_statement :
 142    GreekMode.all.length = 7 ∧
 143    GreekMode.costRank .Ionian = 0 ∧
 144    GreekMode.costRank .Aeolian = 1 ∧
 145    GreekMode.costRank .Locrian = 6 ∧
 146    (∀ m : GreekMode, m ≠ .Locrian →
 147       GreekMode.costRank m < GreekMode.costRank .Locrian) :=
 148  ⟨GreekMode.all_length, rfl, rfl, rfl, GreekMode.locrian_uniquely_worst⟩