all_nodup
plain-language theorem explainer
The list of seven Greek modes is pairwise distinct. Musicologists modeling cross-cultural preferences from φ-rational J-costs cite this to establish a valid domain before ranking. The proof is a one-line decision procedure that verifies the enumerated list contains no duplicates.
Claim. The list of the seven Greek modes has no duplicate entries.
background
The ModalPreferenceFromPhi module enumerates the seven Greek modes (Ionian through Locrian) in a list and ranks them by J-cost relative to a φ-rational reference scale. Lower J-cost predicts higher cross-cultural preference, matching Huron 2006 data with Ionian and Aeolian at the top and Locrian at the bottom. Parallel nodup results appear in NarrativeGeodesic.all_nodup for the seven plot families and AsteroidOreSpectroscopy.all_nodup for the seven ore classes, each confirming that an enumerated collection of seven distinct objects is free of repetition.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the list definition of all modes.
why it matters
This theorem supplies the modes_distinct field inside modalPreferenceCert, which aggregates distinctness with the explicit cost ranks (ionian_lowest, aeolian_second, locrian_highest) to certify the full preference ordering. It completes the prerequisite that the mode set be well-defined before J-cost comparison, consistent with the Recognition Science pattern of using nodup lemmas to ground finite enumerations on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.