module module high

`IndisputableMonolith.Musicology.ModalPreferenceFromPhi`

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

Does not derive the seven modes from the forcing chain.
Does not compute explicit numerical J-cost values, only integer ranks.
Does not address non-diatonic or non-Greek scales.
Does not connect ranks to auditory experiments or perception data.

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