musicology_one_statement
plain-language theorem explainer
The theorem asserts that the seven Greek modes are distinct under the J-cost metric, with Ionian assigned rank 0, Aeolian rank 1, and Locrian uniquely rank 6. Music cognition researchers or cross-cultural aesthetic theorists would cite the result when connecting modal preference orderings to phi-rational interval costs. The proof is a term-mode conjunction that directly assembles the length lemma, three reflexivity equalities, and the dedicated uniqueness lemma for Locrian.
Claim. The inductive type of Greek modes has seven elements. The cost function on modes satisfies cost(Ionian) = 0, cost(Aeolian) = 1, cost(Locrian) = 6, and for every mode m distinct from Locrian one has cost(m) < cost(Locrian).
background
GreekMode is the inductive enumeration of the seven traditional modes (Ionian through Locrian). The costRank function returns the integer J-cost of each mode's interval ratios relative to the phi-rational reference scale; lower values indicate lower cost and therefore higher predicted preference. J itself is the Recognition Science cost J(x) = (x + x^{-1})/2 - 1. The module situates the claim as Track I10 of Plan v5, where modal preference is derived from J-cost ranking and is asserted to reproduce the ordering reported in Huron 2006.
proof idea
The proof is a term-mode conjunction. It supplies GreekMode.all_length to witness the cardinality seven, uses rfl for the three explicit rank equations, and applies the lemma locrian_uniquely_worst to discharge the universal strict inequality.
why it matters
The declaration supplies a compact, citable endpoint for the musicology derivation inside the Recognition framework. It confirms that J-cost ranks the seven modes exactly as required by the phi-rational model, with Ionian and Aeolian lowest and Locrian highest. The construction follows the recurring seven-element pattern seen in NarrativeGeodesic.all_length (seven plot families) and AsteroidOreSpectroscopy.all_length (seven ore classes). The module falsifier is a large cross-cultural survey (n > 1000, >5 cultures) that would place best-modal preference outside the predicted Ionian-Aeolian cluster.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.