Merge pull request #163 from HEPLean/informal_defs
feat: Start on Spin10
This commit is contained in:
commit
2071903022
4 changed files with 38 additions and 4 deletions
|
@ -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
|
||||
|
|
32
HepLean/BeyondTheStandardModel/Spin10/Basic.lean
Normal file
32
HepLean/BeyondTheStandardModel/Spin10/Basic.lean
Normal file
|
@ -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
|
|
@ -75,8 +75,8 @@ macro "informal_definition " name:ident " where " assignments:informalAssignment
|
|||
| `(informalAssignment| ref :≈ $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
|
||||
ref_def? := some (← `($(Lean.quote strVal)))
|
||||
| `(informalAssignmentDeps| deps :≈ [ $deps,* ]) =>
|
||||
dep_def? := some (← `([ $deps,* ]))
|
||||
| `(informalAssignmentDeps| deps :≈ [$deps,*]) =>
|
||||
dep_def? := some (← `([$deps,*]))
|
||||
| _ => Macro.throwError "invalid assignment syntax in informal_definition"
|
||||
unless math_def?.isSome do
|
||||
Macro.throwError "A 'math' assignments is required"
|
||||
|
@ -115,8 +115,8 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
|
|||
| `(informalAssignment| ref :≈ $val:str) =>
|
||||
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
|
||||
ref_def? := some (← `($(Lean.quote strVal)))
|
||||
| `(informalAssignmentDeps| deps :≈ [ $deps,* ]) =>
|
||||
dep_def? := some (← `([ $deps,* ]))
|
||||
| `(informalAssignmentDeps| deps :≈ [$deps,*]) =>
|
||||
dep_def? := some (← `([$deps,*]))
|
||||
| _ => Macro.throwError "invalid assignment syntax"
|
||||
unless math_def?.isSome do
|
||||
Macro.throwError "A 'math' assignments is required"
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
[](https://github.com/HEPLean/HepLean/pulls)
|
||||
[](https://leanprover.zulipchat.com)
|
||||
[](https://heplean.github.io/HepLean/TODOList)
|
||||
[](https://heplean.github.io/HepLean/graph.svg)
|
||||
[](https://github.com/leanprover/lean4/releases/tag/v4.11.0)
|
||||
|
||||
A project to digitalize high energy physics.
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue