canonicalScaleCount_eq
plain-language theorem explainer
The equality states that the number of canonical musical scale types equals five, as predicted by configDim D equal to five in the Recognition Science framework. Researchers working on cross-domain classifications would cite it to verify consistency with other five-element systems such as the phi-ladder note counts. The proof is a direct reflexivity step on the constant definition.
Claim. The number of canonical scale types equals five: $5$.
background
The Ethnomusicology module treats musical scales as another instance of the five-element classification forced by configDim D = 5. It lists the five types as pentatonic, diatonic, hexatonic, octatonic, and chromatic, with note counts following the phi-ladder (pentatonic as 5 = 3 + 2 Fibonacci, diatonic as 7 = 5 + 2, chromatic near phi^5 / 2). The upstream definition sets the count directly to the natural number five.
proof idea
The proof is a one-line term that applies reflexivity to the defining equation of the count.
why it matters
This supplies the scale_count component of the ScaleCountCert structure used downstream. It fills the structural prediction that five canonical types arise from configDim D = 5, matching the same template applied to other five-element systems in the forcing chain. The module doc states the falsifier as any survey finding fewer than five or more than seven types across at least fifty cultures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.