twelve_from_phi

formal source

  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
  86    have h4 : (2 : ℝ)^7 = 128 := by norm_num
  87    rw [h1, h2, h3, h4]
  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