theorem
proved
majorThirdReference_pos
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Musicology.ModalPreferenceFromPhi on GitHub at line 107.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
104/-- φ-rational neighbour: 4 · φ⁻² ≈ 1.528. The discrepancy
105`majorThirdReference - 1` is the σ-charge of the major-third interval
106relative to perfect fifth (3/2). -/
107theorem majorThirdReference_pos : 0 < majorThirdReference := by
108 unfold majorThirdReference; norm_num
109
110theorem majorThirdReference_below_phi : majorThirdReference < phi := by
111 unfold majorThirdReference
112 have := phi_gt_onePointFive; linarith
113
114end
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