ModalPreferenceCert
plain-language theorem explainer
The ModalPreferenceCert structure bundles seven properties that certify the J-cost ranking of the seven Greek modes. Musicologists and Recognition Science researchers cite it to connect cross-cultural modal preferences to the underlying phi-rational cost function. It is assembled directly from the preceding length, nodup, and costRank lemmas without additional proof steps.
Claim. Let $M$ be the set of seven Greek modes. The structure asserts $|M|=7$, the modes are pairwise distinct, the cost function $c:M→ℕ$ satisfies $c(Ionian)=0$, $c(Aeolian)=1$, $c(Locrian)=6$, $c(Ionian)≤1∧c(Aeolian)≤1$, and $∀m∈M$, $m≠Locrian$ implies $c(m)<c(Locrian)$.
background
GreekMode is the inductive type enumerating the seven modes Ionian, Dorian, Phrygian, Lydian, Mixolydian, Aeolian, Locrian. costRank is the function that assigns each mode its integer rank under the J-cost relative to the Ionian reference, with explicit values 0 through 6. The module models cross-cultural modal preference as the ordering induced by this J-cost on φ-rational interval ratios, matching the ranking reported in Huron 2006. Upstream results supply the pattern of 7-element lists (NarrativeGeodesic.all, KinshipGraphCohomology.all, AsteroidOreSpectroscopy.all) and the concrete costRank values via aeolian_second and ionian_lowest.
proof idea
This is a structure definition that directly packages the results of the sibling declarations all_length, all_nodup, ionian_lowest, aeolian_second, locrian_highest, and the two inequality lemmas. No tactics or reductions are performed inside the structure itself.
why it matters
ModalPreferenceCert is instantiated by modalPreferenceCert and functions as the master certificate for Track I10. It records that the observed preference ordering (Ionian and Aeolian lowest, Locrian highest) follows from the J-cost on the phi-ladder, consistent with the Recognition Composition Law. The construction closes the derivation step that links the eight-tick octave and D=3 geometry to musical interval preferences. It leaves open the extension to non-diatonic or non-Western scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.