Quantum
Quantum modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
Quantum.AreaQuantization |
3 | 0 | 2 | 113 | — |
Quantum.BekensteinHawking |
10 | 0 | 16 | 265 | — |
Quantum.BellInequality |
11 | 1 | 10 | 239 | — |
Quantum.BlackHoleInformation |
10 | 0 | 8 | 267 | — |
Quantum.ClassicalEmergence |
9 | 0 | 8 | 241 | — |
Quantum.CommutationStructure |
1 | 0 | 1 | 24 | — |
Quantum.ComplexHilbertStructure |
2 | 0 | 1 | 29 | — |
Quantum.DoubleSlit |
8 | 3 | 12 | 263 | — |
Quantum.EntanglementEntropy |
8 | 0 | 12 | 255 | — |
Quantum.Firewall |
6 | 0 | 3 | 252 | — |
Quantum.HilbertSpace |
0 | 0 | 0 | 26 | — |
Quantum.HolographicBound |
9 | 0 | 11 | 227 | — |
Quantum.Measurement.WavefunctionCollapse |
12 | 2 | 7 | 291 | — |
Quantum.NonlocalityNoSignaling |
6 | 0 | 7 | 247 | — |
Quantum.Observables |
0 | 0 | 0 | 30 | — |
Quantum.PageCurve |
6 | 0 | 8 | 211 | — |
Quantum.PlanckScale |
3 | 0 | 14 | 204 | — |
Quantum.PointerStates |
5 | 0 | 5 | 220 | — |
Quantum.QMInterpretationStructure |
2 | 0 | 1 | 27 | — |
Quantum.ZenoEffect |
8 | 0 | 9 | 207 | — |