From 0bb8a97d53d46d052a8d8093f3aa7819e7ece436 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 7 May 2024 08:50:08 -0400
Subject: [PATCH] refactor: higgs fields

---
 HepLean/StandardModel/HiggsField.lean | 483 ++++++++++++--------------
 1 file changed, 223 insertions(+), 260 deletions(-)

diff --git a/HepLean/StandardModel/HiggsField.lean b/HepLean/StandardModel/HiggsField.lean
index b5f7fae..f4c845c 100644
--- a/HepLean/StandardModel/HiggsField.lean
+++ b/HepLean/StandardModel/HiggsField.lean
@@ -93,6 +93,184 @@ noncomputable def higgsRep : Representation ℂ guageGroup higgsVec where
     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
@@ -101,6 +279,7 @@ 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
@@ -112,6 +291,10 @@ lemma toHiggsVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ
   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
@@ -120,24 +303,27 @@ lemma toVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, Fin
   rw [← φ.higgsVecToFin2ℂ_toHiggsVec]
   exact Smooth.comp smooth_higgsVecToFin2ℂ (φ.toHiggsVec_smooth)
 
-lemma comp_smooth (φ : higgsField) :
+lemma apply_smooth (φ : higgsField) :
     ∀ i, Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℂ) (fun (x : spaceTime) => (φ x i)) := by
   rw [← smooth_pi_space]
   exact φ.toVec_smooth
 
-lemma comp_re_smooth (φ : higgsField) (i : Fin 2):
+lemma apply_re_smooth (φ : higgsField) (i : Fin 2):
     Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (reCLM ∘ (fun (x : spaceTime) =>  (φ x i))) :=
-  Smooth.comp (ContinuousLinearMap.smooth reCLM) (φ.comp_smooth i)
+  Smooth.comp (ContinuousLinearMap.smooth reCLM) (φ.apply_smooth i)
 
-lemma comp_im_smooth (φ : higgsField) (i : Fin 2):
+lemma apply_im_smooth (φ : higgsField) (i : Fin 2):
     Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : spaceTime) =>  (φ x i))) :=
-  Smooth.comp (ContinuousLinearMap.smooth imCLM) (φ.comp_smooth 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
@@ -151,19 +337,19 @@ lemma normSq_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, 
   simp only [mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add]
   refine Smooth.add ?_ ?_
   refine Smooth.smul ?_ ?_
-  exact φ.comp_re_smooth 0
-  exact φ.comp_re_smooth 0
+  exact φ.apply_re_smooth 0
+  exact φ.apply_re_smooth 0
   refine Smooth.smul ?_ ?_
-  exact φ.comp_im_smooth 0
-  exact φ.comp_im_smooth 0
+  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 φ.comp_re_smooth 1
-  exact φ.comp_re_smooth 1
+  exact φ.apply_re_smooth 1
+  exact φ.apply_re_smooth 1
   refine Smooth.smul ?_ ?_
-  exact φ.comp_im_smooth 1
-  exact φ.comp_im_smooth 1
+  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]
@@ -176,7 +362,7 @@ lemma normSq_zero (φ : higgsField) (x : spaceTime) : φ.normSq x = 0 ↔ φ x =
 def potential (φ : higgsField) (μSq lambda : ℝ ) (x : spaceTime) :  ℝ :=
   - μSq * φ.normSq x + lambda * φ.normSq x * φ.normSq x
 
-lemma potential_smooth (φ : higgsField) (μSq lambda : ℝ ) :
+lemma potential_smooth (φ : higgsField) (μSq lambda : ℝ) :
     Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (fun x => φ.potential μSq lambda x) := by
   simp only [potential, normSq, neg_mul]
   exact Smooth.add
@@ -184,257 +370,20 @@ lemma potential_smooth (φ : higgsField) (μSq lambda : ℝ ) :
     (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
 
-/-- Given a vector `ℂ²` the constant higgs field with value equal to that
-section. -/
-noncomputable def const (φ : higgsVec) : higgsField where
-  toFun := fun _ => φ
-  contMDiff_toFun := by
-    intro x
-    rw [Bundle.contMDiffAt_section]
-    exact smoothAt_const
-
-lemma normSq_const (φ : higgsVec) : (const φ).normSq = fun x => (norm φ) ^ 2 := by
-  simp only [normSq, const]
-  funext x
-  simp
-
-lemma potential_const (φ : higgsVec) (μSq lambda : ℝ ) :
-    (const φ).potential μSq lambda = fun x => - μSq * (norm φ) ^ 2 + lambda * (norm φ) ^ 4 := by
-  unfold potential
-  rw [normSq_const]
-  ring_nf
-
-/-- Given a element `v : ℝ` the `higgsField` `(0, v/√2)`. -/
-def constStd (v : ℝ) : higgsField := const ![0, v/√2]
-
-lemma normSq_constStd (v : ℝ) : (constStd v).normSq = fun x => v ^ 2 / 2 := by
-  simp only [normSq_const, constStd]
-  funext x
-  rw [@PiLp.norm_sq_eq_of_L2]
-  rw [Fin.sum_univ_two]
-  simp
-
-/-- The higgs potential as a function of `v : ℝ` when evaluated on a `constStd` field. -/
-def potentialConstStd (μSq lambda v : ℝ) : ℝ := - μSq /2 * v ^ 2  + lambda /4 * v ^ 4
-
-lemma potential_constStd (v μSq lambda : ℝ) :
-    (constStd v).potential μSq lambda = fun _ => potentialConstStd μSq lambda v := by
-  unfold potential potentialConstStd
-  rw [normSq_constStd]
-  simp only [neg_mul]
-  ring_nf
-
-lemma smooth_potentialConstStd (μSq lambda : ℝ) :
-    Smooth 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (fun v => potentialConstStd μSq lambda v) := by
-  simp only [potentialConstStd]
-  have h1 (v : ℝ) : v ^ 4 = v * v * v * v := by
-    ring
-  simp [sq, h1]
-  refine Smooth.add ?_ ?_
-  exact Smooth.smul smooth_const (Smooth.smul smooth_id smooth_id)
-  exact Smooth.smul smooth_const
-    (Smooth.smul (Smooth.smul (Smooth.smul smooth_id smooth_id)  smooth_id)  smooth_id)
-
-
-lemma deriv_potentialConstStd (μSq lambda v : ℝ) :
-    deriv (fun v => potentialConstStd μSq lambda v) v = - μSq * v + lambda * v ^ 3 := by
-  simp only [potentialConstStd]
-  rw [deriv_add, deriv_mul, deriv_mul,  deriv_const, deriv_const, deriv_pow, deriv_pow]
-  simp only [zero_mul, Nat.cast_ofNat, Nat.succ_sub_succ_eq_sub, tsub_zero, pow_one, zero_add,
-    neg_mul]
-  ring
-  exact differentiableAt_const _
-  exact differentiableAt_pow _
-  exact differentiableAt_const _
-  exact differentiableAt_pow _
-  exact DifferentiableAt.const_mul (differentiableAt_pow _) _
-  exact DifferentiableAt.const_mul (differentiableAt_pow _) _
-
-lemma deriv_potentialConstStd_zero (μSq lambda v : ℝ) (hLam : 0 < lambda)
-    (hv : deriv (fun v => potentialConstStd μSq lambda v) v = 0) : v = 0 ∨ v ^ 2 = μSq/lambda:= by
-  rw [deriv_potentialConstStd] at hv
-  ring_nf at hv
-  have h1 : v * (- μSq + lambda * v ^ 2) = 0 := by
-    ring_nf
-    linear_combination hv
-  simp at h1
-  cases'  h1 with h1 h1
-  simp_all
-  apply Or.inr
-  field_simp
-  linear_combination h1
-
-lemma potentialConstStd_bounded' (μSq lambda v x : ℝ) (hLam : 0 < lambda) :
-    potentialConstStd μSq lambda v = x → - μSq ^ 2 / (4  * lambda) ≤ x  := by
-  simp only [potentialConstStd]
-  intro h
-  let y := v ^2
-  have h1 :  lambda / 4 * y * y + (- μSq / 2) * y + (-x) = 0 := by
-    simp [y]
-    linear_combination h
-  rw [quadratic_eq_zero_iff_discrim_eq_sq] at h1
-  simp [discrim] at h1
-  have h2 : 0 ≤ μSq ^ 2 / 2 ^ 2 + 4 * (lambda / 4) * x  := by
-    rw [h1]
-    exact sq_nonneg (2 * (lambda / 4) * y + -μSq / 2)
-  ring_nf at h2
-  rw [← neg_le_iff_add_nonneg'] at h2
-  have h4 :=  (div_le_iff' hLam).mpr h2
-  ring_nf at h4
-  ring_nf
-  exact h4
-  simp only [ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
-  exact OrderIso.mulLeft₀.proof_1 lambda hLam
-
-lemma potentialConstStd_bounded (μSq lambda v : ℝ) (hLam : 0 < lambda) :
-    - μSq ^ 2 / (4  * lambda) ≤ potentialConstStd μSq lambda v := by
-  apply potentialConstStd_bounded' μSq lambda v (potentialConstStd μSq lambda v) hLam
-  rfl
-
-lemma potentialConstStd_IsMinOn_of_eq_bound (μSq lambda v : ℝ) (hLam : 0 < lambda)
-    (hv : potentialConstStd μSq lambda v = - μSq ^ 2 / (4  * lambda)) :
-    IsMinOn (potentialConstStd μSq lambda) Set.univ v := by
-  rw [isMinOn_univ_iff]
-  intro x
-  rw [hv]
-  exact potentialConstStd_bounded μSq lambda x hLam
-
-lemma potentialConstStd_vsq_of_eq_bound (μSq lambda v : ℝ) (hLam : 0 < lambda) :
-    potentialConstStd μSq lambda v = - μSq ^ 2 / (4  * lambda) ↔ v ^ 2 = μSq / lambda := by
-  apply Iff.intro
-  intro h
-  simp [potentialConstStd] at h
-  field_simp at h
-  have h1 :  (8 * lambda ^ 2) * v ^ 2 * v ^ 2 + (- 16 * μSq * lambda ) * v ^ 2
-      + (8 * μSq ^ 2) = 0 := by
-    linear_combination h
-  have hd : discrim (8 * lambda ^ 2) (- 16 * μSq * lambda) (8 * μSq ^ 2) = 0 := by
-    simp [discrim]
-    ring_nf
-  rw [quadratic_eq_zero_iff_of_discrim_eq_zero _ hd] at h1
-  field_simp at h1 ⊢
-  ring_nf at h1
-  have hx :  16 * lambda ≠ 0 := by
-    simp [hLam]
-    exact OrderIso.mulLeft₀.proof_1 lambda hLam
-  apply mul_left_cancel₀ hx
-  ring_nf
-  rw [← h1]
-  ring
-  simp only [ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, false_or]
-  exact OrderIso.mulLeft₀.proof_1 lambda hLam
-  intro h
-  simp [potentialConstStd, h]
-  have hv : v ^ 4 = v^2 * v^2 := by
-    ring
-  rw [hv, h]
-  field_simp
-  ring
-
-lemma potentialConstStd_IsMinOn (μSq lambda v : ℝ) (hLam : 0 < lambda) (hμSq : 0 ≤ μSq) :
-    IsMinOn (potentialConstStd μSq lambda) Set.univ v ↔ v ^ 2 = μSq / lambda := by
-  apply Iff.intro
-  intro h
-  have h1 := potentialConstStd_bounded μSq lambda v hLam
-  rw [isMinOn_univ_iff] at h
-  let vmin := √(μSq / lambda)
-  have hvmin : vmin ^ 2 = μSq / lambda := by
-    simp [vmin]
-    field_simp
-  have h2 := h vmin
-  have h3 := (potentialConstStd_vsq_of_eq_bound μSq lambda vmin hLam).mpr hvmin
-  rw [h3] at h2
-  rw [(potentialConstStd_vsq_of_eq_bound μSq lambda v hLam).mp]
-  exact (Real.partialOrder.le_antisymm _ _ h1 h2).symm
-  intro h
-  rw [← potentialConstStd_vsq_of_eq_bound μSq lambda v hLam] at h
-  exact potentialConstStd_IsMinOn_of_eq_bound μSq lambda v hLam h
-
-
-lemma potentialConstStd_muSq_le_zero_nonneg (μSq lambda v : ℝ) (hLam : 0 < lambda)
-    (hμSq : μSq ≤ 0) : 0 ≤ potentialConstStd μSq lambda v := by
-  simp [potentialConstStd]
-  apply add_nonneg
-  field_simp
-  refine div_nonneg ?_ (by simp)
-  refine neg_nonneg.mpr ?_
-  rw [@mul_nonpos_iff]
-  simp_all
-  apply Or.inr
-  exact sq_nonneg v
-  rw [mul_nonneg_iff]
-  apply Or.inl
-  apply And.intro
-  refine div_nonneg ?_ (by simp)
-  exact le_of_lt hLam
-  have hv : v ^ 4 = (v ^ 2) ^ 2 := by ring
-  rw [hv]
-  exact sq_nonneg (v ^ 2)
-
-lemma potentialConstStd_zero_muSq_le_zero (μSq lambda v : ℝ) (hLam : 0 < lambda)
-    (hμSq : μSq ≤ 0) : potentialConstStd μSq lambda v = 0 ↔ v = 0 := by
-  apply Iff.intro
-  · intro h
-    simp [potentialConstStd] at h
-    field_simp at h
-    have h1 :  v ^ 2 * ((2 * lambda ) * v ^ 2  + (- 4 * μSq  )) = 0 := by
-      linear_combination h
-    simp at h1
-    cases' h1 with h1 h1
-    exact h1
-    have h2 :   v ^ 2 = (4 * μSq) / (2 * lambda) := by
-      field_simp
-      ring_nf
-      linear_combination h1
-    by_cases hμSqZ : μSq = 0
-    rw [hμSqZ] at h2
-    simpa using h2
-    have h3 :  ¬ (0 ≤ 4 * μSq / (2 * lambda)) := by
-      rw [div_nonneg_iff]
-      simp only [gt_iff_lt, Nat.ofNat_pos, mul_nonneg_iff_of_pos_left]
-      rw [not_or]
-      apply And.intro
-      simp only [not_and, not_le]
-      intro hm
-      exact (hμSqZ (le_antisymm hμSq hm)).elim
-      simp only [not_and, not_le, gt_iff_lt, Nat.ofNat_pos, mul_pos_iff_of_pos_left]
-      intro _
-      simp_all only [true_or]
-    rw [← h2] at h3
-    refine (h3 ?_).elim
-    exact sq_nonneg v
-  · intro h
-    simp [potentialConstStd, h]
-
-
-lemma potentialConstStd_IsMinOn_muSq_le_zero (μSq lambda v : ℝ) (hLam : 0 < lambda)
-    (hμSq : μSq ≤ 0) :
-    IsMinOn (potentialConstStd μSq lambda) Set.univ v ↔ v = 0 := by
-  have hx := (potentialConstStd_zero_muSq_le_zero μSq lambda 0 hLam hμSq)
-  simp at hx
-  apply Iff.intro
-  intro h
-  rw [isMinOn_univ_iff] at h
-  have h1 := potentialConstStd_muSq_le_zero_nonneg μSq lambda v hLam hμSq
-  have h2 := h 0
-  rw [hx] at h2
-  exact (potentialConstStd_zero_muSq_le_zero μSq lambda v hLam hμSq).mp
-    (Real.partialOrder.le_antisymm _ _ h1 h2).symm
-  intro h
-  rw [h, isMinOn_univ_iff, hx]
-  intro x
-  exact potentialConstStd_muSq_le_zero_nonneg μSq lambda x hLam hμSq
-
-
-
-lemma const_isConst (φ : Fin 2 → ℂ) : (const φ).isConst := by
+lemma isConst_of_higgsVec (φ : higgsVec) : φ.toField.isConst := by
   intro x _
-  simp [const]
+  simp [higgsVec.toField]
 
-lemma isConst_iff_exists_const (Φ : higgsField) : Φ.isConst ↔ ∃ φ, Φ = const φ := by
+lemma isConst_iff_of_higgsVec (Φ : higgsField) : Φ.isConst ↔ ∃ (φ : higgsVec), Φ = φ.toField := by
   apply Iff.intro
   intro h
   use Φ 0
@@ -447,6 +396,20 @@ lemma isConst_iff_exists_const (Φ : higgsField) : Φ.isConst ↔ ∃ φ, Φ = c
   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