`tetStep_jcost_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.MusicTheory.TuningSystemJCostRanking
domain: MusicTheory
line: 75 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.MusicTheory.TuningSystemJCostRanking on GitHub at line 75.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

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