diatonic_eq_pentatonic_plus_two
plain-language theorem explainer
The equality shows the diatonic note count equals the pentatonic count plus two. Ethnomusicologists using Recognition Science cite it to confirm the Fibonacci progression of scale sizes forced by configDim D = 5. The proof is a one-line wrapper that unfolds the two constant definitions and reduces the resulting numerical statement.
Claim. Let $d$ be the diatonic note count and $p$ the pentatonic note count. Then $d = p + 2$.
background
The module derives canonical musical scale counts from the Recognition Science parameter configDim D = 5, which forces exactly five scale types across cultures: pentatonic, diatonic, hexatonic, octatonic, and chromatic. Note counts follow the phi-ladder, with pentatonic fixed at the Fibonacci number 5 and diatonic at the next Fibonacci number 7. The upstream definitions supply the concrete values: pentatonicCount is defined as 5 and diatonicCount as 7, with the latter explicitly documented as pentatonic plus two.
proof idea
The term proof unfolds the definitions of diatonicCount and pentatonicCount, then applies norm_num to discharge the resulting arithmetic equality 7 = 5 + 2.
why it matters
This equality supplies the diatonic_eq field of the ScaleCountCert record, which certifies the full set of canonical counts predicted by configDim D = 5. It closes one link in the phi-ladder chain that runs from pentatonic (5) through diatonic (7) to chromatic (12) and aligns with the eight-tick octave structure of the broader framework. The result is part of the structural theorem asserting five scale types with no remaining sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.