fifth_quality

proof body

Tactic-mode proof.

 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]
 122        _ = (128 : ℝ) ^ ((1 : ℝ) / 12) := by norm_num
 123    have step2 : (3 / 2 : ℝ) = ((3 / 2 : ℝ) ^ (12 : ℕ)) ^ ((1 : ℝ) / 12) := by
 124      rw [← h_inv_eq]
 125      exact (Real.pow_rpow_inv_natCast h32 (by norm_num : (12 : ℕ) ≠ 0)).symm
 126    rw [step1, step2]
 127    apply Real.rpow_lt_rpow (by norm_num) h hp
 128  have h_lower : (2 : ℝ) ^ ((7 : ℝ) / 12) > 1.497 := by
 129    have h : (1.497 : ℝ) ^ (12 : ℕ) < 128 := by norm_num
 130    have hp : (0 : ℝ) < 1 / 12 := by norm_num
 131    have h2 : (0 : ℝ) ≤ 2 := by norm_num
 132    have h1497 : (0 : ℝ) ≤ 1.497 := by norm_num
 133    have h_inv_eq : ((12 : ℕ) : ℝ)⁻¹ = 1 / 12 := by norm_num
 134    have step1 : (1.497 : ℝ) = ((1.497 : ℝ) ^ (12 : ℕ)) ^ ((1 : ℝ) / 12) := by
 135      rw [← h_inv_eq]
 136      exact (Real.pow_rpow_inv_natCast h1497 (by norm_num : (12 : ℕ) ≠ 0)).symm
 137    have step2 : (2 : ℝ) ^ ((7 : ℝ) / 12) = (128 : ℝ) ^ ((1 : ℝ) / 12) := by
 138      calc (2 : ℝ) ^ ((7 : ℝ) / 12)
 139        _ = (2 : ℝ) ^ ((7 : ℝ) * (1 / 12)) := by ring_nf
 140        _ = ((2 : ℝ) ^ (7 : ℝ)) ^ (1 / 12 : ℝ) := by rw [Real.rpow_mul h2]
 141        _ = (128 : ℝ) ^ ((1 : ℝ) / 12) := by norm_num
 142    rw [step1, step2]
 143    exact Real.rpow_lt_rpow (by positivity) h hp
 144  rw [abs_lt]
 145  constructor <;> linarith
 146
 147/-- The major third in 12-TET is about 14 cents sharp. -/