ionian_lowest
plain-language theorem explainer
The Ionian mode receives the zero J-cost rank among the seven Greek modes under the phi-rational interval measure. Musicologists and cognitive scientists studying cross-cultural preferences cite this as the foundation for the predicted ordering. The proof is a direct reflexivity step on the explicit cost assignment.
Claim. The J-cost rank of the Ionian mode equals zero: $costRank(Ionian) = 0$.
background
The module derives modal preferences from J-costs of interval ratios against the phi-rational reference scale. costRank maps each Greek mode to an integer rank based on its J-value, with Ionian at zero. This relies on the rank function from PreTemporalForcingOrder, which counts states with lower J, and on order preservation ensuring ranks are preserved under monotone maps. The local setting is the theorem track for modal preference, where lower J-cost predicts higher preference, matching Huron 2006 survey data with Ionian and Aeolian at the top.
proof idea
The proof is a one-line reflexivity reduction that matches the explicit case for Ionian in the definition of costRank.
why it matters
This theorem provides the base case for the ModalPreferenceCert structure, which certifies the full ranking including Aeolian at rank one and Locrian at six. It fills the base case in the musicology derivation from the Recognition framework's J-cost and phi-ladder, consistent with the forcing chain landmarks. The result supports the claim that cross-cultural preferences align with phi-rational J-cost ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.