`pentatonicSize`

definition

show as: view math explainer →

module: IndisputableMonolith.Aesthetics.MusicalScale
domain: Aesthetics
line: 168 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Aesthetics.MusicalScale on GitHub at line 168.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 165/-! ## Pentatonic Connection -/
 166
 167/-- The pentatonic scale has 5 notes, related to φ. -/
 168def pentatonicSize : ℕ := 5
 169
 170/-- The diatonic scale has 7 notes. -/
 171def diatonicSize : ℕ := 7
 172
 173/-- 5 and 7 are consecutive Fibonacci numbers. -/
 174theorem pentatonic_diatonic_fib : pentatonicSize + diatonicSize = 12 := by native_decide
 175
 176/-- The Fibonacci-like structure: 5, 7, 12 -/
 177theorem scale_fibonacci : pentatonicSize + diatonicSize = semitonesPerOctave := by native_decide
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.