locrian_uniquely_worst
plain-language theorem explainer
The theorem states that every Greek mode except Locrian has strictly lower cost rank than Locrian itself. Musicologists modeling cross-cultural preferences via interval costs would cite it to confirm Locrian as the unique maximum. The proof uses exhaustive case analysis on the inductive GreekMode type, discharging the Locrian case by contradiction and deciding the inequality for the other six modes by computation.
Claim. For every Greek mode $m$ with $m$ distinct from Locrian, the cost rank of $m$ is strictly less than the cost rank of Locrian.
background
GreekMode is the inductive enumeration of the seven modes: Ionian (major), Dorian, Phrygian, Lydian, Mixolydian, Aeolian (minor), and Locrian. costRank is the function that assigns natural-number ranks to these modes, with Ionian at 0, Aeolian at 1, Mixolydian at 2, Lydian at 3, Dorian at 4, Phrygian at 5, and Locrian at 6. The module derives modal preference orderings from J-costs of each mode's interval ratios measured against a φ-rational reference scale; lower rank corresponds to higher predicted preference.
proof idea
The proof performs case analysis on the inductive GreekMode. The Locrian case is eliminated by ex falso using the hypothesis m ≠ Locrian. For each of the remaining six constructors the strict inequality costRank m < costRank Locrian is settled by the decide tactic.
why it matters
This lemma supplies the locrian_highest field of ModalPreferenceCert and is invoked inside musicology_one_statement to assert that Locrian is uniquely worst. It completes the chain showing that the φ-derived cost ordering reproduces the observed ranking (Ionian and Aeolian lowest, Locrian highest) reported in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.