Revision #1588 → #1799 · back to history
modifiedHiggs particle5a55e28e0824
| Field | From #1588 | To #1799 |
|---|
| note | Particle-physics definition with no Mathlib content. | Particle-physics definition with no Mathlib content (no 'Higgs' files exist in Mathlib). |
modifiedLagrangian framework of the Standard Model530445c19ea5
| Field | From #1588 | To #1799 |
|---|
| note | Quantum field theory / Lagrangian formalism is not developed in Mathlib (no 'Lagrangian' declarations). | Quantum field theory / Lagrangian formalism is not developed in Mathlib (grep finds no 'Lagrangian' declarations). |
modifiedSU(3)×SU(2)×U(1) gauge symmetry5fbbaaea793a
| Field | From #1588 | To #1799 |
|---|
| note | Mathlib defines the abstract groups SU(n)/U(n) via Matrix.specialUnitaryGroup and Matrix.unitaryGroup, but not the Standard Model gauge group or its action as a physical symmetry. | Mathlib defines the abstract groups SU(n)/U(n) via Matrix.specialUnitaryGroup and Matrix.unitaryGroup (verified), but not the Standard Model gauge group or its action as a physical symmetry. |
modifiedGauge covariant derivative of QCD69e993aef3c6
| Field | From #1588 | To #1799 |
|---|
| note | Mathlib has a general covariant-derivative/connection structure on vector bundles, but not the specific QCD gauge covariant derivative with gluon fields and SU(3) generators. | Mathlib has a general covariant-derivative/connection structure on vector bundles (verified), but not the specific QCD gauge covariant derivative with gluon fields and SU(3) generators. |
modifiedElectroweak sector Lagrangianed75fc00a20f
| Field | From #1588 | To #1799 |
|---|
| note | Yang–Mills electroweak theory has no formalization in Mathlib (no Yang–Mills content). | Yang–Mills electroweak theory has no formalization in Mathlib (grep finds no Yang–Mills content). |
modifiedElectroweak gauge covariant derivative9d4cd49a83a0
| Field | From #1588 | To #1799 |
|---|
| note | Only the abstract vector-bundle covariant derivative exists; the specific electroweak SU(2)×U(1) covariant derivative is not formalized. | Only the abstract vector-bundle covariant derivative exists (verified); the specific electroweak SU(2)×U(1) covariant derivative is not formalized. |
addedDirac equation5509c0e5b192
addedDirac matrices (gamma matrices)8de2de9ddc00
addedGell-Mann matrices (SU(3) generators)80c574272d91
addedPauli matrices (SU(2) generators)27c150f0a398
addedYang–Mills existence and mass gap problemb953f155d04e