`locrian_highest`

proved

show as: view math explainer →

module: IndisputableMonolith.Musicology.ModalPreferenceFromPhi
domain: Musicology
line: 82 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Musicology.ModalPreferenceFromPhi on GitHub at line 82.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  79theorem aeolian_second : costRank .Aeolian = 1 := rfl
  80
  81/-- Locrian has highest rank. -/
  82theorem locrian_highest : costRank .Locrian = 6 := rfl
  83
  84/-- Ionian and Aeolian dominate (rank ≤ 1). -/
  85theorem ionian_aeolian_dominant :
  86    costRank .Ionian ≤ 1 ∧ costRank .Aeolian ≤ 1 := by
  87  refine ⟨?_, ?_⟩ <;> decide
  88
  89/-- Locrian is uniquely worst (rank > all others). -/
  90theorem locrian_uniquely_worst (m : GreekMode) (h : m ≠ .Locrian) :
  91    costRank m < costRank .Locrian := by
  92  cases m <;> first | (exfalso; exact h rfl) | decide
  93
  94end GreekMode
  95
  96/-! ## §2. φ-rational interval reference -/
  97
  98noncomputable section
  99
 100/-- Reference major-third frequency ratio = 5/4 (just intonation,
 101φ-rational neighbour 4·φ⁻² ≈ 1.528 vs 1.25 for just). -/
 102def majorThirdReference : ℝ := 5 / 4
 103
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.