module module moderate

`IndisputableMonolith.Musicology.ModalPreferenceFromPhi`

The ModalPreferenceFromPhi module ranks the seven Greek modes by J-cost derived from Recognition Science, placing Ionian and Aeolian at the lowest ranks (most preferred) and Locrian at the highest. Music theorists or RS researchers extending the framework to scales would cite the explicit ordering. The module consists entirely of definitions and enumerated facts with no proofs.

claimGreekMode enumerates the seven traditional modes; costRank : GreekMode → ℕ satisfies costRank(Ionian) = 0, costRank(Aeolian) = 1 and costRank(Locrian) = 6, with lower values indicating lower J-cost and higher preference.

background

The module sits in the musicology domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the cost machinery from Cost. It defines GreekMode as the enumeration of Ionian, Dorian, Phrygian, Lydian, Mixolydian, Aeolian and Locrian, then introduces costRank as the ordering induced by the J-cost function. The DOC_COMMENT states the ranking directly: lower cost rank means higher preference, with Ionian and Aeolian lowest and Locrian highest.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete modal ranking that instantiates the J-cost in a new empirical domain, connecting to the phi-ladder and RCL from the forcing chain (T5–T6). No parent theorems appear in the used_by list, so the module currently stands as an isolated application rather than a lemma feeding a larger result.

scope and limits

Does not derive or compute explicit J-cost values for each mode.
Does not prove the ranking from the Recognition Composition Law.
Does not address non-Greek or non-diatonic scales.
Does not claim the ranking is universal across all musical cultures.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (16)

inductive GreekMode L43
def costRank L57
def all L67
theorem all_length L70
theorem all_nodup L73
theorem ionian_lowest L76
theorem aeolian_second L79
theorem locrian_highest L82
theorem ionian_aeolian_dominant L85
theorem locrian_uniquely_worst L90
def majorThirdReference L102
theorem majorThirdReference_pos L107
theorem majorThirdReference_below_phi L110
structure ModalPreferenceCert L118
def modalPreferenceCert L129
theorem musicology_one_statement L141