MusicTheory
MusicTheory modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
MusicTheory.CircleOfFifths |
10 | 0 | 3 | 96 | — |
MusicTheory.Consonance |
21 | 0 | 2 | 152 | — |
MusicTheory.CrossCulturalTonalUniversalsFromJCost |
0 | 0 | 1 | 37 | — |
MusicTheory.HarmonicModes |
24 | 0 | 15 | 156 | — |
MusicTheory.PitchPerceptionFromPhiLadder |
11 | 0 | 2 | 252 | — |
MusicTheory.Rhythm |
9 | 0 | 7 | 107 | — |
MusicTheory.TuningSystemJCostRanking |
6 | 0 | 4 | 100 | — |
MusicTheory.Valence |
14 | 0 | 4 | 132 | — |