modalPreferenceCert
plain-language theorem explainer
ModalPreferenceCert assembles a certified record of the seven Greek modes under J-cost ranking derived from φ-rational intervals. Cognitive musicologists and cross-cultural researchers would cite it to link Huron 2006 preference data to explicit cost ranks. The definition is a direct record constructor that references pre-established length, nodup, and costRank facts for the GreekMode inductive type.
Claim. The structure ModalPreferenceCert certifies that the seven Greek modes are pairwise distinct, with costRank(Ionian) = 0, costRank(Aeolian) = 1, costRank(Locrian) = 6, that Ionian and Aeolian occupy the two lowest ranks, and that Locrian is strictly highest in cost.
background
ModalPreferenceCert is defined in the Musicology track as a structure whose fields encode the J-cost ranking of the seven Greek modes (Ionian through Locrian) relative to a φ-rational reference scale. J-cost is the Recognition Science cost function applied to interval ratios; lower values predict higher cultural preference. The module states that this ranking reproduces the observed order: major (Ionian) and minor (Aeolian) most preferred, Locrian least preferred. Upstream results supply the supporting facts: NarrativeGeodesic.all_length and all_nodup establish that the mode list has length 7 and contains no duplicates; analogous length and nodup theorems appear in AsteroidOreSpectroscopy and KinshipGraphCohomology for parallel enumerations.
proof idea
The definition is a one-line record constructor. It sets modes_count to GreekMode.all_length, modes_distinct to GreekMode.all_nodup, and the six rank predicates directly to the corresponding GreekMode lemmas (ionian_lowest, aeolian_second, locrian_highest, ionian_aeolian_dominant, locrian_uniquely_worst). No further tactics or reductions are required.
why it matters
This definition supplies the concrete certification required by the musicology derivation in Track I10. It closes the gap between the abstract J-cost function and the enumerated Greek modes, confirming that the predicted preference order matches empirical survey data. The construction sits downstream of the φ-ladder and RCL identities; it is cited by any later result that needs a verified modal cost ordering. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.