feat: Add start to Spin10

HepLean.lean

@@ -47,6 +47,7 @@ import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
 import HepLean.BeyondTheStandardModel.PatiSalam.Basic
+import HepLean.BeyondTheStandardModel.Spin10.Basic
 import HepLean.BeyondTheStandardModel.TwoHDM.Basic
 import HepLean.FeynmanDiagrams.Basic
 import HepLean.FeynmanDiagrams.Instances.ComplexScalar

HepLean/BeyondTheStandardModel/Spin10/Basic.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.BeyondTheStandardModel.PatiSalam.Basic
+import HepLean.Meta.Informal
+/-!
+
+# The Spin(10) Model
+
+Note: By physicists this is usually called SO(10). However, the true gauge group involved
+is Spin(10).
+
+-/
+
+namespace Spin10Model
+
+informal_definition GaugeGroupI where
+  math :≈ "The group `Spin(10)`."
+  physics :≈ "The gauge group of the Spin(10) model (aka SO(10)-model.)"
+
+informal_definition embedPatiSalam where
+  physics :≈ "The embedding of the Pati-Salam gauge group into Spin(10)."
+  math :≈ "The lift of the embedding `SO(6) x SO(4) → SO(10)` to universal covers,
+    giving a homomorphism `Spin(6) x Spin(4) → Spin(10)`. Precomposed with the isomorphism,
+    ``PatiSalam.gaugeGroupISpinEquiv,
+    between `SU(4) x SU(2) x SU(2)` and `Spin(6) x Spin(4)`."
+  ref :≈ "Page 56 of https://math.ucr.edu/home/baez/guts.pdf"
+  deps :≈ [``GaugeGroupI, ``PatiSalam.GaugeGroupI, ``PatiSalam.gaugeGroupISpinEquiv]
+
+end Spin10Model

README.md

@@ -4,6 +4,7 @@
 [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
 [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
 [![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList)
+[![](https://img.shields.io/badge/Informal_dependencies-Graph-green)](https://heplean.github.io/HepLean/graph.svg)
 [![](https://img.shields.io/badge/Lean-v4.11.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.11.0)
 
 A project to digitalize high energy physics.