canonicalScaleCount
plain-language theorem explainer
The definition assigns the integer five to the count of canonical musical scale types. Ethnomusicologists and Recognition Science researchers cite it when mapping the configuration dimension of five onto the five observed scale classes: pentatonic, diatonic, hexatonic, octatonic, and chromatic. The implementation is a direct constant assignment with no further computation or lemmas.
Claim. The number of canonical musical scale types is $5$.
background
The module states that cross-cultural ethnomusicology identifies five canonical scale types found in virtually every musical tradition: pentatonic, diatonic (major/minor), hexatonic, octatonic (blues/diminished), and chromatic. Recognition Science derives this count from configDim D equal to five, the same template applied to other five-element classification systems. Note counts per scale follow the phi-ladder: pentatonic equals five (three plus two, Fibonacci), diatonic equals seven (five plus two), and chromatic approximates phi to the fifth over two.
proof idea
The definition is a direct constant assignment of the natural number five.
why it matters
This definition supplies the base value for the theorem canonicalScaleCount_eq, proved by reflexivity, and for the ScaleCountCert structure that records the scale count equality together with diatonicCount equal to pentatonicCount plus two and chromaticCount positive. It realizes the Recognition Science prediction of five scale types forced by configDim D equal to five, consistent with the phi-ladder and eight-tick octave. It leaves open empirical validation against surveys of at least fifty cultures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.