  37noncomputable section
  38
  39/-- Number of semitones in an octave. -/
  40def semitonesPerOctave : ℕ := 12
  41
  42/-- Semitone frequency ratio: 2^(1/12). -/
  43def semitoneRatio : ℝ := 2 ^ (1 / 12 : ℝ)
  44
  45/-- Perfect fifth frequency ratio in equal temperament: 2^(7/12). -/
  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

papers checked against this theorem

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