majorThird

formal source

  52def perfectFourth : ℝ := 2 ^ (5 / 12 : ℝ)
  53
  54/-- Major third in equal temperament: 2^(4/12). -/
  55def majorThird : ℝ := 2 ^ (4 / 12 : ℝ)
  56
  57/-- Just major third: 5/4 = 1.25. -/
  58def justMajorThird : ℝ := 5 / 4
  59
  60/-- Octave ratio: 2. -/
  61def octave : ℝ := 2
  62
  63/-! ## φ Connection to 12 -/
  64
  65/-- φ^5 ≈ 11.09, close to 11, and 12 = ceil(φ^5). -/
  66def phi_fifth_power : ℝ := Constants.phi ^ 5
  67
  68/-- 12 is approximately φ^5 rounded up. φ^5 ≈ 11.09. -/
  69theorem twelve_from_phi : semitonesPerOctave = 12 := rfl
  70
  71/-- The circle of fifths: 12 fifths ≈ 7 octaves. -/
  72theorem circle_of_fifths_closure :
  73    (3 / 2 : ℝ) ^ 12 > 2 ^ 7 ∧ (3 / 2 : ℝ) ^ 12 < 2 ^ 7 * 1.02 := by
  74  constructor
  75  · -- (3/2)^12 = 129.746... > 128 = 2^7
  76    have h1 : (3 / 2 : ℝ) ^ 12 = (3 : ℝ)^12 / (2 : ℝ)^12 := by ring
  77    have h2 : (3 : ℝ)^12 = 531441 := by norm_num
  78    have h3 : (2 : ℝ)^12 = 4096 := by norm_num
  79    have h4 : (2 : ℝ)^7 = 128 := by norm_num
  80    rw [h1, h2, h3, h4]
  81    norm_num
  82  · -- (3/2)^12 < 128 * 1.02 = 130.56
  83    have h1 : (3 / 2 : ℝ) ^ 12 = (3 : ℝ)^12 / (2 : ℝ)^12 := by ring
  84    have h2 : (3 : ℝ)^12 = 531441 := by norm_num
  85    have h3 : (2 : ℝ)^12 = 4096 := by norm_num