pith. sign in
module module high

IndisputableMonolith.Musicology.ModalPreferenceFromPhi

show as:
view Lean formalization →

This module defines the seven Greek modes and assigns them integer cost ranks derived from the J-cost function, establishing Ionian and Aeolian as lowest-ranked (most preferred) and Locrian as highest. Music theorists or RS researchers extending the framework to scale preferences would cite the explicit ordering. The module is built from enumerations, rank computations, and short lemmas verifying uniqueness and ordering properties.

claimLet $M$ be the set of Greek modes. The rank function $r: M o \{0,1,\dots,6\}$ satisfies $r(\text{Ionian})=0$, $r(\text{Aeolian})=1$, $r(\text{Locrian})=6$, with lower $r$ indicating lower J-cost and thus higher preference.

background

The module imports the RS time quantum $\tau_0=1$ tick from Constants and the J-cost machinery from the Cost module. It introduces GreekMode as an enumeration of the seven traditional modes and costRank as the integer ordering induced by evaluating the J-cost on each mode. Sibling definitions include all (the complete list), all_nodup (distinctness), and targeted lemmas such as ionian_lowest and locrian_highest that record the extremal ranks.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module populates the musicology domain by supplying concrete mode rankings that can feed parent results on phi-derived preferences. It directly implements the DOC_COMMENT claim that Ionian and Aeolian are the two lowest-cost modes while Locrian is uniquely worst, extending the J-uniqueness and phi-ladder landmarks into scale selection without yet appearing in any used_by theorems.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)