GreekMode
plain-language theorem explainer
GreekMode enumerates the seven classical Greek modes as an inductive type with constructors Ionian through Locrian. Music theorists and empirical psychologists cite it when mapping J-cost rankings of diatonic intervals to cross-cultural preference surveys. The definition is a direct inductive construction that supplies the domain for all subsequent cost assignments and uniqueness theorems in the module.
Claim. The Greek modes form the finite set consisting of the seven elements Ionian (major), Dorian, Phrygian, Lydian, Mixolydian, Aeolian (minor), and Locrian.
background
Recognition Science ranks musical intervals by J-cost, the function satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) with J(x) = (x + x^{-1})/2 - 1. The module derives modal preferences from φ-rational interval ratios referenced to the major scale. GreekMode supplies the exhaustive enumeration of the seven diatonic modes required for cost-rank assignment. Upstream, the Cost abbreviation from RSNative.Core provides the quantity type, while PreTemporalForcingOrder.rank supplies the numerical ordering convention used in the costRank definition.
proof idea
The declaration is an inductive definition introducing one constructor per mode, followed by automatic derivation of DecidableEq and Repr. No lemmas or tactics are invoked beyond the standard inductive construction.
why it matters
GreekMode is the domain for the ModalPreferenceCert structure and the musicology_one_statement theorem, which certify Ionian and Aeolian as the two lowest cost ranks and Locrian as uniquely highest. It realizes the empirical prediction of the Modal Preference from φ-Rational Intervals track, connecting J-uniqueness (T5) and the eight-tick octave (T7) to observable preferences. The module falsifier is a cross-cultural survey (n > 1000) showing best-modal preference outside the predicted Ionian-Aeolian cluster.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.