pentatonic_diatonic_fib
plain-language theorem explainer
The declaration establishes that the pentatonic scale cardinality of five plus the diatonic scale cardinality of seven equals twelve, matching consecutive Fibonacci numbers in the phi-derived musical construction. Researchers deriving the twelve-tone octave from golden-ratio optimization would cite this identity when linking scale sizes to the circle-of-fifths closure. The proof reduces to direct numerical evaluation of the two constant definitions.
Claim. Let $P = 5$ be the cardinality of the pentatonic scale and $D = 7$ the cardinality of the diatonic scale. Then $P + D = 12$.
background
The module derives the Western twelve-tone scale from the golden ratio through optimal frequency ratios and closure under fifths. PentatonicSize is defined as the constant 5, noted as related to phi. DiatonicSize is defined as the constant 7, described as the number of notes in the diatonic scale. The module documentation states that 12 emerges from phi-scaling as round(phi^5 / 2) and that the circle of fifths closes after twelve steps with (3/2)^12 approximately 2^7.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic sum of the two constant definitions.
why it matters
This identity supplies the Fibonacci-like step 5 + 7 = 12 that supports the module's claim of twelve semitones arising from phi optimization. It connects directly to the module's predictions on scale sizes having phi-related structure and to the forcing-chain landmark of the eight-tick octave by realizing a period-12 division. No downstream theorems are listed, leaving open how the identity integrates with the Recognition Composition Law for frequency ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.