`all_length`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Musicology.ModalPreferenceFromPhi on GitHub at line 70.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  67def all : List GreekMode :=
  68  [.Ionian, .Aeolian, .Mixolydian, .Lydian, .Dorian, .Phrygian, .Locrian]
  69
  70theorem all_length : all.length = 7 := by decide
  71
  72/-- Mode set is pairwise distinct. -/
  73theorem all_nodup : all.Nodup := by decide
  74
  75/-- Ionian has lowest rank. -/
  76theorem ionian_lowest : costRank .Ionian = 0 := rfl
  77
  78/-- Aeolian has rank 1. -/
  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,

papers checked against this theorem

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