diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean index c6429d7..a3432b5 100644 --- a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean +++ b/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. -/ -def potential (Φ1 Φ2 : HiggsField) - (m11Sq m22Sq lam₁ lam₂ lam₃ lam₄ : ℝ) (m12Sq lam₅ lam₆ lam₇ : ℂ) (x : SpaceTime) : ℝ := - m11Sq * Φ1.normSq x + m22Sq * Φ2.normSq x - - (m12Sq * (Φ1.innerProd Φ2) x + conj m12Sq * (Φ2.innerProd Φ1) x).re - + 1/2 * lam₁ * Φ1.normSq x ^ 2 + 1/2 * lam₂ * Φ2.normSq x ^ 2 - + lam₃ * Φ1.normSq x * Φ2.normSq x - + lam₄ * ‖Φ1.innerProd Φ2 x‖ - + (1/2 * lam₅ * (Φ1.innerProd Φ2) x ^ 2 + 1/2 * conj lam₅ * (Φ2.innerProd Φ1) x ^ 2).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 +/-- The potential of the two Higgs doublet model. -/ +def potential (Φ1 Φ2 : HiggsField) (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ) + (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ) (x : SpaceTime) : ℝ := + 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 + + 1/2 * 𝓵₁ * ‖Φ1‖_H ^ 2 x * ‖Φ1‖_H ^ 2 x + 1/2 * 𝓵₂ * ‖Φ2‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x + + 𝓵₃ * ‖Φ1‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x + + 𝓵₄ * ‖⟪Φ1, Φ2⟫_H x‖ ^ 2 + (1/2 * 𝓵₅ * ⟪Φ1, Φ2⟫_H x ^ 2 + 1/2 * conj 𝓵₅ * ⟪Φ2, Φ1⟫_H x ^ 2).re + + (𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj 𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re + + (𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj 𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H 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 diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean index 70f15e4..d9ad6c8 100644 --- a/HepLean/StandardModel/HiggsBoson/Basic.lean +++ b/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] - ring +/-! + +## Constant higgs fields + +-/ /-- A higgs field is constant if it is equal for all `x` `y` in `spaceTime`. -/ def IsConst (Φ : HiggsField) : Prop := ∀ x y, Φ x = Φ y diff --git a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean index b494d1c..d562b72 100644 --- a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean +++ b/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) ℂ := diff --git a/docs/references.bib b/docs/references.bib index 6022c68..44c329a 100644 --- a/docs/references.bib +++ b/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},