IndisputableMonolith.MusicTheory.CircleOfFifths

   1/-
   2  MusicTheory/CircleOfFifths.lean
   3
   4  THE 12/8 = 3/2 BRIDGE
   5
   6  Musical pitch space has 12 semitones per octave. The RS DFT-8 has 8
   7  modes per cycle. The ratio 12/8 = 3/2 IS the perfect fifth — the
   8  most consonant non-trivial interval. Both structures are forced by
   9  the same cost function.
  10
  11  The circle of fifths arises because 7 perfect fifths almost span
  12  12 semitones: (3/2)^7 ≈ 2^(12/2) = 2^6... more precisely,
  13  log₂(3/2) ≈ 7/12, making 12 the best small-integer approximation.
  14
  15  Part of: IndisputableMonolith/MusicTheory/
  16-/
  17
  18import Mathlib
  19import IndisputableMonolith.MusicTheory.HarmonicModes
  20
  21namespace IndisputableMonolith.MusicTheory.CircleOfFifths
  22
  23/-! ## Core Constants -/
  24
  25@[simp] def semitonesPerOctave : ℕ := 12
  26@[simp] def rsModesPerOctave : ℕ := 8
  27@[simp] noncomputable def fifth : ℝ := 3 / 2
  28
  29/-! ## The 12/8 = 3/2 Bridge
  30
  31This is the central insight: the ratio of musical semitones (12) to
  32RS modes (8) IS the perfect fifth. -/
  33
  34theorem twelve_eight_ratio_is_fifth :
  35    (semitonesPerOctave : ℝ) / rsModesPerOctave = fifth := by
  36  simp; norm_num
  37
  38theorem semitones_eq_12 : semitonesPerOctave = 12 := rfl
  39theorem modes_eq_8 : rsModesPerOctave = 8 := rfl
  40
  41/-! ## Pythagorean Comma
  42
  43The Pythagorean comma is the small discrepancy between 12 perfect fifths
  44and 7 octaves: (3/2)^12 / 2^7 > 1. This is why equal temperament
  45exists — it distributes this comma evenly across all 12 semitones. -/
  46
  47theorem pythagorean_comma_positive :
  48    (3 / 2 : ℝ) ^ 12 / 2 ^ 7 > 1 := by
  49  norm_num
  50
  51theorem pythagorean_comma_small :
  52    (3 / 2 : ℝ) ^ 12 / 2 ^ 7 < 1.02 := by
  53  norm_num
  54
  55/-! ## Seven Fifths ≈ Four Octaves
  56
  57The best rational approximation to log₂(3/2) with denominator ≤ 12
  58is 7/12. This means 7 fifths nearly span 4 octaves (= 12 semitones).
  59We prove the concrete version: (3/2)^7 is close to 2^(7·7/12). -/
  60
  61theorem seven_fifths_close_to_four_octaves :
  62    (3 / 2 : ℝ) ^ 7 > 11 ∧ (3 / 2 : ℝ) ^ 7 < 18 := by
  63  constructor <;> norm_num
  64
  65theorem twelve_fifths_overshoot :
  66    (3 / 2 : ℝ) ^ 12 > 2 ^ 7 := by
  67  norm_num
  68
  69/-! ## Fifth Is Simplest Non-Trivial Consonance
  70
  71Among all superparticular ratios (n+1)/n with n ≥ 2,
  72the fifth (3/2, n=2) has the smallest J-cost. The octave (2/1, n=1)
  73is simpler but trivial (mere repetition). -/
  74
  75theorem fifth_cost_lt_octave_cost :
  76    Cost.Jcost HarmonicModes.fifth < Cost.Jcost HarmonicModes.octave := by
  77  rw [HarmonicModes.fifth_jcost, HarmonicModes.octave_jcost]; norm_num
  78
  79/-! ## Chromatic Scale from φ
  80
  81The continued fraction expansion of log₂(3/2) begins
  82[0; 1, 1, 2, 2, 3, 1, ...]. The denominators of the convergents are
  831, 2, 5, 12, 29, 41, ... The first "good" approximation with
  84manageable denominator is 7/12, which is why Western music settled
  85on 12 semitones. The appearance of Fibonacci-like numbers in the
  86convergents connects this to φ. -/
  87
  88theorem twelve_divides_lcm_structure :
  89    Nat.lcm 3 4 = 12 := by native_decide
  90
  91theorem fifth_fourth_product :
  92    fifth * HarmonicModes.fourth = HarmonicModes.octave := by
  93  simp [HarmonicModes.fourth, HarmonicModes.octave]; ring
  94
  95end IndisputableMonolith.MusicTheory.CircleOfFifths
  96