theorem proved term proof

`tetStep_jcost_pos`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  75theorem tetStep_jcost_pos : 0 < stepCost tetStep := by

proof body

Term-mode proof.

  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). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

ji_beats_tet in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use
tuningRankingCert in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use

depends on (11)

Lean names referenced from this declaration's body.

Jcost_pos_of_ne_one in IndisputableMonolith.Cost decl_use
Jcost_pos_of_ne_one in IndisputableMonolith.Cost.JcostCore decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
beats in IndisputableMonolith.Gap45 decl_use
beats in IndisputableMonolith.Gap45.Beat decl_use
Jcost_pos_of_ne_one in IndisputableMonolith.Information.LocalCache decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
stepCost in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use
tetStep in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use
tetStep_band in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use