locrian_highest
plain-language theorem explainer
Locrian mode receives the highest J-cost rank of 6 among the seven Greek modes. Music cognition researchers cite this result to confirm the predicted ordering from φ-rational intervals against cross-cultural survey data. The proof is immediate reflexivity on the costRank definition.
Claim. The cost rank of the Locrian mode equals 6.
background
The module assigns J-cost ranks to the seven Greek modes based on interval ratios relative to the φ-rational reference scale. costRank maps each mode to an integer, with lower values indicating higher preference; the definition explicitly places Locrian at 6. Upstream rank from PreTemporalForcingOrder supplies the numerical ordering of forcing stages, while the order-preservation rank from RRF counts states with strictly lower J-value.
proof idea
The proof is a one-line wrapper that applies reflexivity to the costRank definition.
why it matters
This theorem supplies the locrian_highest field for the ModalPreferenceCert structure, which aggregates mode counts, distinctness, and the full rank bounds. It anchors the Recognition Science claim that J-cost ordering from the phi-ladder governs modal preference, consistent with T5 J-uniqueness and the RCL. The result leaves open empirical validation through expanded cross-cultural surveys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.