pith. machine review for the scientific record. sign in
def definition def or abbrev

strictMusicRealization

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  38noncomputable def strictMusicRealization : StrictLogicRealization where
  39  Carrier := FrequencyRatio

proof body

Definition body.

  40  Cost := Nat
  41  zeroCost := inferInstance
  42  compare := ratioCost
  43  compose := fun a b => ⟨a.1 * b.1, mul_pos a.2 b.2⟩
  44  one := ⟨1, one_pos⟩
  45  generator := octave
  46  identity_law := ratioCost_self
  47  non_contradiction_law := ratioCost_symm
  48  excluded_middle_law := True
  49  composition_law := True
  50  invariance_law := True
  51  nontrivial_law := by
  52    have hne : octave ≠ (⟨1, one_pos⟩ : FrequencyRatio) := by
  53      intro h
  54      have hv := congrArg Subtype.val h
  55      norm_num [octave] at hv
  56    simp [ratioCost, hne]
  57

used by (8)

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

depends on (17)

Lean names referenced from this declaration's body.