StandardModel
StandardModel modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
StandardModel.CKMMatrix |
9 | 0 | 29 | 297 | — |
StandardModel.ElectroweakBreaking |
8 | 0 | 16 | 271 | — |
StandardModel.ElectroweakMassBridge |
11 | 0 | 7 | 212 | — |
StandardModel.HiggsEFTBridge |
11 | 0 | 6 | 279 | — |
StandardModel.HiggsEFTLowEnergyLimit |
1 | 0 | 1 | 114 | — |
StandardModel.HiggsObservableSkeleton |
10 | 0 | 5 | 231 | — |
StandardModel.HiggsRungAssignment |
8 | 0 | 8 | 220 | — |
StandardModel.HiggsYukawaBridge |
7 | 0 | 3 | 182 | — |
StandardModel.LongitudinalVectorScattering |
7 | 0 | 7 | 202 | — |
StandardModel.NeutrinoMassHierarchy |
12 | 4 | 19 | 334 | — |
StandardModel.PMNSMatrix |
7 | 0 | 23 | 343 | — |
StandardModel.ProtonMass |
4 | 2 | 6 | 88 | — |
StandardModel.Q3Representations |
13 | 0 | 10 | 216 | — |
StandardModel.StrongCP |
7 | 0 | 14 | 322 | — |
StandardModel.SupersymmetryBreaking |
2 | 0 | 10 | 248 | — |
StandardModel.WZMassRatio |
5 | 0 | 18 | 228 | — |
StandardModel.WeakCoupling |
7 | 1 | 1 | 114 | — |
StandardModel.WeinbergAngle |
4 | 0 | 16 | 232 | — |