ModalPreferenceCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the J-cost function or the phi-ladder.
- Does not perform statistical analysis of survey data.
- Does not address non-Greek modal systems.
- Does not claim uniqueness of the ranking outside the seven modes.
formal statement (Lean)
118structure ModalPreferenceCert where
119 modes_count : GreekMode.all.length = 7
120 modes_distinct : GreekMode.all.Nodup
121 ionian_lowest : GreekMode.costRank .Ionian = 0
122 aeolian_second : GreekMode.costRank .Aeolian = 1
123 locrian_highest : GreekMode.costRank .Locrian = 6
124 ionian_aeolian_dominant :
125 GreekMode.costRank .Ionian ≤ 1 ∧ GreekMode.costRank .Aeolian ≤ 1
126 locrian_uniquely_worst :
127 ∀ m : GreekMode, m ≠ .Locrian → GreekMode.costRank m < GreekMode.costRank .Locrian
128