diatonicSize
plain-language theorem explainer
The diatonic scale size is fixed at 7. Workers deriving Western scales from the golden ratio φ cite this constant to close the Fibonacci relation 5 + 7 = 12. The declaration is a direct constant assignment with no computational steps.
Claim. The diatonic scale contains exactly 7 notes.
background
The module derives the 12-tone equal-tempered scale from φ by optimizing consonance (simple ratios such as 2:1 and 3:2) and circle-of-fifths closure. Scale cardinalities 5 and 7 appear as consecutive Fibonacci numbers whose sum recovers the 12 semitones per octave. The upstream result supplies an explicit angular Lipschitz constant on the circle via a log-derivative bound, furnishing the analytic control needed for phase-lift arguments that justify the 12-step closure.
proof idea
Direct definition that assigns the constant 7 to the natural-number type.
why it matters
The definition supplies the second summand in pentatonic_diatonic_fib and scale_fibonacci, both of which assert 5 + 7 = 12. It therefore anchors the module's claim that 12 emerges from rounding φ^5/2 and that other scales (5, 7, 19, 31) inherit φ-related structure. The parent theorems close the Fibonacci-like pattern required by the Recognition Science treatment of musical aesthetics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.