third_quality

proof body

Tactic-mode proof.

 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 φ. -/