pith. sign in
module module moderate

IndisputableMonolith.Musicology.ModalPreferenceFromPhi

show as:
view Lean formalization →

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)