Acoustics
Acoustics modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
Acoustics.Harmonic_Distortion_RS |
4 | 0 | 3 | 36 | - |
Acoustics.Human_Voice_Range_RS |
4 | 0 | 3 | 36 | - |
Acoustics.Middle_C_Frequency_RS |
4 | 0 | 3 | 36 | - |
Acoustics.MusicConsonanceFromJCost |
4 | 0 | 3 | 47 | - |
Acoustics.MusicPitchJNDFromJCost |
5 | 0 | 3 | 87 | - |
Acoustics.Musical_Note_A4_Exact_RS |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_001 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_002 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_003 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_004 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_005 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_006 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_007 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_008 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_009 |
4 | 0 | 3 | 36 | - |
Acoustics.RS_ACS_Cert_010 |
4 | 0 | 3 | 36 | - |
Acoustics.RoomAcousticsFromPhiLadder |
3 | 0 | 2 | 51 | - |
Acoustics.RoomAcousticsSabineFromJCost |
2 | 0 | 2 | 62 | - |
Acoustics.RoomImpulseResponseFromJCost |
4 | 0 | 3 | 51 | - |
Acoustics.Room_Acoustics_RT60_RS |
4 | 0 | 3 | 36 | - |
Acoustics.SpeechIntelligibilityFromJCost |
6 | 0 | 3 | 79 | - |