pythagoreanComma

formal source

  88    norm_num
  89
  90/-- The Pythagorean comma: (3/2)^12 / 2^7 ≈ 1.0136. -/
  91def pythagoreanComma : ℝ := (3 / 2) ^ 12 / 2 ^ 7
  92
  93/-- The Pythagorean comma is small (< 2%). -/
  94theorem comma_small : pythagoreanComma < 1.02 := by
  95  simp only [pythagoreanComma]
  96  have h1 : (3 / 2 : ℝ) ^ 12 = 531441 / 4096 := by norm_num
  97  have h2 : (2 : ℝ) ^ 7 = 128 := by norm_num
  98  rw [h1, h2]
  99  norm_num
 100
 101/-! ## Interval Quality Theorems -/
 102
 103/-- The fifth in 12-TET is within 0.2% of just (less than 2 cents). -/
 104theorem fifth_quality : |perfectFifth - justFifth| < 0.003 := by
 105  -- 2^(7/12) ≈ 1.4983, 3/2 = 1.5
 106  -- |1.4983 - 1.5| ≈ 0.0017 < 0.003
 107  -- This is verified by numerical computation; proof uses interval bounds
 108  simp only [perfectFifth, justFifth]
 109  -- Use native_decide with numerical bounds
 110  -- perfectFifth = 2^(7/12), justFifth = 3/2
 111  -- We prove bounds via: 1.497 < 2^(7/12) < 1.5
 112  have h_upper : (2 : ℝ) ^ ((7 : ℝ) / 12) < 3 / 2 := by
 113    have h : (128 : ℝ) < (3 / 2 : ℝ) ^ (12 : ℕ) := by norm_num
 114    have hp : (0 : ℝ) < 1 / 12 := by norm_num
 115    have h2 : (0 : ℝ) ≤ 2 := by norm_num
 116    have h32 : (0 : ℝ) ≤ 3 / 2 := by norm_num
 117    have h_inv_eq : ((12 : ℕ) : ℝ)⁻¹ = 1 / 12 := by norm_num
 118    have step1 : (2 : ℝ) ^ ((7 : ℝ) / 12) = (128 : ℝ) ^ ((1 : ℝ) / 12) := by
 119      calc (2 : ℝ) ^ ((7 : ℝ) / 12)
 120        _ = (2 : ℝ) ^ ((7 : ℝ) * (1 / 12)) := by ring_nf
 121        _ = ((2 : ℝ) ^ (7 : ℝ)) ^ (1 / 12 : ℝ) := by rw [Real.rpow_mul h2]