IndisputableMonolith.Musicology.ModalPreferenceFromPhi
The module defines Greek musical modes and their cost ranks under the Recognition Science J-cost function, establishing Ionian and Aeolian as lowest-ranked (most preferred) and Locrian as highest. Music theorists applying RS to scale preferences would cite these definitions. The module consists of enumerated modes, a ranking function, and supporting lemmas on uniqueness and ordering, all built from imported Cost primitives.
claimGreek modes are enumerated as seven distinct objects; the cost rank function assigns integers with $\mathrm{rank}(\mathrm{Ionian})=0$, $\mathrm{rank}(\mathrm{Aeolian})=1$, $\mathrm{rank}(\mathrm{Locrian})=6$, lower rank indicating higher preference under the J-cost derived from $\phi$.
background
The module imports Constants, where the fundamental RS time quantum satisfies $\tau_0=1$ tick, and Cost, which supplies the J-cost and defectDist primitives used to rank structures. It introduces GreekMode as the seven classical modes and costRank as the integer-valued preference measure. The local setting is an application of the phi-ladder to discrete combinatorial objects, with the module doc-comment stating that lower cost rank equals greater preference.
proof idea
This is a definition module, no proofs. It enumerates the modes, defines the ranking map, and supplies basic lemmas on length, nodup, and extremal positions (ionian_lowest, locrian_highest) that follow directly from the ordering.
why it matters in Recognition Science
The module supplies the musicological layer that applies the phi-forced self-similar fixed point (T6) and J-cost to modal structures. No downstream theorems are recorded in the used_by graph, so it currently stands as an isolated application rather than a dependency for larger results.
scope and limits
- Does not derive the J-cost function itself.
- Does not treat non-diatonic or microtonal scales.
- Does not compute continuous pitch values, only discrete ranks.
- Does not address historical or cultural validation of the preference order.
depends on (2)
declarations in this module (16)
-
inductive
GreekMode -
def
costRank -
def
all -
theorem
all_length -
theorem
all_nodup -
theorem
ionian_lowest -
theorem
aeolian_second -
theorem
locrian_highest -
theorem
ionian_aeolian_dominant -
theorem
locrian_uniquely_worst -
def
majorThirdReference -
theorem
majorThirdReference_pos -
theorem
majorThirdReference_below_phi -
structure
ModalPreferenceCert -
def
modalPreferenceCert -
theorem
musicology_one_statement