diatonicCount
plain-language theorem explainer
DiatonicCount fixes the note count of the diatonic scale at the integer 7. Researchers verifying the phi-ladder predictions for canonical scales in cross-cultural ethnomusicology cite this constant when checking the Fibonacci relation to the pentatonic count. The definition is a direct constant assignment requiring no further reduction.
Claim. The diatonic scale contains exactly seven notes, satisfying $7 = 5 + 2$ where the pentatonic count is 5.
background
The module establishes that five canonical scale types are forced by configDim D = 5, matching the template for other five-element classifications in Recognition Science. Scale lengths follow the phi-ladder: pentatonic count equals 5 (Fibonacci 3 + 2) and diatonic count equals 7 (Fibonacci 5 + 2). Chromatic count is placed near phi^5 / 2. The local setting treats these counts as structural consequences of the same forcing chain that yields D = 3 spatial dimensions and the eight-tick octave.
proof idea
Direct definition that assigns the constant 7 to diatonicCount. The sibling theorem diatonic_eq_pentatonic_plus_two unfolds both counts and applies norm_num to obtain the equality.
why it matters
This definition supplies the numerical value required by the ScaleCountCert structure, which certifies five canonical scales together with the relation diatonicCount = pentatonicCount + 2. It implements the phi-ladder step for the ethnomusicology classification forced by configDim = 5. The parent theorem diatonic_eq_pentatonic_plus_two depends on it to close the Fibonacci relation 7 = 5 + 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.