/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.StandardModel.Basic import Mathlib.Data.Complex.Exponential import Mathlib.Tactic.Polyrith import Mathlib.Geometry.Manifold.VectorBundle.Basic import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.RepresentationTheory.Basic import Mathlib.Analysis.InnerProductSpace.Basic import Mathlib.Geometry.Manifold.ContMDiff.Product import Mathlib.Analysis.Complex.RealDeriv import Mathlib.Analysis.Calculus.Deriv.Add import Mathlib.Analysis.Calculus.Deriv.Pow import Mathlib.Algebra.QuadraticDiscriminant /-! # The Higgs field This file defines the basic properties for the higgs field in the standard model. -/ universe v u namespace StandardModel noncomputable section open Manifold open Matrix open Complex open ComplexConjugate /-- The complex vector space in which the Higgs field takes values. -/ abbrev higgsVec := EuclideanSpace ℂ (Fin 2) /-- The trivial vector bundle 𝓡² × ℂ². (TODO: Make associated bundle.) -/ abbrev higgsBundle := Bundle.Trivial spaceTime higgsVec instance : SmoothVectorBundle higgsVec higgsBundle (𝓡 4) := Bundle.Trivial.smoothVectorBundle higgsVec 𝓘(ℝ, spaceTime) /-- A higgs field is a smooth section of the higgs bundle. -/ abbrev higgsField : Type := SmoothSection (𝓡 4) higgsVec higgsBundle instance : NormedAddCommGroup (Fin 2 → ℂ) := by exact Pi.normedAddCommGroup section higgsVec /-- The continous linear map from the vector space `higgsVec` to `(Fin 2 → ℂ)` acheived by casting vectors. -/ def higgsVecToFin2ℂ : higgsVec →L[ℝ] (Fin 2 → ℂ) where toFun x := x map_add' x y := by simp map_smul' a x := by simp lemma smooth_higgsVecToFin2ℂ : Smooth 𝓘(ℝ, higgsVec) 𝓘(ℝ, Fin 2 → ℂ) higgsVecToFin2ℂ := ContinuousLinearMap.smooth higgsVecToFin2ℂ /-- Given an element of `gaugeGroup` the linear automorphism of `higgsVec` it gets taken to. -/ @[simps!] noncomputable def higgsRepMap (g : guageGroup) : higgsVec →ₗ[ℂ] higgsVec where toFun S := (g.2.2 ^ 3) • (g.2.1.1 *ᵥ S) map_add' S T := by simp [Matrix.mulVec_add, smul_add] rw [Matrix.mulVec_add, smul_add] map_smul' a S := by simp [Matrix.mulVec_smul] rw [Matrix.mulVec_smul] exact smul_comm _ _ _ /-- The representation of the SM guage group acting on `ℂ²`. -/ noncomputable def higgsRep : Representation ℂ guageGroup higgsVec where toFun := higgsRepMap map_mul' U V := by apply LinearMap.ext intro S simp only [higgsRepMap, Prod.snd_mul, Submonoid.coe_inf, Prod.fst_mul, Submonoid.coe_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply, LinearMap.map_smul_of_tower, mulVec_mulVec] simp [mul_pow, smul_smul, mul_comm] map_one' := by apply LinearMap.ext intro S simp only [higgsRepMap, LinearMap.mul_apply, AddHom.coe_mk, LinearMap.coe_mk] change 1 ^ 3 • (1 *ᵥ _) = _ rw [one_pow, Matrix.one_mulVec] simp only [one_smul, LinearMap.one_apply] namespace higgsVec /-- Given a vector `ℂ²` the constant higgs field with value equal to that section. -/ noncomputable def toField (φ : higgsVec) : higgsField where toFun := fun _ => φ contMDiff_toFun := by intro x rw [Bundle.contMDiffAt_section] exact smoothAt_const /-- The higgs potential for `higgsVec`, i.e. for constant higgs fields. -/ def potential (μSq lambda : ℝ) (φ : higgsVec) : ℝ := - μSq * ‖φ‖ ^ 2 + lambda * ‖φ‖ ^ 4 lemma potential_snd_term_nonneg {lambda : ℝ} (hLam : 0 < lambda) (φ : higgsVec) : 0 ≤ lambda * ‖φ‖ ^ 4 := by rw [mul_nonneg_iff] apply Or.inl simp_all only [ge_iff_le, norm_nonneg, pow_nonneg, and_true] exact le_of_lt hLam lemma potential_as_quad (μSq lambda : ℝ) (φ : higgsVec) : lambda * ‖φ‖ ^ 2 * ‖φ‖ ^ 2 + (- μSq ) * ‖φ‖ ^ 2 + (- potential μSq lambda φ ) = 0 := by simp [potential] ring lemma zero_le_potential_discrim (μSq lambda : ℝ) (φ : higgsVec) (hLam : 0 < lambda) : 0 ≤ discrim (lambda ) (- μSq ) (- potential μSq lambda φ) := by have h1 := potential_as_quad μSq lambda φ rw [quadratic_eq_zero_iff_discrim_eq_sq] at h1 rw [h1] exact sq_nonneg (2 * (lambda ) * ‖φ‖ ^ 2 + -μSq) simp only [ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false] exact ne_of_gt hLam lemma potential_eq_zero_sol (μSq lambda : ℝ) (hLam : 0 < lambda)(φ : higgsVec) (hV : potential μSq lambda φ = 0) : φ = 0 ∨ ‖φ‖ ^ 2 = μSq / lambda := by have h1 := potential_as_quad μSq lambda φ rw [hV] at h1 have h2 : ‖φ‖ ^ 2 * (lambda * ‖φ‖ ^ 2 + -μSq ) = 0 := by linear_combination h1 simp at h2 cases' h2 with h2 h2 simp_all apply Or.inr field_simp at h2 ⊢ ring_nf linear_combination h2 lemma potential_eq_zero_sol_of_μSq_nonpos {μSq lambda : ℝ} (hLam : 0 < lambda) (hμSq : μSq ≤ 0) (φ : higgsVec) (hV : potential μSq lambda φ = 0) : φ = 0 := by cases' (potential_eq_zero_sol μSq lambda hLam φ hV) with h1 h1 exact h1 by_cases hμSqZ : μSq = 0 simpa [hμSqZ] using h1 refine ((?_ : ¬ 0 ≤ μSq / lambda) (?_)).elim · simp_all [div_nonneg_iff] intro h exact lt_imp_lt_of_le_imp_le (fun _ => h) (lt_of_le_of_ne hμSq hμSqZ) · rw [← h1] exact sq_nonneg ‖φ‖ lemma potential_bounded_below (μSq lambda : ℝ) (hLam : 0 < lambda) (φ : higgsVec) : - μSq ^ 2 / (4 * lambda) ≤ potential μSq lambda φ := by have h1 := zero_le_potential_discrim μSq lambda φ hLam simp [discrim] at h1 ring_nf at h1 rw [← neg_le_iff_add_nonneg'] at h1 have h3 : lambda * potential μSq lambda φ * 4 = (4 * lambda) * potential μSq lambda φ := by ring rw [h3] at h1 have h2 := (div_le_iff' (by simp [hLam] : 0 < 4 * lambda )).mpr h1 ring_nf at h2 ⊢ exact h2 lemma potential_bounded_below_of_μSq_nonpos {μSq lambda : ℝ} (hLam : 0 < lambda) (hμSq : μSq ≤ 0) (φ : higgsVec) : 0 ≤ potential μSq lambda φ := by simp only [potential, neg_mul, add_zero] refine add_nonneg ?_ (potential_snd_term_nonneg hLam φ) field_simp rw [@mul_nonpos_iff] simp_all only [ge_iff_le, norm_nonneg, pow_nonneg, and_self, or_true] lemma potential_eq_bound_discrim_zero (μSq lambda : ℝ) (hLam : 0 < lambda)(φ : higgsVec) (hV : potential μSq lambda φ = - μSq ^ 2 / (4 * lambda)) : discrim (lambda) (- μSq) (- potential μSq lambda φ) = 0 := by simp [discrim, hV] field_simp ring lemma potential_eq_bound_higgsVec_sq (μSq lambda : ℝ) (hLam : 0 < lambda)(φ : higgsVec) (hV : potential μSq lambda φ = - μSq ^ 2 / (4 * lambda)) : ‖φ‖ ^ 2 = μSq / (2 * lambda) := by have h1 := potential_as_quad μSq lambda φ rw [quadratic_eq_zero_iff_of_discrim_eq_zero _ (potential_eq_bound_discrim_zero μSq lambda hLam φ hV)] at h1 rw [h1] field_simp ring_nf simp only [ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false] exact ne_of_gt hLam lemma potential_eq_bound_iff (μSq lambda : ℝ) (hLam : 0 < lambda)(φ : higgsVec) : potential μSq lambda φ = - μSq ^ 2 / (4 * lambda) ↔ ‖φ‖ ^ 2 = μSq / (2 * lambda) := by apply Iff.intro · intro h exact potential_eq_bound_higgsVec_sq μSq lambda hLam φ h · intro h have hv : ‖φ‖ ^ 4 = ‖φ‖ ^ 2 * ‖φ‖ ^ 2 := by ring_nf field_simp [potential, hv, h] ring lemma potential_eq_bound_iff_of_μSq_nonpos {μSq lambda : ℝ} (hLam : 0 < lambda) (hμSq : μSq ≤ 0) (φ : higgsVec) : potential μSq lambda φ = 0 ↔ φ = 0 := by apply Iff.intro · intro h exact potential_eq_zero_sol_of_μSq_nonpos hLam hμSq φ h · intro h simp [potential, h] lemma potential_eq_bound_IsMinOn (μSq lambda : ℝ) (hLam : 0 < lambda) (φ : higgsVec) (hv : potential μSq lambda φ = - μSq ^ 2 / (4 * lambda)) : IsMinOn (potential μSq lambda) Set.univ φ := by rw [isMinOn_univ_iff] intro x rw [hv] exact potential_bounded_below μSq lambda hLam x lemma potential_eq_bound_IsMinOn_of_μSq_nonpos {μSq lambda : ℝ} (hLam : 0 < lambda) (hμSq : μSq ≤ 0) (φ : higgsVec) (hv : potential μSq lambda φ = 0) : IsMinOn (potential μSq lambda) Set.univ φ := by rw [isMinOn_univ_iff] intro x rw [hv] exact potential_bounded_below_of_μSq_nonpos hLam hμSq x lemma potential_bound_reached_of_μSq_nonneg {μSq lambda : ℝ} (hLam : 0 < lambda) (hμSq : 0 ≤ μSq) : ∃ (φ : higgsVec), potential μSq lambda φ = - μSq ^ 2 / (4 * lambda) := by use ![√(μSq/(2 * lambda)), 0] refine (potential_eq_bound_iff μSq lambda hLam _).mpr ?_ simp [@PiLp.norm_sq_eq_of_L2, Fin.sum_univ_two] field_simp [mul_pow] lemma IsMinOn_potential_iff_of_μSq_nonneg {μSq lambda : ℝ} (hLam : 0 < lambda) (hμSq : 0 ≤ μSq) : IsMinOn (potential μSq lambda) Set.univ φ ↔ ‖φ‖ ^ 2 = μSq /(2 * lambda) := by apply Iff.intro · intro h obtain ⟨φm, hφ⟩ := potential_bound_reached_of_μSq_nonneg hLam hμSq have hm := isMinOn_univ_iff.mp h φm rw [hφ] at hm have h1 := potential_bounded_below μSq lambda hLam φ rw [← potential_eq_bound_iff μSq lambda hLam φ] exact (Real.partialOrder.le_antisymm _ _ h1 hm).symm · intro h rw [← potential_eq_bound_iff μSq lambda hLam φ] at h exact potential_eq_bound_IsMinOn μSq lambda hLam φ h lemma IsMinOn_potential_iff_of_μSq_nonpos {μSq lambda : ℝ} (hLam : 0 < lambda) (hμSq : μSq ≤ 0) : IsMinOn (potential μSq lambda) Set.univ φ ↔ φ = 0 := by apply Iff.intro · intro h have h0 := isMinOn_univ_iff.mp h 0 rw [(potential_eq_bound_iff_of_μSq_nonpos hLam hμSq 0).mpr (by rfl)] at h0 have h1 := potential_bounded_below_of_μSq_nonpos hLam hμSq φ rw [← (potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ)] exact (Real.partialOrder.le_antisymm _ _ h1 h0).symm · intro h rw [← potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ] at h exact potential_eq_bound_IsMinOn_of_μSq_nonpos hLam hμSq φ h end higgsVec end higgsVec namespace higgsField open Complex Real /-- Given a `higgsField`, the corresponding map from `spaceTime` to `higgsVec`. -/ def toHiggsVec (φ : higgsField) : spaceTime → higgsVec := φ lemma toHiggsVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, higgsVec) φ.toHiggsVec := by intro x0 have h1 := φ.contMDiff x0 rw [Bundle.contMDiffAt_section] at h1 have h2 : (fun x => ((trivializationAt higgsVec (Bundle.Trivial spaceTime higgsVec) x0) { proj := x, snd := φ x }).2) = φ := by rfl simp only [h2] at h1 exact h1 lemma toField_toHiggsVec_apply (φ : higgsField) (x : spaceTime) : (φ.toHiggsVec x).toField x = φ x := by rfl lemma higgsVecToFin2ℂ_toHiggsVec (φ : higgsField) : higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := by ext x rfl lemma toVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ := by rw [← φ.higgsVecToFin2ℂ_toHiggsVec] exact Smooth.comp smooth_higgsVecToFin2ℂ (φ.toHiggsVec_smooth) lemma apply_smooth (φ : higgsField) : ∀ i, Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℂ) (fun (x : spaceTime) => (φ x i)) := by rw [← smooth_pi_space] exact φ.toVec_smooth lemma apply_re_smooth (φ : higgsField) (i : Fin 2): Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (reCLM ∘ (fun (x : spaceTime) => (φ x i))) := Smooth.comp (ContinuousLinearMap.smooth reCLM) (φ.apply_smooth i) lemma apply_im_smooth (φ : higgsField) (i : Fin 2): Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : spaceTime) => (φ x i))) := Smooth.comp (ContinuousLinearMap.smooth imCLM) (φ.apply_smooth i) /-- 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 only [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add] rw [@norm_sq_eq_inner ℂ] simp lemma normSq_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) φ.normSq := by rw [normSq_expand] refine Smooth.add ?_ ?_ simp only [mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add] refine Smooth.add ?_ ?_ refine Smooth.smul ?_ ?_ exact φ.apply_re_smooth 0 exact φ.apply_re_smooth 0 refine Smooth.smul ?_ ?_ exact φ.apply_im_smooth 0 exact φ.apply_im_smooth 0 simp only [mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add] refine Smooth.add ?_ ?_ refine Smooth.smul ?_ ?_ exact φ.apply_re_smooth 1 exact φ.apply_re_smooth 1 refine Smooth.smul ?_ ?_ exact φ.apply_im_smooth 1 exact φ.apply_im_smooth 1 lemma normSq_nonneg (φ : higgsField) (x : spaceTime) : 0 ≤ φ.normSq x := by simp only [normSq, ge_iff_le, norm_nonneg, pow_nonneg] lemma normSq_zero (φ : higgsField) (x : spaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by simp only [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.add (Smooth.neg (Smooth.smul smooth_const φ.normSq_smooth)) (Smooth.smul (Smooth.smul smooth_const φ.normSq_smooth) φ.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 /-- A higgs field is constant if it is equal for all `x` `y` in `spaceTime`. -/ def isConst (Φ : higgsField) : Prop := ∀ x y, Φ x = Φ y lemma isConst_of_higgsVec (φ : higgsVec) : φ.toField.isConst := by intro x _ simp [higgsVec.toField] lemma isConst_iff_of_higgsVec (Φ : higgsField) : Φ.isConst ↔ ∃ (φ : higgsVec), Φ = φ.toField := by apply Iff.intro intro h use Φ 0 ext x y rw [← h x 0] rfl intro h intro x y obtain ⟨φ, hφ⟩ := h subst hφ rfl lemma normSq_of_higgsVec (φ : higgsVec) :φ.toField.normSq = fun x => (norm φ) ^ 2 := by simp only [normSq, higgsVec.toField] funext x simp lemma potential_of_higgsVec (φ : higgsVec) (μSq lambda : ℝ ) : φ.toField.potential μSq lambda = fun _ => higgsVec.potential μSq lambda φ := by simp [higgsVec.potential] unfold potential rw [normSq_of_higgsVec] funext x simp only [neg_mul, add_right_inj] ring_nf end higgsField end end StandardModel