all
plain-language theorem explainer
The definition supplies the exhaustive ordered list of the seven Greek modes for J-cost evaluation in the phi-rational musicology model. Researchers deriving cross-cultural modal preferences from Recognition Science constants would cite this enumeration when ranking interval ratios against the Ionian reference. The body is a direct constructor list drawn from the GreekMode inductive type.
Claim. Let $M$ be the inductive type whose constructors are the seven Greek modes (Ionian, Dorian, Phrygian, Lydian, Mixolydian, Aeolian, Locrian). Then $all = [Ionian, Aeolian, Mixolydian, Lydian, Dorian, Phrygian, Locrian]$.
background
The module treats modal preference as a J-cost ranking of interval ratios relative to a phi-rational reference scale. GreekMode is the inductive type whose seven constructors label the standard modes, with Ionian as major reference and Aeolian as minor. J-cost is the Recognition Science functional $J(x) = (x + x^{-1})/2 - 1$, applied here to mode intervals so that lower cost predicts higher preference.
proof idea
The definition is a direct list literal that enumerates the seven constructors of GreekMode in the stated order. No lemmas or tactics are invoked; the body simply assembles the complete collection.
why it matters
This supplies the domain enumeration required for the musicology track (I10 of Plan v5) that derives modal rankings matching Huron 2006 data. It supports downstream convexity results such as actionJ_convex_on_interp and geodesic_minimizes_unconditional by providing the mode list for cost comparisons. The construction parallels upstream enumerations such as NarrativeGeodesic.all (seven plot families) and KinshipGraphCohomology.all (eight kinship systems), reinforcing the pattern of complete domain lists in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.