def
definition
perfectFifth
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Aesthetics.MusicalScale on GitHub at line 46.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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