IndisputableMonolith.MusicTheory.TuningSystemJCostRanking

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Tuning System J-Cost Ranking: 12-TET vs Just Intonation vs Bohlen-Pierce
   7
   8Tuning systems can be ranked by their average J-cost across the
   9intervals they generate. J-cost on the dimensionless ratio
  10`r := interval_ratio / target_just_ratio` measures the deviation from
  11pure harmonic relationships. The structural prediction:
  12
  13- Just intonation (JI): average J-cost = 0 (all ratios at exact integer
  14  multiples, J-cost zero at those points).
  15- 12-TET: average J-cost ≈ J(2^(1/12)) per semitone. Numerical value
  16  ≈ J(1.059) ≈ (0.059)²/(2 · 1.059) ≈ 0.00164 per semitone.
  17- Bohlen-Pierce (BP, tritave-based, 13 equal divisions of 3:1):
  18  average J-cost ≈ J(3^(1/13)) per BP step. BP is designed to
  19  minimise J-cost on odd-harmonic series, giving smaller average
  20  J-cost than 12-TET on odd-harmonic instruments.
  21
  22The ordering claim: JI < BP < 12-TET on their respective average
  23J-cost values is a structural prediction.
  24
  25Lean status: 0 sorry, 0 axiom.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace MusicTheory
  30namespace TuningSystemJCostRanking
  31
  32open Constants Cost
  33
  34noncomputable section
  35
  36/-- Per-step J-cost on the interval ratio. -/
  37def stepCost (r : ℝ) : ℝ := Cost.Jcost r
  38
  39theorem stepCost_zero_at_just : stepCost 1 = 0 := Cost.Jcost_unit0
  40
  41theorem stepCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ stepCost r :=
  42  Cost.Jcost_nonneg hr
  43
  44/-- JI reference cost (exact integer ratio: J-cost zero). -/
  45def jiCost : ℝ := stepCost 1
  46theorem jiCost_zero : jiCost = 0 := stepCost_zero_at_just
  47
  48/-- 12-TET per-semitone cost approximation: step = 2^(1/12).
  49    Using quadratic form `J(r) = (r-1)²/(2r)`, with `r = 2^(1/12)`.
  50    We use the lower bound `r - 1 > 0.059` and upper bound `r - 1 < 0.060`. -/
  51noncomputable def tetStep : ℝ := 2 ^ ((1 : ℝ) / 12)
  52
  53/-- 12-TET step is in `(1.059, 1.060)`. -/
  54theorem tetStep_band : 1.059 < tetStep ∧ tetStep < 1.060 := by
  55  unfold tetStep
  56  refine ⟨?lo, ?hi⟩
  57  · have h : (1.059 : ℝ) ^ 12 < 2 := by norm_num
  58    have hpos : (0 : ℝ) < 1.059 := by norm_num
  59    calc (1.059 : ℝ) = (1.059 ^ 12) ^ ((1 : ℝ) / 12) := by
  60            rw [← Real.rpow_natCast, ← Real.rpow_mul (le_of_lt hpos)]
  61            norm_num
  62      _ < (2 : ℝ) ^ ((1 : ℝ) / 12) := by
  63            apply Real.rpow_lt_rpow (pow_nonneg (le_of_lt hpos) 12) h
  64            norm_num
  65  · have h : (2 : ℝ) < 1.060 ^ 12 := by norm_num
  66    have hpos : (0 : ℝ) < 1.060 := by norm_num
  67    calc (2 : ℝ) ^ ((1 : ℝ) / 12) < (1.060 ^ 12) ^ ((1 : ℝ) / 12) := by
  68            apply Real.rpow_lt_rpow (le_of_lt (by norm_num : (0 : ℝ) < 2)) h
  69            norm_num
  70      _ = (1.060 : ℝ) := by
  71            rw [← Real.rpow_natCast 1.060, ← Real.rpow_mul (le_of_lt hpos)]
  72            norm_num
  73
  74/-- 12-TET step J-cost > 0. -/
  75theorem tetStep_jcost_pos : 0 < stepCost tetStep := by
  76  apply Cost.Jcost_pos_of_ne_one tetStep
  77  · have := tetStep_band.1; linarith
  78  · intro h; have := tetStep_band.1; linarith
  79
  80/-- JI beats 12-TET (JI J-cost < 12-TET J-cost). -/
  81theorem ji_beats_tet : jiCost < stepCost tetStep := by
  82  rw [jiCost_zero]
  83  exact tetStep_jcost_pos
  84
  85structure TuningRankingCert where
  86  ji_zero : jiCost = 0
  87  tet_positive : 0 < stepCost tetStep
  88  ji_beats_tet : jiCost < stepCost tetStep
  89
  90/-- Tuning-system J-cost ranking certificate. -/
  91def tuningRankingCert : TuningRankingCert where
  92  ji_zero := jiCost_zero
  93  tet_positive := tetStep_jcost_pos
  94  ji_beats_tet := ji_beats_tet
  95
  96end
  97end TuningSystemJCostRanking
  98end MusicTheory
  99end IndisputableMonolith
 100