`diatonicCount`

definition

show as: view math explainer →

module: IndisputableMonolith.Ethnomusicology.ScaleCountFromConfigDim
domain: Ethnomusicology
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethnomusicology.ScaleCountFromConfigDim on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  42def pentatonicCount : ℕ := 5
  43
  44/-- Diatonic note count: 7 = pentatonic + 2. -/
  45def diatonicCount : ℕ := 7
  46
  47theorem diatonic_eq_pentatonic_plus_two : diatonicCount = pentatonicCount + 2 := by
  48  unfold diatonicCount pentatonicCount; norm_num
  49
  50/-- Chromatic count: 12. -/
  51def chromaticCount : ℕ := 12
  52
  53theorem chromatic_pos : 0 < chromaticCount := by
  54  unfold chromaticCount; norm_num
  55
  56structure ScaleCountCert where
  57  scale_count : canonicalScaleCount = 5
  58  diatonic_eq : diatonicCount = pentatonicCount + 2
  59  chromatic_pos : 0 < chromaticCount
  60
  61noncomputable def cert : ScaleCountCert where
  62  scale_count := canonicalScaleCount_eq
  63  diatonic_eq := diatonic_eq_pentatonic_plus_two
  64  chromatic_pos := chromatic_pos
  65
  66theorem cert_inhabited : Nonempty ScaleCountCert := ⟨cert⟩
  67
  68end
  69end ScaleCountFromConfigDim
  70end Ethnomusicology
  71end IndisputableMonolith

papers checked against this theorem

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