scale_fibonacci
plain-language theorem explainer
The pentatonic scale size plus the diatonic scale size equals the semitone count per octave, confirming the 5 + 7 = 12 Fibonacci relation in the 12-tone system. Researchers deriving musical scales from the golden ratio in Recognition Science would cite this identity to link scale structure to phi-ladder arithmetic. The proof is a one-line native computation that evaluates the three constant definitions directly.
Claim. The pentatonic scale size (5 notes) plus the diatonic scale size (7 notes) equals the number of semitones per octave (12).
background
The module derives the Western 12-tone equal temperament scale from the golden ratio phi by optimizing consonance and closure under frequency ratios. PentatonicSize is defined as the constant 5, diatonicSize as the constant 7, and semitonesPerOctave as the constant 12. These sizes are presented as consecutive Fibonacci numbers whose sum recovers the octave division, consistent with the module observation that 12 emerges from rounding phi^5 / 2 and that the circle of fifths closes after 12 steps with (3/2)^12 approximately 2^7.
proof idea
The proof is a one-line wrapper that applies native_decide to the three constant definitions. Native_decide evaluates the arithmetic equality 5 + 7 = 12 by direct computation without further lemmas.
why it matters
This identity anchors the Fibonacci-like structure 5, 7, 12 inside the phi-derived musical scale construction. It supports the module claim that 12 semitones arise from phi^5 scaling and optimal frequency ratios, placing the result within the Recognition Science aesthetics framework that connects phi-ladder arithmetic to observable harmonic structure. No downstream uses are recorded, so the declaration functions as a local consistency check rather than a lemma for further theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.