diff --git a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
index 7f2660fc0..e8ad0d75f 100644
--- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
+++ b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
@@ -6,18 +6,67 @@ Authors: Joseph Tooby-Smith
 import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.GramMatrix
 /-!
 
-# The potential of the two Higgs doublet model
+# The potential of the Two Higgs doublet model
 
 ## i. Overview
 
-In this file we give the potential of the two Higgs doublet model (2HDM) in Lean, and derive
-properties thereof.
+In this module we give the define the parameters of the 2HDM potential, and
+give stability properties of the potential.
+
+## ii. Key results
+
+- `PotentialParameters` : The parameters of the 2HDM potential.
+- `massTerm` : The mass term of the 2HDM potential.
+- `quarticTerm` : The quartic term of the 2HDM potential.
+- `potential` : The full potential of the 2HDM.
+- `PotentialIsStable` : The condition that the potential is stable.
+
+## iii. Table of contents
+
+- A. The parameters of the potential
+  - A.1. The potential parameters corresponding to zero
+  - A.2. Gram parameters
+  - A.3. Specific cases
+- B. The mass term
+- C. The quartic term
+- D. The full potential
+- E. Stability of the potential
+  - E.1. The stability condition
+  - E.2. Instability of the stabilityCounterExample potential
+  - E.3. The reduced mass term
+  - E.4. The reduced quartic term
+  - E.5. Stability in terms of the gram vectors
+  - E.6. Strong stability implies stability
+  - E.7. Showing step in hep-ph/0605184 is invalid
+
+## iv. References
+
+For the parameterization of the potential we follow the convention of
+- https://arxiv.org/pdf/1605.03237
+
+Stability arguments of the potential follow, in part, those from
+- https://arxiv.org/abs/hep-ph/0605184
+Although we note that we explicitly prove that one of the steps in this paper is not valid.
 
 -/
 namespace TwoHiggsDoublet
 open InnerProductSpace
 open StandardModel
 
+/-!
+
+## A. The parameters of the potential
+
+We define a type for the parameters of the Higgs potential in the 2HDM.
+
+We follow the convention of `1605.03237`, which is highlighted in the explicit construction
+of the potential itself.
+
+We relate these parameters to the `ξ` and `η` parameters used in the gram vector formalism
+given in arXiv:hep-ph/0605184.
+
+-/
+
 /-- The parameters of the Two Higgs doublet model potential.
   Following the convention of https://arxiv.org/pdf/1605.03237. -/
 structure PotentialParameters where
@@ -44,6 +93,57 @@ structure PotentialParameters where
 
 namespace PotentialParameters
 
+/-!
+
+### A.1. The potential parameters corresponding to zero
+
+We define an instance of `Zero` for the potential parameters, corresponding to all
+parameters being zero, and therefore the potential itself being zero.
+
+-/
+
+instance : Zero PotentialParameters where
+  zero :=
+    { m₁₁2 := 0
+      m₂₂2 := 0
+      m₁₂2 := 0
+      𝓵₁ := 0
+      𝓵₂ := 0
+      𝓵₃ := 0
+      𝓵₄ := 0
+      𝓵₅ := 0
+      𝓵₆ := 0
+      𝓵₇ := 0 }
+
+@[simp] lemma zero_m₁₁2 : (0 : PotentialParameters).m₁₁2 = 0 := rfl
+
+@[simp] lemma zero_m₂₂2 : (0 : PotentialParameters).m₂₂2 = 0 := rfl
+
+@[simp] lemma zero_m₁₂2 : (0 : PotentialParameters).m₁₂2 = 0 := rfl
+
+@[simp] lemma zero_𝓵₁ : (0 : PotentialParameters).𝓵₁ = 0 := rfl
+
+@[simp] lemma zero_𝓵₂ : (0 : PotentialParameters).𝓵₂ = 0 := rfl
+
+@[simp] lemma zero_𝓵₃ : (0 : PotentialParameters).𝓵₃ = 0 := rfl
+
+@[simp] lemma zero_𝓵₄ : (0 : PotentialParameters).𝓵₄ = 0 := rfl
+
+@[simp] lemma zero_𝓵₅ : (0 : PotentialParameters).𝓵₅ = 0 := rfl
+
+@[simp] lemma zero_𝓵₆ : (0 : PotentialParameters).𝓵₆ = 0 := rfl
+
+@[simp] lemma zero_𝓵₇ : (0 : PotentialParameters).𝓵₇ = 0 := rfl
+
+/-!
+
+### A.2. Gram parameters
+
+A reparameterization of the potential parameters corresponding to `ξ` and `η` in
+arXiv:hep-ph/0605184.
+
+-/
+
 /-- A reparameterization of the parameters of the quadratic terms of the
   potential for use with the gramVector. -/
 noncomputable def ξ (P : PotentialParameters) : Fin 1 ⊕ Fin 3 → ℝ := fun μ =>
@@ -53,6 +153,11 @@ noncomputable def ξ (P : PotentialParameters) : Fin 1 ⊕ Fin 3 → ℝ := fun
   | Sum.inr 1 => Complex.im P.m₁₂2
   | Sum.inr 2 => (P.m₁₁2 - P.m₂₂2) / 2
 
+@[simp]
+lemma ξ_zero : (0 : PotentialParameters).ξ = 0 := by
+  ext μ
+  fin_cases μ <;> simp [ξ]
+
 /-- A reparameterization of the parameters of the quartic terms of the
   potential for use with the gramVector. -/
 noncomputable def η (P : PotentialParameters) : Fin 1 ⊕ Fin 3 → Fin 1 ⊕ Fin 3 → ℝ
@@ -78,10 +183,52 @@ lemma η_symm (P : PotentialParameters) (μ ν : Fin 1 ⊕ Fin 3) :
     P.η μ ν = P.η ν μ := by
   fin_cases μ <;> fin_cases ν <;> simp [η]
 
+@[simp]
+lemma η_zero : (0 : PotentialParameters).η = 0 := by
+  ext μ ν
+  fin_cases μ <;> fin_cases ν <;> simp [η]
+
+/-!
+
+### A.3. Specific cases
+
+-/
+
+/-- An example of potential parameters that serve as a counterexample to the stability
+  condition given in arXiv:hep-ph/0605184.
+  This corresponds to the potential:
+  `2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im + ‖H.Φ1 - H.Φ2‖ ^ 4`
+  which has the property that the quartic term is non-negative and only zero if
+  the mass term is also zero, but the potential is not stable.
+  In the proof that `stabilityCounterExample_not_potentialIsStable`, we give
+  explicit vectors `H.Φ1` and `H.Φ2` that show this potential is not stable.
+
+  This is the first occurrence of such a counterexample in the literature to the best of
+  the author's knowledge.
+-/
+def stabilityCounterExample : PotentialParameters := {(0 : PotentialParameters) with
+    m₁₂2 := Complex.I
+    𝓵₁ := 2
+    𝓵₂ := 2
+    𝓵₃ := 2
+    𝓵₄ := 2
+    𝓵₅ := 2
+    𝓵₆ := -2
+    𝓵₇ := -2}
+
 end PotentialParameters
 
 open ComplexConjugate
 
+/-!
+
+## B. The mass term
+
+We define the mass term of the potential, write it in terms of the gram vector,
+and prove that it is gauge invariant.
+
+-/
+
 /-- The mass term of the two Higgs doublet model potential. -/
 noncomputable def massTerm (P : PotentialParameters) (H : TwoHiggsDoublet) : ℝ :=
   P.m₁₁2 * ‖H.Φ1‖ ^ 2 + P.m₂₂2 * ‖H.Φ2‖ ^ 2 -
@@ -100,6 +247,28 @@ lemma gaugeGroupI_smul_massTerm (g : StandardModel.GaugeGroupI) (P : PotentialPa
   rw [massTerm_eq_gramVector, massTerm_eq_gramVector]
   simp
 
+@[simp]
+lemma massTerm_zero : massTerm 0 = 0 := by
+  ext H
+  simp [massTerm]
+
+lemma massTerm_stabilityCounterExample (H : TwoHiggsDoublet) :
+    massTerm PotentialParameters.stabilityCounterExample H =
+    2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im := by
+  simp [massTerm, PotentialParameters.stabilityCounterExample]
+  rw [show ⟪H.Φ2, H.Φ1⟫_ℂ = conj ⟪H.Φ1, H.Φ2⟫_ℂ from Eq.symm (conj_inner_symm H.Φ2 H.Φ1)]
+  rw [Complex.conj_im]
+  ring_nf
+
+/-!
+
+## C. The quartic term
+
+We define the quartic term of the potential, write it in terms of the gram vector,
+and prove that it is gauge invariant.
+
+-/
+
 /-- The quartic term of the two Higgs doublet model potential. -/
 noncomputable def quarticTerm (P : PotentialParameters) (H : TwoHiggsDoublet) : ℝ :=
   1/2 * P.𝓵₁ * ‖H.Φ1‖ ^ 2 * ‖H.Φ1‖ ^ 2 + 1/2 * P.𝓵₂ * ‖H.Φ2‖ ^ 2 * ‖H.Φ2‖ ^ 2
@@ -142,6 +311,82 @@ lemma gaugeGroupI_smul_quarticTerm (g : StandardModel.GaugeGroupI) (P : Potentia
   rw [quarticTerm_eq_gramVector, quarticTerm_eq_gramVector]
   simp
 
+@[simp]
+lemma quarticTerm_zero : quarticTerm 0 = 0 := by
+  ext H
+  simp [quarticTerm]
+
+lemma quarticTerm_stabilityCounterExample (H : TwoHiggsDoublet) :
+    quarticTerm .stabilityCounterExample H =
+    (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2:= by
+  /- Proof by calculation. -/
+  calc _ = (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2
+    + 2 * ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2
+    + (⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + ⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re
+    - 2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ2, H.Φ1⟫_ℂ).re) := by
+        simp [quarticTerm, PotentialParameters.stabilityCounterExample, Complex.add_re,
+          ← Complex.ofReal_pow]
+        ring
+      _ = (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) ^ 2
+      + 4 * (⟪H.Φ1, H.Φ2⟫_ℂ).re ^ 2
+      - 2 * (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2) * ((⟪H.Φ1, H.Φ2⟫_ℂ).re + (⟪H.Φ2, H.Φ1⟫_ℂ).re) := by
+        have h1 : 2 * ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2
+            + (⟪H.Φ1, H.Φ2⟫_ℂ ^ 2 + ⟪H.Φ2, H.Φ1⟫_ℂ ^ 2).re = 4 * (⟪H.Φ1, H.Φ2⟫_ℂ).re ^ 2 := by
+          rw [show ⟪H.Φ2, H.Φ1⟫_ℂ = conj ⟪H.Φ1, H.Φ2⟫_ℂ from Eq.symm (conj_inner_symm H.Φ2 H.Φ1)]
+          generalize ⟪H.Φ1, H.Φ2⟫_ℂ = z
+          have hz : z = z.re + z.im * Complex.I := by exact Eq.symm (Complex.re_add_im z)
+          generalize z.re = x at hz
+          generalize z.im = y at hz
+          subst hz
+          have h0 : ‖↑x + ↑y * Complex.I‖ ^ 2 = x ^ 2 + y ^ 2 := by
+            rw [Complex.norm_add_mul_I, Real.sq_sqrt]
+            positivity
+          rw [h0]
+          simp [Complex.add_re, sq]
+          ring
+        rw [← h1]
+        ring
+      _ = (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 := by
+        rw [show ⟪H.Φ2, H.Φ1⟫_ℂ = conj ⟪H.Φ1, H.Φ2⟫_ℂ from Eq.symm (conj_inner_symm H.Φ2 H.Φ1)]
+        rw [Complex.conj_re]
+        ring
+
+lemma quarticTerm_stabilityCounterExample_eq_norm_pow_four (H : TwoHiggsDoublet) :
+    quarticTerm .stabilityCounterExample H = ‖H.Φ1 - H.Φ2‖ ^ 4 := by
+  /- Proof by calculation. -/
+  calc _
+      _ = (‖H.Φ1‖ ^ 2 + ‖H.Φ2‖ ^ 2 - 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).re) ^ 2 := by
+        rw [quarticTerm_stabilityCounterExample]
+      _ = (‖H.Φ1 - H.Φ2‖ ^ 2) ^ 2 := by
+        congr
+        have h1 (v : HiggsVec) : ‖v‖ ^ 2 = (⟪v, v⟫_ℂ).re := by
+          rw [inner_self_eq_norm_sq_to_K]
+          simp [← Complex.ofReal_pow]
+        rw [h1, h1, h1]
+        simp only [inner_sub_right, inner_sub_left, Complex.sub_re]
+        rw [show ⟪H.Φ2, H.Φ1⟫_ℂ = conj ⟪H.Φ1, H.Φ2⟫_ℂ from Eq.symm (conj_inner_symm H.Φ2 H.Φ1)]
+        rw [Complex.conj_re]
+        ring
+      _ = ‖H.Φ1 - H.Φ2‖ ^ 4 := by ring
+
+lemma massTerm_zero_of_quarticTerm_zero_stabilityCounterExample (H : TwoHiggsDoublet)
+    (h : quarticTerm .stabilityCounterExample H = 0) :
+    massTerm .stabilityCounterExample H = 0 := by
+  rw [quarticTerm_stabilityCounterExample_eq_norm_pow_four] at h
+  rw [massTerm_stabilityCounterExample]
+  simp at h
+  have h1 : H.Φ1 = H.Φ2 := by grind
+  simp [← Complex.ofReal_pow, h1]
+
+/-!
+
+## D. The full potential
+
+We define the full potential as the sum of the mass and quartic terms,
+and prove that it is gauge invariant.
+
+-/
+
 /-- The potential of the two Higgs doublet model. -/
 noncomputable def potential (P : PotentialParameters) (H : TwoHiggsDoublet) : ℝ :=
   massTerm P H + quarticTerm P H
@@ -152,18 +397,243 @@ lemma gaugeGroupI_smul_potential (g : StandardModel.GaugeGroupI)
     potential P (g • H) = potential P H := by
   rw [potential, potential]
   simp
+
+@[simp]
+lemma potential_zero : potential 0 = 0 := by
+  ext H
+  simp [potential]
+
+lemma potential_stabilityCounterExample (H : TwoHiggsDoublet) :
+    potential .stabilityCounterExample H = 2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im + ‖H.Φ1 - H.Φ2‖ ^ 4 := by
+  simp [potential, massTerm_stabilityCounterExample,
+    quarticTerm_stabilityCounterExample_eq_norm_pow_four]
+
 /-!
 
-## Boundedness of the potential
+## E. Stability of the potential
 
 -/
 
-/-- The condition that the potential is bounded from below. -/
-def PotentialIsBounded (P : PotentialParameters) : Prop :=
+/-!
+
+### E.1. The stability condition
+
+We define the condition that the potential is stable, that is, bounded from below.
+
+-/
+
+/-- The condition that the potential is stable. -/
+def PotentialIsStable (P : PotentialParameters) : Prop :=
   ∃ c : ℝ, ∀ H : TwoHiggsDoublet, c ≤ potential P H
 
-lemma potentialIsBounded_iff_forall_gramVector (P : PotentialParameters) :
-    PotentialIsBounded P ↔ ∃ c : ℝ, ∀ K : Fin 1 ⊕ Fin 3 → ℝ, 0 ≤ K (Sum.inl 0) →
+/-!
+
+### E.2. Instability of the stabilityCounterExample potential
+
+-/
+
+open Real
+
+/-- The potential `stabilityCounterExample` is not stable. -/
+lemma stabilityCounterExample_not_potentialIsStable :
+    ¬ PotentialIsStable .stabilityCounterExample := by
+  simp [PotentialIsStable]
+  intro c
+  /- The angle t and properties thereof. -/
+  let t := Real.arctan (2 * Real.sqrt (|c| + 1))⁻¹
+  have t_pos : 0 < t := by
+    simp [t]
+    grind
+  have t_le_pi_div_2 : t ≤ Real.pi / 2 := by
+    simpa [t] using le_of_lt <| arctan_lt_pi_div_two ((√(|c| + 1))⁻¹ * 2⁻¹)
+  have t_ne_zero : t ≠ 0 := by
+    simp [t]
+    grind
+  have sin_t_pos : 0 < sin t := by
+    simp [t]
+    grind
+  have cos_t_pos : 0 < cos t := by
+    simp [t]
+    exact cos_arctan_pos ((√(|c| + 1))⁻¹ * 2⁻¹)
+  have t_mul_sin_t_nonneg : 0 ≤ 2 * t * sin t - t ^ 2 := by
+    rw [sub_nonneg]
+    trans 2 * t * (2 / Real.pi * t)
+    · ring_nf
+      rw [mul_assoc]
+      apply le_mul_of_one_le_right
+      · positivity
+      · field_simp
+        exact Real.pi_le_four
+    · have := Real.mul_le_sin (le_of_lt t_pos) t_le_pi_div_2
+      nlinarith
+  /- The Two Higgs doublet violating stability.
+    The two Higgs doublet is constructed so that for the gram vector
+    `v` we have:
+    - `v₀ = cos t/(2 * t * (sin t)^2)`
+    - `v₁/v₀ = (1 - t * sin t)`
+    - `v₂/v₀ = - t * cos t`
+    - `v₃ = 0` -/
+  let H : TwoHiggsDoublet := {
+    Φ1 := !₂[√(cos t/(4 * t * (sin t)^2)), 0]
+    Φ2 := √(cos t/(4 * t * (sin t)^2)) • !₂[1 - t * sin t - Complex.I * t * cos t,
+      √(2 * t * sin t - t ^ 2)] }
+  have Φ1_norm_sq : ‖H.Φ1‖ ^ 2 = cos t/(4 * t * (sin t)^2) := by
+    simp [H, PiLp.norm_sq_eq_of_L2]
+    rw [sq_sqrt]
+    positivity
+  have Φ2_norm_sq : ‖H.Φ2‖ ^ 2 = cos t/(4 * t * (sin t)^2) := by
+    simp [H, norm_smul, mul_pow]
+    rw [sq_sqrt (by positivity)]
+    simp [PiLp.norm_sq_eq_of_L2]
+    rw [sq_sqrt (by positivity)]
+    have h0 : ‖1 - ↑t * Complex.sin ↑t - Complex.I * ↑t * Complex.cos ↑t‖ ^ 2 =
+        1 + t ^ 2 - 2 * t * sin t := by
+      rw [← Complex.normSq_eq_norm_sq]
+      trans Complex.normSq (Complex.ofReal (1 - t * sin t) +
+        Complex.ofReal (-t * cos t) * Complex.I)
+      · simp
+        ring_nf
+      rw [Complex.normSq_add_mul_I]
+      trans 1 + t ^2 * (sin t ^2 + cos t ^2) - 2 *(t * sin t)
+      · ring
+      rw [sin_sq_add_cos_sq]
+      ring
+    rw [h0]
+    field_simp
+    ring
+  have Φ1_inner_Φ2 : ⟪H.Φ1, H.Φ2⟫_ℂ = Complex.ofReal (cos t/(4 * t * (sin t)^2) *
+      (1 - t * sin t)) + Complex.I *
+      Complex.ofReal (cos t/(4 * t * (sin t)^2) * (- t * cos t)) := by
+    simp [H, PiLp.inner_apply]
+    trans Complex.ofReal ((√(cos t / (4 * t * sin t ^ 2))) ^ 2) *
+        (1 - ↑t * Complex.sin ↑t - Complex.I * ↑t * Complex.cos ↑t)
+    · simp
+      ring
+    rw [sq_sqrt (by positivity)]
+    simp only [Complex.ofReal_div, Complex.ofReal_cos, Complex.ofReal_mul, Complex.ofReal_ofNat,
+      Complex.ofReal_pow, Complex.ofReal_sin]
+    ring
+  have Φ1_inner_Φ2_re : (⟪H.Φ1, H.Φ2⟫_ℂ).re = cos t/(4 * t * (sin t)^2) * (1 - t * sin t) := by
+    rw [Φ1_inner_Φ2, Complex.add_re, Complex.ofReal_re, Complex.re_mul_ofReal]
+    simp
+  have Φ1_inner_Φ2_im : (⟪H.Φ1, H.Φ2⟫_ℂ).im = cos t/(4 * t * (sin t)^2) * (- t * cos t) := by
+    rw [Φ1_inner_Φ2, Complex.add_im, Complex.im_mul_ofReal, Complex.ofReal_im]
+    simp
+  have potential_H_cos_sin : potential .stabilityCounterExample H =
+      - (cos t) ^ 2/ (4 * (sin t)^2) := by
+    rw [potential, massTerm_stabilityCounterExample, quarticTerm_stabilityCounterExample]
+    rw [Φ1_norm_sq, Φ2_norm_sq, Φ1_inner_Φ2_re, Φ1_inner_Φ2_im]
+    field
+  have potential_H_tan : potential .stabilityCounterExample H =
+      - 1/(4 * tan t ^ 2) := by
+    rw [potential_H_cos_sin, tan_eq_sin_div_cos]
+    field
+  have potential_eq_c : potential .stabilityCounterExample H = - (|c| + 1) := by
+    rw [potential_H_tan, tan_arctan]
+    field_simp
+    rw [sq_sqrt (by positivity)]
+    ring
+  /- Proving potential is unbounded. -/
+  use H
+  rw [potential_eq_c]
+  grind
+
+/-!
+
+### E.3. The reduced mass term
+
+The reduced mass term is a function that helps express the stability condition.
+It is the function `J2` in https://arxiv.org/abs/hep-ph/0605184.
+
+-/
+
+/-- A function related to the mass term of the potential, used in the stableness
+  condition and equivalent to the term `J2` in
+  https://arxiv.org/abs/hep-ph/0605184. -/
+noncomputable def massTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ :=
+  P.ξ (Sum.inl 0) + ∑ μ, P.ξ (Sum.inr μ) * k μ
+
+lemma massTermReduced_lower_bound (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3))
+    (hk : ‖k‖ ^ 2 ≤ 1) : P.ξ (Sum.inl 0) - √(∑ a, |P.ξ (Sum.inr a)| ^ 2) ≤ massTermReduced P k := by
+  simp only [Fin.isValue, massTermReduced]
+  have h1 (a b c : ℝ) (h : - b ≤ c) : a - b ≤ a + c:= by grind
+  apply h1
+  let ξEuclid : EuclideanSpace ℝ (Fin 3) := WithLp.toLp 2 (fun a => P.ξ (Sum.inr a))
+  trans - ‖ξEuclid‖
+  · simp [PiLp.norm_eq_of_L2, ξEuclid]
+  trans - (‖k‖ * ‖ξEuclid‖)
+  · simp
+    simp at hk
+    have ha (a b : ℝ) (h : a ≤ 1) (ha : 0 ≤ a) (hb : 0 ≤ b) : a * b ≤ b := by nlinarith
+    apply ha
+    · exact hk
+    · exact norm_nonneg k
+    · exact norm_nonneg ξEuclid
+  trans - ‖⟪k, ξEuclid⟫_ℝ‖
+  · simp
+    exact abs_real_inner_le_norm k ξEuclid
+  trans ⟪k, ξEuclid⟫_ℝ
+  · simp
+    grind
+  simp [PiLp.inner_apply, ξEuclid]
+
+@[simp]
+lemma massTermReduced_zero : massTermReduced 0 = 0 := by
+  ext k
+  simp [massTermReduced]
+
+lemma massTermReduced_stabilityCounterExample (k : EuclideanSpace ℝ (Fin 3)) :
+    massTermReduced .stabilityCounterExample k = k 1 := by
+  simp [massTermReduced, PotentialParameters.ξ, Fin.isValue,
+    PotentialParameters.stabilityCounterExample, Fin.sum_univ_three]
+
+/-!
+
+### E.4. The reduced quartic term
+
+The reduced quartic term is a function that helps express the stability condition.
+It is the function `J4` in https://arxiv.org/abs/hep-ph/0605184.
+
+-/
+
+/-- A function related to the quartic term of the potential, used in the stableness
+  condition and equivalent to the term `J4` in
+  https://arxiv.org/abs/hep-ph/0605184. -/
+noncomputable def quarticTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ :=
+  P.η (Sum.inl 0) (Sum.inl 0) + 2 * ∑ b, k b * P.η (Sum.inl 0) (Sum.inr b) +
+  ∑ a, ∑ b, k a * k b * P.η (Sum.inr a) (Sum.inr b)
+
+@[simp]
+lemma quarticTermReduced_zero : quarticTermReduced 0 = 0 := by
+  ext k
+  simp [quarticTermReduced]
+
+lemma quarticTermReduced_stabilityCounterExample (k : EuclideanSpace ℝ (Fin 3)) :
+    quarticTermReduced .stabilityCounterExample k = (1 - k 0) ^ 2 := by
+  simp [quarticTermReduced, PotentialParameters.η, Fin.isValue,
+    PotentialParameters.stabilityCounterExample, Fin.sum_univ_three]
+  ring
+
+lemma quarticTermReduced_stabilityCounterExample_nonneg (k : EuclideanSpace ℝ (Fin 3)) :
+    0 ≤ quarticTermReduced .stabilityCounterExample k := by
+  rw [quarticTermReduced_stabilityCounterExample]
+  apply sq_nonneg
+
+/-!
+
+### E.5. Stability in terms of the gram vectors
+
+We give some necessary and sufficient conditions for the potential to be stable
+in terms of the gram vectors.
+
+This follows the analysis in https://arxiv.org/abs/hep-ph/0605184.
+
+We also give some necessary conditions.
+
+-/
+
+lemma potentialIsStable_iff_forall_gramVector (P : PotentialParameters) :
+    PotentialIsStable P ↔ ∃ c : ℝ, ∀ K : Fin 1 ⊕ Fin 3 → ℝ, 0 ≤ K (Sum.inl 0) →
       ∑ μ : Fin 3, K (Sum.inr μ) ^ 2 ≤ K (Sum.inl 0) ^ 2 →
       c ≤ ∑ μ, P.ξ μ * K μ + ∑ a, ∑ b, K a * K b * P.η a b := by
   apply Iff.intro
@@ -184,13 +654,13 @@ lemma potentialIsBounded_iff_forall_gramVector (P : PotentialParameters) :
     apply le_of_eq
     rw [potential, massTerm_eq_gramVector, quarticTerm_eq_gramVector]
 
-lemma potentialIsBounded_iff_forall_euclid (P : PotentialParameters) :
-    PotentialIsBounded P ↔ ∃ c, ∀ K0 : ℝ, ∀ K : EuclideanSpace ℝ (Fin 3), 0 ≤ K0 →
+lemma potentialIsStable_iff_forall_euclid (P : PotentialParameters) :
+    PotentialIsStable P ↔ ∃ c, ∀ K0 : ℝ, ∀ K : EuclideanSpace ℝ (Fin 3), 0 ≤ K0 →
       ‖K‖ ^ 2 ≤ K0 ^ 2 → c ≤ P.ξ (Sum.inl 0) * K0 + ∑ μ, P.ξ (Sum.inr μ) * K μ
       + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0)
       + 2 * K0 * ∑ b, K b * P.η (Sum.inl 0) (Sum.inr b) +
       ∑ a, ∑ b, K a * K b * P.η (Sum.inr a) (Sum.inr b) := by
-  rw [potentialIsBounded_iff_forall_gramVector]
+  rw [potentialIsStable_iff_forall_gramVector]
   refine exists_congr (fun c => ?_)
   rw [Equiv.forall_congr_left (Equiv.sumArrowEquivProdArrow (Fin 1) (Fin 3) ℝ)]
   simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
@@ -220,13 +690,13 @@ lemma potentialIsBounded_iff_forall_euclid (P : PotentialParameters) :
     rw [PotentialParameters.η_symm]
   ring
 
-lemma potentialIsBounded_iff_forall_euclid_lt (P : PotentialParameters) :
-    PotentialIsBounded P ↔ ∃ c ≤ 0, ∀ K0 : ℝ, ∀ K : EuclideanSpace ℝ (Fin 3), 0 < K0 →
+lemma potentialIsStable_iff_forall_euclid_lt (P : PotentialParameters) :
+    PotentialIsStable P ↔ ∃ c ≤ 0, ∀ K0 : ℝ, ∀ K : EuclideanSpace ℝ (Fin 3), 0 < K0 →
       ‖K‖ ^ 2 ≤ K0 ^ 2 → c ≤ P.ξ (Sum.inl 0) * K0 + ∑ μ, P.ξ (Sum.inr μ) * K μ
       + K0 ^ 2 * P.η (Sum.inl 0) (Sum.inl 0)
       + 2 * K0 * ∑ b, K b * P.η (Sum.inl 0) (Sum.inr b) +
       ∑ a, ∑ b, K a * K b * P.η (Sum.inr a) (Sum.inr b) := by
-  rw [potentialIsBounded_iff_forall_euclid]
+  rw [potentialIsStable_iff_forall_euclid]
   apply Iff.intro
   · intro h
     obtain ⟨c, hc⟩ := h
@@ -245,59 +715,10 @@ lemma potentialIsBounded_iff_forall_euclid_lt (P : PotentialParameters) :
     · refine hc K0 K ?_ hle
       grind
 
-/-!
-
-## Mass term reduced
-
--/
-
-/-- A function related to the mass term of the potential, used in the boundedness
-  condition and equivalent to the term `J2` in
-  https://arxiv.org/abs/hep-ph/0605184. -/
-noncomputable def massTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ :=
-  P.ξ (Sum.inl 0) + ∑ μ, P.ξ (Sum.inr μ) * k μ
-
-lemma massTermReduced_lower_bound (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3))
-    (hk : ‖k‖ ^ 2 ≤ 1) : P.ξ (Sum.inl 0) - √(∑ a, |P.ξ (Sum.inr a)| ^ 2) ≤ massTermReduced P k := by
-  simp only [Fin.isValue, massTermReduced]
-  have h1 (a b c : ℝ) (h : - b ≤ c) : a - b ≤ a + c:= by grind
-  apply h1
-  let ξEuclid : EuclideanSpace ℝ (Fin 3) := WithLp.toLp 2 (fun a => P.ξ (Sum.inr a))
-  trans - ‖ξEuclid‖
-  · simp [@PiLp.norm_eq_of_L2, ξEuclid]
-  trans - (‖k‖ * ‖ξEuclid‖)
-  · simp
-    simp at hk
-    have ha (a b : ℝ) (h : a ≤ 1) (ha : 0 ≤ a) (hb : 0 ≤ b) : a * b ≤ b := by nlinarith
-    apply ha
-    · exact hk
-    · exact norm_nonneg k
-    · exact norm_nonneg ξEuclid
-  trans - ‖⟪k, ξEuclid⟫_ℝ‖
-  · simp
-    exact abs_real_inner_le_norm k ξEuclid
-  trans ⟪k, ξEuclid⟫_ℝ
-  · simp
-    grind
-  simp [PiLp.inner_apply, ξEuclid]
-
-/-!
-
-## Quartic term reduced
-
--/
-
-/-- A function related to the quartic term of the potential, used in the boundedness
-  condition and equivalent to the term `J4` in
-  https://arxiv.org/abs/hep-ph/0605184. -/
-noncomputable def quarticTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ :=
-  P.η (Sum.inl 0) (Sum.inl 0) + 2 * ∑ b, k b * P.η (Sum.inl 0) (Sum.inr b) +
-  ∑ a, ∑ b, k a * k b * P.η (Sum.inr a) (Sum.inr b)
-
-lemma potentialIsBounded_iff_exists_forall_forall_reduced (P : PotentialParameters) :
-    PotentialIsBounded P ↔ ∃ c ≤ 0, ∀ K0 : ℝ, ∀ k : EuclideanSpace ℝ (Fin 3), 0 < K0 →
+lemma potentialIsStable_iff_exists_forall_forall_reduced (P : PotentialParameters) :
+    PotentialIsStable P ↔ ∃ c ≤ 0, ∀ K0 : ℝ, ∀ k : EuclideanSpace ℝ (Fin 3), 0 < K0 →
       ‖k‖ ^ 2 ≤ 1 → c ≤ K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P k := by
-  rw [potentialIsBounded_iff_forall_euclid_lt]
+  rw [potentialIsStable_iff_forall_euclid_lt]
   refine exists_congr <| fun c => and_congr_right <| fun hc => forall_congr' <| fun K0 => ?_
   apply Iff.intro
   · refine fun h k hK0 k_le_one => (h (K0 • k) hK0 ?_).trans (le_of_eq ?_)
@@ -323,10 +744,10 @@ lemma potentialIsBounded_iff_exists_forall_forall_reduced (P : PotentialParamete
       field_simp
       ring
 
-lemma quarticTermReduced_nonneg_of_potentialIsBounded (P : PotentialParameters)
-    (hP : PotentialIsBounded P) (k : EuclideanSpace ℝ (Fin 3))
+lemma quarticTermReduced_nonneg_of_potentialIsStable (P : PotentialParameters)
+    (hP : PotentialIsStable P) (k : EuclideanSpace ℝ (Fin 3))
     (hk : ‖k‖ ^ 2 ≤ 1) : 0 ≤ quarticTermReduced P k := by
-  rw [potentialIsBounded_iff_exists_forall_forall_reduced] at hP
+  rw [potentialIsStable_iff_exists_forall_forall_reduced] at hP
   suffices hp : ∀ (a b : ℝ), (∃ c ≤ 0, ∀ x, 0 < x → c ≤ a * x + b * x ^ 2) →
       0 ≤ b ∧ (b = 0 → 0 ≤ a) by
     obtain ⟨c, hc, h⟩ := hP
@@ -366,17 +787,17 @@ lemma quarticTermReduced_nonneg_of_potentialIsBounded (P : PotentialParameters)
       (by grind [Real.sqrt_sq_eq_abs])) (hs (|x| + |d| + 1) (by positivity))
   exact fun x hx => (le_div_iff_of_neg (by grind)).mpr (by grind)
 
-lemma potentialIsBounded_iff_exists_forall_reduced (P : PotentialParameters) :
-    PotentialIsBounded P ↔ ∃ c, 0 ≤ c ∧ ∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
+lemma potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced (P : PotentialParameters) :
+    PotentialIsStable P ↔ ∃ c, 0 ≤ c ∧ ∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
       0 ≤ quarticTermReduced P k ∧
       (massTermReduced P k < 0 →
       massTermReduced P k ^ 2 ≤ 4 * quarticTermReduced P k * c) := by
-  rw [potentialIsBounded_iff_exists_forall_forall_reduced]
+  rw [potentialIsStable_iff_exists_forall_forall_reduced]
   refine Iff.intro (fun ⟨c, hc, h⟩ => ⟨-c, by grind, fun k hk => ?_⟩)
     (fun ⟨c, hc, h⟩ => ⟨-c, by grind, fun K0 k hk0 hk => ?_⟩)
   · have hJ4_nonneg : 0 ≤ quarticTermReduced P k := by
-      refine quarticTermReduced_nonneg_of_potentialIsBounded P ?_ k hk
-      rw [potentialIsBounded_iff_exists_forall_forall_reduced]
+      refine quarticTermReduced_nonneg_of_potentialIsStable P ?_ k hk
+      rw [potentialIsStable_iff_exists_forall_forall_reduced]
       exact ⟨c, hc, h⟩
     have h0 : ∀ K0, 0 < K0 → c ≤ K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P k :=
       fun K0 a => h K0 k a hk
@@ -432,10 +853,10 @@ lemma potentialIsBounded_iff_exists_forall_reduced (P : PotentialParameters) :
         · nlinarith
         · grind
 
-lemma massTermReduced_pos_of_quarticTermReduced_zero_potentialIsBounded (P : PotentialParameters)
-    (hP : PotentialIsBounded P) (k : EuclideanSpace ℝ (Fin 3))
+lemma massTermReduced_pos_of_quarticTermReduced_zero_potentialIsStable (P : PotentialParameters)
+    (hP : PotentialIsStable P) (k : EuclideanSpace ℝ (Fin 3))
     (hk : ‖k‖ ^ 2 ≤ 1) (hq : quarticTermReduced P k = 0) : 0 ≤ massTermReduced P k := by
-  rw [potentialIsBounded_iff_exists_forall_reduced] at hP
+  rw [potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced] at hP
   obtain ⟨c, hc₀, hc⟩ := hP
   specialize hc k hk
   rw [hq] at hc
@@ -443,10 +864,85 @@ lemma massTermReduced_pos_of_quarticTermReduced_zero_potentialIsBounded (P : Pot
   generalize massTermReduced P k = j2 at *
   grind
 
-@[sorryful]
-lemma potentialIsBounded_iff_forall_reduced (P : PotentialParameters) :
-    PotentialIsBounded P ↔ ∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
-      0 ≤ quarticTermReduced P k ∧ (quarticTermReduced P k = 0 → 0 ≤ massTermReduced P k) := by
-  sorry
+/-!
+
+### E.6. Strong stability implies stability
+
+Stability in terms of the positivity of the quartic term, implies that the whole
+potential is stable.
+
+-/
+
+/-- The potential is stable if it is strongly stable, i.e. its quartic term is always positive.
+    The proof of this result relies on the compactness of the closed unit ball in
+    `EuclideanSpace ℝ (Fin 3)`, and the `extreme value theorem`. -/
+lemma potentialIsStable_of_strong (P : PotentialParameters)
+    (h : ∀ k, ‖k‖ ^ 2 ≤ 1 → 0 < quarticTermReduced P k) :
+    PotentialIsStable P := by
+  rw [potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced]
+  let S := Metric.closedBall (0 : EuclideanSpace ℝ (Fin 3)) 1
+  have S_isCompact : IsCompact S := isCompact_closedBall 0 1
+  have S_nonEmpty : S.Nonempty := ⟨0, by simp [S]⟩
+  obtain ⟨kmax, kmax_S, kmax_isMax⟩ := IsCompact.exists_isMaxOn
+    (isCompact_closedBall 0 1) S_nonEmpty
+    (f := fun k => (massTermReduced P k ^ 2) / (4 * quarticTermReduced P k)) <| by
+    apply ContinuousOn.div₀
+    · apply Continuous.continuousOn
+      simp only [massTermReduced, Fin.isValue]
+      fun_prop
+    · apply Continuous.continuousOn
+      simp only [quarticTermReduced, Fin.isValue]
+      fun_prop
+    · intro x hx
+      specialize h x (by simpa using hx)
+      linarith
+  use (massTermReduced P kmax) ^ 2 / (4 * quarticTermReduced P kmax)
+  apply And.intro
+  · refine (le_div_iff₀ ?_).mpr ?_
+    · specialize h kmax (by simpa using kmax_S)
+      linarith
+    · simp only [zero_mul]
+      exact sq_nonneg (massTermReduced P kmax)
+  · intro k hk
+    apply And.intro
+    · specialize h k hk
+      linarith
+    · intro hq
+      rw [isMaxOn_iff] at kmax_isMax
+      refine (div_le_iff₀' ?_).mp (kmax_isMax k (by simpa using hk))
+      grind
+
+/-!
+
+### E.7. Showing step in hep-ph/0605184 is invalid
+
+-/
+
+/-- A lemma invalidating the step in https://arxiv.org/pdf/hep-ph/0605184 leading to
+  equation (4.4). -/
+lemma forall_reduced_exists_not_potentialIsStable :
+    ∃ P, ¬ PotentialIsStable P ∧ (∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
+    0 ≤ quarticTermReduced P k ∧ (quarticTermReduced P k = 0 → 0 ≤ massTermReduced P k)) := by
+  /- Construction of the explicit counter example.
+    The reason that this counter example works is that:
+    - There is a zero of the quartic term `z` on the boundary.
+    - The quartic term is equal to `((k - z) · z)²`, as `k - z` approaches orthogonal to `z`,
+      this becomes small on two accounts: the abs of `k - z` has to become small as `z` is on
+      the boundary, and the angle between `k - z` and `z` also becomes small.
+    - The mass term is of the form `-(k - z) · w` for some `w` orthogonal to `z`, so as `k - z`
+      approaches orthogonal to `z`, the mass term becomes small only on the account that the abs of
+      `k - z` becomes small. -/
+  use .stabilityCounterExample
+  apply And.intro
+  /- The condition that P is not stable. -/
+  · exact stabilityCounterExample_not_potentialIsStable
+  /- The condition on the reduced terms. -/
+  · refine fun k hk => And.intro (quarticTermReduced_stabilityCounterExample_nonneg k)
+      (fun hq => ?_)
+    simp [quarticTermReduced_stabilityCounterExample] at hq
+    simp only [PiLp.norm_sq_eq_of_L2, Real.norm_eq_abs, sq_abs, Fin.sum_univ_three,
+      Fin.isValue] at hk
+    have hk1 : k 1 = 0 := by nlinarith
+    rw [massTermReduced_stabilityCounterExample, hk1]
 
 end TwoHiggsDoublet
diff --git a/scripts/MetaPrograms/module_doc_no_lint.txt b/scripts/MetaPrograms/module_doc_no_lint.txt
index dfc1c11ae..01842ff4c 100644
--- a/scripts/MetaPrograms/module_doc_no_lint.txt
+++ b/scripts/MetaPrograms/module_doc_no_lint.txt
@@ -91,7 +91,6 @@ PhysLean/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSol
 PhysLean/Particles/BeyondTheStandardModel/Spin10/Basic.lean
 PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
 PhysLean/Particles/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean
-PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
 PhysLean/Particles/FlavorPhysics/CKMMatrix/Basic.lean
 PhysLean/Particles/FlavorPhysics/CKMMatrix/Invariants.lean
 PhysLean/Particles/FlavorPhysics/CKMMatrix/PhaseFreedom.lean