third_quality

formal source

 145  constructor <;> linarith
 146
 147/-- The major third in 12-TET is about 14 cents sharp. -/
 148theorem third_quality : majorThird > justMajorThird := by
 149  -- 2^(4/12) = 2^(1/3) ≈ 1.2599 > 1.25 = 5/4
 150  -- Prove: 2^(1/3) > 5/4 ⟺ 2 > (5/4)^3 = 125/64 = 1.953125
 151  simp only [majorThird, justMajorThird]
 152  have h_exp : (4 : ℝ) / 12 = 1 / 3 := by norm_num
 153  rw [h_exp]
 154  have h_cube : (5 / 4 : ℝ) ^ (3 : ℕ) < 2 := by norm_num
 155  have h_pos_54 : (0 : ℝ) ≤ 5 / 4 := by norm_num
 156  have hp : (0 : ℝ) < 1 / 3 := by norm_num
 157  -- (5/4) = ((5/4)^3)^(1/3) using Real.pow_rpow_inv_natCast
 158  have h_identity : (5 / 4 : ℝ) = ((5 / 4 : ℝ) ^ (3 : ℕ)) ^ ((3 : ℕ)⁻¹ : ℝ) :=
 159    (Real.pow_rpow_inv_natCast h_pos_54 (by norm_num : (3 : ℕ) ≠ 0)).symm
 160  have h_inv_eq : ((3 : ℕ)⁻¹ : ℝ) = 1 / 3 := by norm_num
 161  rw [h_inv_eq] at h_identity
 162  rw [h_identity]
 163  apply Real.rpow_lt_rpow (by positivity) h_cube hp
 164
 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