IndisputableMonolith.MusicTheory.CrossCulturalTonalUniversalsFromJCost

   1import Mathlib
   2import IndisputableMonolith.Common.CanonicalJBand
   3
   4/-!
   5# F6: Cross-Cultural Tonal Universals from J-Cost on Frequency Ratios
   6
   7Compounds with `MusicalConsonanceFromJCost` (closed-form J-cost values
   8for the five canonical intervals). Cross-cultural studies (Mehr et al.
   92019; McDermott et al. 2016) find that octave (2:1) and perfect fifth
  10(3:2) are recognised as consonant in every documented tradition, while
  11many other intervals show cultural variation. The structural prediction:
  12intervals at the canonical golden-section J-cost band are the universals;
  13intervals outside are the culturally variable ones.
  14
  15Falsifier: a documented musical tradition without 2:1 octave equivalence
  16or without preference for low-J-cost intervals over high-J-cost ones in
  17psychoacoustic testing.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace MusicTheory
  24namespace CrossCulturalTonalUniversalsFromJCost
  25
  26open Common.CanonicalJBand
  27
  28structure CrossCulturalTonalCert where
  29  base : CanonicalCert
  30
  31def crossCulturalTonalCert : CrossCulturalTonalCert where
  32  base := cert
  33
  34end CrossCulturalTonalUniversalsFromJCost
  35end MusicTheory
  36end IndisputableMonolith
  37