Aesthetics
Aesthetics modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
Aesthetics.BerlyneInvertedU |
4 | 0 | 3 | 80 | — |
Aesthetics.CulturalAestheticFromJCost |
4 | 0 | 2 | 70 | — |
Aesthetics.MusicalScale |
7 | 0 | 12 | 195 | — |
Aesthetics.NarrativeGeodesic |
20 | 0 | 6 | 390 | — |
Aesthetics.NarrativeStructureFromF2Cube |
4 | 0 | 3 | 69 | — |
Aesthetics.SymmetryGroupPreference |
17 | 0 | 6 | 346 | — |
Aesthetics.VisualBeauty |
5 | 0 | 3 | 179 | — |