Merge pull request #74 from HEPLean/Update-versions

refactor: Higgs physics

HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean

@@ -18,20 +18,89 @@ namespace TwoHDM
 
 open StandardModel
 open ComplexConjugate
+open HiggsField
 
 noncomputable section
 
-/-- The potential of the two Higgs doublet model.  -/
+/-- The potential of the two Higgs doublet model. -/
-def potential (Φ1 Φ2 : HiggsField)
+def potential (Φ1 Φ2 : HiggsField) (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ)
-    (m11Sq m22Sq lam₁ lam₂ lam₃ lam₄ : ℝ) (m12Sq lam₅ lam₆ lam₇ : ℂ) (x : SpaceTime) : ℝ :=
+    (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ) (x : SpaceTime) : ℝ :=
-  m11Sq * Φ1.normSq x  + m22Sq * Φ2.normSq x
+  m₁₁2 * ‖Φ1‖_H ^ 2 x  + m₂₂2 * ‖Φ2‖_H ^ 2 x - (m₁₂2 * ⟪Φ1, Φ2⟫_H x + conj m₁₂2 * ⟪Φ2, Φ1⟫_H x).re
-  - (m12Sq * (Φ1.innerProd Φ2) x + conj m12Sq * (Φ2.innerProd Φ1) x).re
+  + 1/2 * 𝓵₁ *  ‖Φ1‖_H ^ 2 x * ‖Φ1‖_H ^ 2 x + 1/2 * 𝓵₂ * ‖Φ2‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x
-  + 1/2 * lam₁ * Φ1.normSq x ^ 2 + 1/2 * lam₂ * Φ2.normSq x ^ 2
+  + 𝓵₃ * ‖Φ1‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x
-  + lam₃ * Φ1.normSq x * Φ2.normSq x
+  + 𝓵₄ * ‖⟪Φ1, Φ2⟫_H x‖ ^ 2 + (1/2 * 𝓵₅ * ⟪Φ1, Φ2⟫_H  x ^ 2 + 1/2 * conj 𝓵₅ * ⟪Φ2, Φ1⟫_H x ^ 2).re
-  + lam₄ * ‖Φ1.innerProd Φ2 x‖
+  + (𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj 𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re
-  + (1/2 * lam₅ * (Φ1.innerProd Φ2) x ^ 2 + 1/2 * conj lam₅ * (Φ2.innerProd Φ1) x ^ 2).re
+  + (𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj 𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re
-  + (lam₆ * Φ1.normSq x * (Φ1.innerProd Φ2) x + conj lam₆ * Φ1.normSq x * (Φ2.innerProd Φ1) x).re
+
-  + (lam₇ * Φ2.normSq x * (Φ1.innerProd Φ2) x + conj lam₇ * Φ2.normSq x * (Φ2.innerProd Φ1) x).re
+namespace potential
+
+variable (Φ1 Φ2 : HiggsField)
+variable (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ)
+variable (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ)
+/-!
+
+## Simple properties of the potential
+
+-/
+
+/-- Swapping `Φ1` with `Φ2`, and a number of the parameters (with possible conjugation) leads
+  to an identical potential. -/
+lemma swap_fields :
+    potential Φ1 Φ2 m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇
+    = potential Φ2 Φ1 m₂₂2 m₁₁2 𝓵₂ 𝓵₁ 𝓵₃ 𝓵₄ (conj m₁₂2) (conj 𝓵₅) (conj 𝓵₇) (conj 𝓵₆)  := by
+  funext x
+  simp only [potential, HiggsField.normSq, Complex.add_re, Complex.mul_re, Complex.conj_re,
+    Complex.conj_im, neg_mul, sub_neg_eq_add, one_div, Complex.norm_eq_abs, Complex.inv_re,
+    Complex.re_ofNat, Complex.normSq_ofNat, div_self_mul_self', Complex.inv_im, Complex.im_ofNat,
+    neg_zero, zero_div, zero_mul, sub_zero, Complex.mul_im, add_zero, mul_neg, Complex.ofReal_pow,
+    RingHomCompTriple.comp_apply, RingHom.id_apply]
+  ring_nf
+  simp only [one_div, add_left_inj, add_right_inj, mul_eq_mul_left_iff]
+  apply Or.inl
+  rw [HiggsField.innerProd, HiggsField.innerProd, ← InnerProductSpace.conj_symm, Complex.abs_conj]
+
+/-- If `Φ₂` is zero the potential reduces to the Higgs potential on `Φ₁`. -/
+lemma right_zero : potential Φ1 0 m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇  =
+    StandardModel.HiggsField.potential Φ1 (- m₁₁2) (𝓵₁/2) := by
+  funext x
+  simp only [potential, normSq, ContMDiffSection.coe_zero, Pi.zero_apply, norm_zero, ne_eq,
+    OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero, add_zero, innerProd_right_zero,
+    innerProd_left_zero, Complex.zero_re, sub_zero, one_div, Complex.ofReal_pow,
+    Complex.ofReal_zero, HiggsField.potential, neg_neg, add_right_inj, mul_eq_mul_right_iff,
+    pow_eq_zero_iff, norm_eq_zero, or_self_right]
+  ring_nf
+  simp only [true_or]
+
+/-- If `Φ₁` is zero the potential reduces to the Higgs potential on `Φ₂`. -/
+lemma left_zero : potential 0 Φ2 m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇  =
+    StandardModel.HiggsField.potential Φ2 (- m₂₂2) (𝓵₂/2) := by
+  rw [swap_fields, right_zero]
+
+/-!
+
+## Potential bounded from below
+
+TODO: Complete this section.
+
+-/
+
+/-!
+
+## Smoothness of the potential
+
+TODO: Complete this section.
+
+-/
+
+/-!
+
+## Invariance of the potential under gauge transformations
+
+TODO: Complete this section.
+
+-/
+
+end potential
 
 end
 end TwoHDM

HepLean/StandardModel/HiggsBoson/Basic.lean

@@ -23,7 +23,7 @@ This file defines the basic properties for the higgs field in the standard model
 
 ## References
 
-- We use conventions given in: https://pdg.lbl.gov/2019/reviews/rpp2019-rev-higgs-boson.pdf
+- We use conventions given in: [Review of Particle Physics, PDG][ParticleDataGroup:2018ovx]
 
 -/
 universe v u
@@ -35,6 +35,11 @@ open Matrix
 open Complex
 open ComplexConjugate
 open SpaceTime
+/-!
+
+## Definition of the Higgs bundle
+
+-/
 
 /-- The trivial vector bundle 𝓡² × ℂ². (TODO: Make associated bundle.) -/
 abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec
@@ -60,6 +65,12 @@ noncomputable def HiggsVec.toField (φ : HiggsVec) : HiggsField where
 namespace HiggsField
 open  Complex Real
 
+/-!
+
+## Relation to `HiggsVec`
+
+-/
+
 /-- Given a `higgsField`, the corresponding map from `spaceTime` to `higgsVec`. -/
 def toHiggsVec (φ : HiggsField) : SpaceTime → HiggsVec := φ
 
@@ -80,6 +91,88 @@ lemma toField_toHiggsVec_apply (φ : HiggsField) (x : SpaceTime) :
 lemma higgsVecToFin2ℂ_toHiggsVec (φ : HiggsField) :
     higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl
 
+/-!
+
+## The inner product and norm of Higgs fields
+
+-/
+
+/-- Given two `HiggsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/
+def innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
+
+/-- Notation for the inner product of two Higgs fields. -/
+scoped[StandardModel.HiggsField] notation "⟪" φ1 "," φ2 "⟫_H" => innerProd φ1 φ2
+
+@[simp]
+lemma innerProd_left_zero (φ : HiggsField) : ⟪0, φ⟫_H = 0 := by
+  funext x
+  simp [innerProd]
+
+@[simp]
+lemma innerProd_right_zero (φ : HiggsField) : ⟪φ, 0⟫_H = 0 := by
+  funext x
+  simp [innerProd]
+
+lemma innerProd_expand (φ1 φ2 : HiggsField)  :
+    ⟪φ1, φ2⟫_H  = fun x => (conj (φ1 x 0) * (φ2 x 0) + conj (φ1 x 1) * (φ2 x 1) ) := by
+  funext x
+  simp only [innerProd, PiLp.inner_apply, RCLike.inner_apply, Fin.sum_univ_two]
+
+/-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the
+ higgs vector.  -/
+@[simp]
+def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ( ‖φ x‖ ^ 2)
+
+/-- Notation for the norm squared of a Higgs field. -/
+scoped[StandardModel.HiggsField] notation "‖" φ1 "‖_H ^ 2" => normSq φ1
+
+lemma innerProd_self_eq_normSq (φ : HiggsField) (x : SpaceTime) :
+    ⟪φ, φ⟫_H x  = ‖φ‖_H ^ 2 x := by
+  erw [normSq, @PiLp.norm_sq_eq_of_L2, Fin.sum_univ_two]
+  simp only [ ofReal_add, ofReal_pow, innerProd, PiLp.inner_apply,
+    RCLike.inner_apply, Fin.sum_univ_two, conj_mul']
+
+lemma normSq_eq_innerProd_self (φ : HiggsField) (x : SpaceTime) :
+    ‖φ x‖ ^ 2 = (⟪φ, φ⟫_H x).re := by
+  rw [innerProd_self_eq_normSq]
+  rfl
+
+lemma toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) :
+    ‖φ x‖  = ‖φ.toHiggsVec x‖ := rfl
+
+lemma normSq_expand (φ : HiggsField)  :
+    φ.normSq  = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1) ).re := by
+  funext x
+  simp [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add, @norm_sq_eq_inner ℂ]
+
+lemma normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ φ.normSq x := by
+  simp [normSq, ge_iff_le, norm_nonneg, pow_nonneg]
+
+lemma normSq_zero (φ : HiggsField) (x : SpaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by
+  simp [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero]
+
+/-!
+
+## The Higgs potential
+
+-/
+
+/-- The Higgs potential of the form `- μ² * |φ|² + λ * |φ|⁴`. -/
+@[simp]
+def potential (φ : HiggsField) (μSq lambda : ℝ ) (x : SpaceTime) :  ℝ :=
+  - μSq * φ.normSq x + lambda * φ.normSq x * φ.normSq x
+
+lemma potential_apply (φ : HiggsField) (μSq lambda : ℝ) (x : SpaceTime) :
+    (φ.potential μSq lambda) x = HiggsVec.potential μSq lambda (φ.toHiggsVec x) := by
+  simp [HiggsVec.potential, toHiggsVec_norm]
+  ring
+
+/-!
+
+## Smoothness
+
+-/
+
 lemma toVec_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ :=
   smooth_higgsVecToFin2ℂ.comp φ.toHiggsVec_smooth
 
@@ -95,22 +188,6 @@ lemma apply_im_smooth (φ : HiggsField) (i : Fin 2):
     Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : SpaceTime) =>  (φ x i))) :=
   (ContinuousLinearMap.smooth imCLM).comp (φ.apply_smooth i)
 
-/-- Given two `higgsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/
-def innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
-
-/-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the
- higgs vector.  -/
-@[simp]
-def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ( ‖φ x‖ ^ 2)
-
-lemma toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) :
-    ‖φ x‖  = ‖φ.toHiggsVec x‖ := rfl
-
-lemma normSq_expand (φ : HiggsField)  :
-    φ.normSq  = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1) ).re := by
-  funext x
-  simp [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add, @norm_sq_eq_inner ℂ]
-
 lemma normSq_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) φ.normSq := by
   rw [normSq_expand]
   refine Smooth.add ?_ ?_
@@ -131,27 +208,17 @@ lemma normSq_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ,
   exact φ.apply_im_smooth 1
   exact φ.apply_im_smooth 1
 
-lemma normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ φ.normSq x := by
-  simp [normSq, ge_iff_le, norm_nonneg, pow_nonneg]
-
-lemma normSq_zero (φ : HiggsField) (x : SpaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by
-  simp [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero]
-
-/-- The Higgs potential of the form `- μ² * |φ|² + λ * |φ|⁴`. -/
-@[simp]
-def potential (φ : HiggsField) (μSq lambda : ℝ ) (x : SpaceTime) :  ℝ :=
-  - μSq * φ.normSq x + lambda * φ.normSq x * φ.normSq x
-
 lemma potential_smooth (φ : HiggsField) (μSq lambda : ℝ) :
     Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (fun x => φ.potential μSq lambda x) := by
   simp only [potential, normSq, neg_mul]
   exact (smooth_const.smul φ.normSq_smooth).neg.add
     ((smooth_const.smul φ.normSq_smooth).smul φ.normSq_smooth)
 
-lemma potential_apply (φ : HiggsField) (μSq lambda : ℝ) (x : SpaceTime) :
+/-!
-    (φ.potential μSq lambda) x = HiggsVec.potential μSq lambda (φ.toHiggsVec x) := by
+
-  simp [HiggsVec.potential, toHiggsVec_norm]
+## Constant higgs fields
-  ring
+
+-/
 
 /-- A higgs field is constant if it is equal for all `x` `y` in `spaceTime`. -/
 def IsConst (Φ : HiggsField) : Prop := ∀ x y, Φ x = Φ y

HepLean/StandardModel/HiggsBoson/TargetSpace.lean

@@ -24,7 +24,7 @@ This file is a import of `SM.HiggsBoson.Basic`.
 
 ## References
 
-- We use conventions given in: https://pdg.lbl.gov/2019/reviews/rpp2019-rev-higgs-boson.pdf
+- We use conventions given in: [Review of Particle Physics, PDG][ParticleDataGroup:2018ovx]
 
 -/
 universe v u
@@ -36,6 +36,12 @@ open Matrix
 open Complex
 open ComplexConjugate
 
+/-!
+
+## The definition of the Higgs vector space.
+
+-/
+
 /-- The complex vector space in which the Higgs field takes values. -/
 abbrev HiggsVec := EuclideanSpace ℂ (Fin 2)
 
@@ -50,6 +56,15 @@ lemma smooth_higgsVecToFin2ℂ : Smooth 𝓘(ℝ, HiggsVec) 𝓘(ℝ, Fin 2 →
   ContinuousLinearMap.smooth higgsVecToFin2ℂ
 
 namespace HiggsVec
+/-- An orthonormal basis of higgsVec. -/
+noncomputable def orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec :=
+  EuclideanSpace.basisFun (Fin 2) ℂ
+
+/-!
+
+## The representation of the gauge group on the Higgs vector space
+
+-/
 
 /-- The Higgs representation as a homomorphism from the gauge group to unitary `2×2`-matrices. -/
 @[simps!]
@@ -63,10 +78,6 @@ noncomputable def higgsRepUnitary : GaugeGroup →* unitaryGroup (Fin 2) ℂ whe
     repeat rw [mul_assoc]
   map_one' := by simp
 
-/-- An orthonormal basis of higgsVec. -/
-noncomputable def orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec :=
-  EuclideanSpace.basisFun (Fin 2) ℂ
-
 /-- Takes in a `2×2`-matrix and returns a linear map of `higgsVec`. -/
 noncomputable def matrixToLin : Matrix (Fin 2) (Fin 2) ℂ →* (HiggsVec →L[ℂ] HiggsVec) where
   toFun g := LinearMap.toContinuousLinearMap
@@ -109,24 +120,37 @@ lemma higgsRepUnitary_mul (g : GaugeGroup) (φ : HiggsVec) :
 lemma rep_apply (g : GaugeGroup) (φ : HiggsVec) : rep g φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) :=
   higgsRepUnitary_mul g φ
 
-lemma norm_invariant (g : GaugeGroup) (φ : HiggsVec) : ‖rep g φ‖ = ‖φ‖ :=
-  ContinuousLinearMap.norm_map_of_mem_unitary (unitaryToLin (higgsRepUnitary g)).2 φ
-
 section potentialDefn
 
 variable (μSq lambda : ℝ)
 local notation "λ" => lambda
 
+/-!
+
+## The potential for a Higgs vector
+
+-/
+
 /-- The higgs potential for `higgsVec`, i.e. for constant higgs fields. -/
 def potential (φ : HiggsVec) : ℝ := - μSq  * ‖φ‖ ^ 2 + λ * ‖φ‖ ^ 4
 
+lemma potential_as_quad (φ : HiggsVec) :
+    λ  * ‖φ‖ ^ 2 * ‖φ‖ ^ 2 + (- μSq ) * ‖φ‖ ^ 2 + (- potential μSq (λ) φ) = 0 := by
+  simp [potential]; ring
+
+/-!
+
+## Invariance of the potential under global gauge transformation
+
+-/
+
+lemma norm_invariant (g : GaugeGroup) (φ : HiggsVec) : ‖rep g φ‖ = ‖φ‖ :=
+  ContinuousLinearMap.norm_map_of_mem_unitary (unitaryToLin (higgsRepUnitary g)).2 φ
+
 lemma potential_invariant (φ : HiggsVec)  (g : GaugeGroup) :
     potential μSq (λ) (rep g φ) = potential μSq (λ) φ := by
   simp only [potential, neg_mul, norm_invariant]
 
-lemma potential_as_quad (φ : HiggsVec) :
-    λ  * ‖φ‖ ^ 2 * ‖φ‖ ^ 2 + (- μSq ) * ‖φ‖ ^ 2 + (- potential μSq (λ) φ) = 0 := by
-  simp [potential]; ring
 
 end potentialDefn
 section potentialProp
@@ -136,6 +160,12 @@ variable (μSq : ℝ)
 variable (hLam : 0 < lambda)
 local notation "λ" => lambda
 
+/-!
+
+## Lower bound on potential
+
+-/
+
 lemma potential_snd_term_nonneg (φ : HiggsVec) :
     0 ≤ λ * ‖φ‖ ^ 4 := by
   rw [mul_nonneg_iff]
@@ -197,6 +227,12 @@ lemma potential_bounded_below_of_μSq_nonpos  {μSq : ℝ}
   field_simp [mul_nonpos_iff]
   simp_all [ge_iff_le, norm_nonneg, pow_nonneg, and_self, or_true]
 
+/-!
+
+## Minimum of the potential
+
+-/
+
 lemma potential_eq_bound_discrim_zero (φ : HiggsVec)
     (hV : potential μSq (λ) φ = - μSq ^ 2 / (4  * λ)) :
     discrim (λ) (- μSq) (- potential μSq (λ) φ) = 0 := by
@@ -264,6 +300,12 @@ lemma IsMinOn_potential_iff_of_μSq_nonpos {μSq : ℝ} (hμSq : μSq ≤ 0) :
   · exact potential_eq_bound_IsMinOn_of_μSq_nonpos hLam hμSq φ
 
 end potentialProp
+/-!
+
+## Gauge freedom
+
+-/
+
 /-- Given a Higgs vector, a rotation matrix which puts the first component of the
 vector to zero, and the second component to a real -/
 def rotateMatrix (φ : HiggsVec) : Matrix (Fin 2) (Fin 2) ℂ :=

docs/references.bib

@@ -34,6 +34,18 @@
   year          = "2020"
 }
 
+@Article{         ParticleDataGroup:2018ovx,
+  author        = "Tanabashi, M. and others",
+  collaboration = "Particle Data Group",
+  title         = "{Review of Particle Physics}",
+  doi           = "10.1103/PhysRevD.98.030001",
+  journal       = "Phys. Rev. D",
+  volume        = "98",
+  number        = "3",
+  pages         = "030001",
+  year          = "2018"
+}
+
 @Article{         raynor2021graphical,
   title         = {Graphical combinatorics and a distributive law for modular
                   operads},