CondensedMatter
CondensedMatter modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
CondensedMatter.AndersonLocalizationFromJCost |
4 | 0 | 3 | 58 | - |
CondensedMatter.BCS_Coherence_Length_RS |
4 | 0 | 3 | 36 | - |
CondensedMatter.Cooper_Pair_Binding_RS |
4 | 0 | 3 | 36 | - |
CondensedMatter.CuprateTcFromPhiLadder |
4 | 0 | 3 | 51 | - |
CondensedMatter.GlassTransitionStructure |
2 | 0 | 1 | 22 | - |
CondensedMatter.Hall_Resistance_RS |
4 | 0 | 3 | 36 | - |
CondensedMatter.HighTcSuperconductivityStructure |
3 | 0 | 1 | 26 | - |
CondensedMatter.JCostPhaseTransition |
6 | 0 | 4 | 72 | - |
CondensedMatter.Josephson_Frequency_RS |
4 | 0 | 3 | 36 | - |
CondensedMatter.MottTransitionFromJCost |
4 | 0 | 3 | 47 | - |
CondensedMatter.Mott_Insulator_U_RS |
4 | 0 | 3 | 36 | - |
CondensedMatter.RoomTemperatureSuperconductivityStructure |
3 | 0 | 1 | 27 | - |
CondensedMatter.SpinGlassFreezingRatio |
6 | 0 | 3 | 138 | - |
CondensedMatter.StronglyCorrelatedElectronsStructure |
2 | 0 | 1 | 23 | - |
CondensedMatter.TopologicalPhasesStructure |
2 | 0 | 1 | 23 | - |