Merge pull request #168 from HEPLean/informal_defs

feat: Informal lemmas about Higgs bosons

HepLean.lean

@@ -50,6 +50,7 @@ import HepLean.BeyondTheStandardModel.GeorgiGlashow.Basic
 import HepLean.BeyondTheStandardModel.PatiSalam.Basic
 import HepLean.BeyondTheStandardModel.Spin10.Basic
 import HepLean.BeyondTheStandardModel.TwoHDM.Basic
+import HepLean.BeyondTheStandardModel.TwoHDM.GaugeOrbits
 import HepLean.FeynmanDiagrams.Basic
 import HepLean.FeynmanDiagrams.Instances.ComplexScalar
 import HepLean.FeynmanDiagrams.Instances.Phi4

HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean

@@ -142,7 +142,8 @@ lemma left_eq_neg_right : P.toFun Φ1 (- Φ1) =
 -/
 
 /-! TODO: Prove bounded properties of the 2HDM potential.
-  See e.g. https://inspirehep.net/literature/201299. -/
+  See e.g. https://inspirehep.net/literature/201299 and
+  https://arxiv.org/pdf/hep-ph/0605184. -/
 
 /-- The proposition on the coefficents for a potential to be bounded. -/
 def IsBounded : Prop :=

HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean

@@ -0,0 +1,35 @@
+/-
+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.TwoHDM.Basic
+/-!
+
+# Gauge orbits for the 2HDM
+
+The main reference for material in this section is https://arxiv.org/pdf/hep-ph/0605184.
+
+-/
+
+namespace TwoHDM
+
+informal_definition prodMatrix where
+  math :≈ "For two Higgs fields `Φ₁` and `Φ₂`, the map from space time to 2 x 2 complex matrices
+  defined by ((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂)). "
+  ref :≈ "https://arxiv.org/pdf/hep-ph/0605184 eq 3.8."
+  deps :≈ [``StandardModel.HiggsVec, ``SpaceTime]
+
+informal_lemma prodMatrix_positive_semidefinite where
+  math :≈ "For all x in ``SpaceTime, ``prodMatrix at `x` is positive semidefinite."
+  deps :≈ [``prodMatrix, ``SpaceTime]
+
+informal_lemma prodMatrix_hermitian where
+  math :≈ "For all x in ``SpaceTime, ``prodMatrix at `x` is hermitian."
+  deps :≈ [``prodMatrix, ``SpaceTime]
+
+informal_lemma prodMatrix_smooth where
+  math :≈ "The map ``prodMatrix is a smooth function on spacetime."
+  deps :≈ [``prodMatrix]
+
+end TwoHDM

HepLean/StandardModel/Basic.lean

@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.LinearAlgebra.Matrix.ToLin
+import HepLean.SpaceTime.Basic
 import HepLean.Meta.Informal
 /-!
 # The Standard Model
@@ -83,4 +84,26 @@ informal_definition GaugeGroup where
   deps :≈ [``GaugeGroupI, ``gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup, ``gaugeGroupℤ₃SubGroup,
     ``GaugeGroupQuot]
 
+/-!
+
+## Smoothness structure on the gauge group.
+
+-/
+
+informal_lemma gaugeGroupI_lie where
+  math :≈ "The gauge group `GaugeGroupI` is a Lie group.."
+  deps :≈ [``GaugeGroupI]
+
+informal_lemma gaugeGroup_lie where
+  math :≈ "For every q in ``GaugeGroupQuot the group ``GaugeGroup q is a Lie group."
+  deps :≈ [``GaugeGroup]
+
+informal_definition gaugeBundleI where
+  math :≈ "The trivial principal bundle over SpaceTime with structure group ``GaugeGroupI."
+  deps :≈ [``GaugeGroupI, ``SpaceTime]
+
+informal_definition gaugeTransformI where
+  math :≈ "A global section of ``gaugeBundleI."
+  deps :≈ [``gaugeBundleI]
+
 end StandardModel

HepLean/StandardModel/HiggsBoson/GaugeAction.lean

@@ -190,6 +190,11 @@ theorem rotate_fst_real_snd_zero (φ : HiggsVec) :
   · simp only [Fin.mk_one, Fin.isValue, Pi.smul_apply, Function.comp_apply, cons_val_one, head_cons,
       tail_cons, smul_zero]
 
+informal_lemma guage_orbit where
+  math :≈ "There exists a `g` in ``GaugeGroupI such that `rep g φ = φ'` if and only if
+    ‖φ‖ = ‖φ'‖."
+  deps :≈ [``rotate_fst_zero_snd_real]
+
 informal_lemma stability_group_single where
   physics :≈ "The Higgs boson breaks electroweak symmetry down to the electromagnetic force."
   math :≈ "The stablity group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`,
@@ -203,7 +208,7 @@ informal_lemma stability_group where
     by the action of ``StandardModel.HiggsVec.rep is given by `SU(3) x ℤ₆` where ℤ₆
     is the subgroup of `SU(2) x U(1)` with elements `(α^(-3) * I₂, α)` where
     α is a sixth root of unity."
-  deps :≈ [``StandardModel.HiggsVec, ``StandardModel.HiggsVec.rep]
+  deps :≈ [``HiggsVec, ``rep]
 
 end HiggsVec
 
@@ -211,5 +216,30 @@ end HiggsVec
 /-! TODO: Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary) -/
 /-! TODO: Prove invariance of potential under global gauge action. -/
 
+namespace HiggsField
+
+/-!
+
+## Gauge transformations acting on Higgs fields.
+
+-/
+
+informal_definition gaugeAction where
+  math :≈ "The action of ``gaugeTransformI on ``HiggsField acting pointwise through
+    ``HiggsVec.rep."
+  deps :≈ [``HiggsVec.rep, ``gaugeTransformI]
+
+informal_lemma guage_orbit where
+  math :≈ "There exists a `g` in ``gaugeTransformI such that `gaugeAction g φ = φ'` if and only if
+    φ(x)^† φ(x) = φ'(x)^† φ'(x)."
+  deps :≈ [``gaugeAction]
+
+informal_lemma gauge_orbit_surject where
+  math :≈ "For every smooth map f from ``SpaceTime to ℝ such that `f` is positive semidefinite,
+    there exists a Higgs field φ such that `f = φ^† φ`."
+  deps :≈ [``HiggsField, ``SpaceTime]
+
+end HiggsField
+
 end StandardModel
 end