pith. machine review for the scientific record. sign in
theorem proved term proof high

scale_fibonacci

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 177theorem scale_fibonacci : pentatonicSize + diatonicSize = semitonesPerOctave := by native_decide

proof body

Term-mode proof.

 178
 179/-! ## Falsification Criteria
 180
 181The musical scale derivation is falsifiable:
 182
 1831. **12 not optimal**: If a different number gives better consonance/closure
 184
 1852. **φ connection spurious**: If φ^5 ≈ 11 is coincidental
 186
 1873. **Circle of fifths**: If (3/2)^n ≠ 2^m for any small n, m
 188-/
 189
 190end
 191
 192end MusicalScale
 193end Aesthetics
 194end IndisputableMonolith

depends on (15)

Lean names referenced from this declaration's body.