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 |
0 | 0 | 0 | 46 | - |
Quantum.BekensteinHawking |
10 | 0 | 16 | 265 | - |
Quantum.BellInequality |
11 | 1 | 10 | 239 | - |
Quantum.BlackHoleInformation |
10 | 0 | 8 | 267 | - |
Quantum.BornRule |
6 | 1 | 0 | 115 | - |
Quantum.BornRuleStructure |
4 | 0 | 1 | 35 | - |
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.EntanglementOntologyStructure |
2 | 0 | 1 | 30 | - |
Quantum.Firewall |
6 | 0 | 3 | 252 | - |
Quantum.HilbertSpace |
0 | 0 | 0 | 26 | - |
Quantum.HolographicBound |
9 | 0 | 11 | 227 | - |
Quantum.NonlocalityNoSignaling |
6 | 0 | 7 | 247 | - |
Quantum.Observables |
0 | 0 | 0 | 30 | - |
Quantum.PlanckScale |
3 | 0 | 14 | 204 | - |
Quantum.PointerStates |
5 | 0 | 5 | 220 | - |
Quantum.PureTwoQubit.EntropyConcurrence |
41 | 0 | 9 | 675 | - |
Quantum.QMInterpretationStructure |
2 | 0 | 1 | 27 | - |
Quantum.RecognitionFirst.EightTickWeyl |
4 | 0 | 3 | 96 | - |
Quantum.RecognitionFirst.RecogPhysicsStaging |
0 | 0 | 0 | 36 | - |
Quantum.ZenoEffect |
8 | 0 | 9 | 207 | - |