  46def perfectFifth : ℝ := 2 ^ (7 / 12 : ℝ)
  47
  48/-- Just perfect fifth: 3/2 = 1.5. -/
  49def justFifth : ℝ := 3 / 2
  50
  51/-- Perfect fourth frequency ratio: 2^(5/12). -/
  52def perfectFourth : ℝ := 2 ^ (5 / 12 : ℝ)
  53
  54/-- Major third in equal temperament: 2^(4/12). -/
  55def majorThird : ℝ := 2 ^ (4 / 12 : ℝ)
  56
  57/-- Just major third: 5/4 = 1.25. -/
  58def justMajorThird : ℝ := 5 / 4
  59
  60/-- Octave ratio: 2. -/
  61def octave : ℝ := 2
  62
  63/-! ## φ Connection to 12 -/
  64
  65/-- φ^5 ≈ 11.09, close to 11, and 12 = ceil(φ^5). -/
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.