costRank
plain-language theorem explainer
costRank assigns natural-number ranks to the seven Greek modes by increasing J-cost against the phi-rational reference scale, placing Ionian at 0 and Locrian at 6. Music theorists and Recognition Science researchers would cite it to ground cross-cultural modal preference in the forcing chain. The definition is realized by exhaustive pattern matching on the GreekMode inductive type.
Claim. Define the function costRank from GreekMode to natural numbers by costRank(Ionian) = 0, costRank(Aeolian) = 1, costRank(Mixolydian) = 2, costRank(Lydian) = 3, costRank(Dorian) = 4, costRank(Phrygian) = 5, costRank(Locrian) = 6.
background
GreekMode is the inductive type with seven constructors enumerating the traditional modes: Ionian (major), Dorian, Phrygian, Lydian, Mixolydian, Aeolian (minor), and Locrian. costRank orders them by J-cost, where J(x) = (x + x^{-1})/2 - 1 is the Recognition Science cost function from T5. The module models modal preference as J-cost ranking of interval ratios relative to the phi-rational reference, matching Huron 2006 surveys with Ionian and Aeolian lowest and Locrian highest. Upstream, the modes definition supplies the finite set of truncated modes from the Galerkin2D classical bridge.
proof idea
The declaration is a definition by pattern matching that directly enumerates the seven constructors of GreekMode and assigns the integers 0 through 6 in order of increasing J-cost.
why it matters
costRank supplies the concrete ordering consumed by downstream results including ionian_lowest, aeolian_second, locrian_highest, locrian_uniquely_worst, and the ModalPreferenceCert structure. It fills the paper proposition that cross-cultural modal preference follows J-cost on the phi-ladder, connecting to T5 J-uniqueness, the eight-tick octave, and the phi^5 constants. No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.