From 5a8983504ae1bd704299dc025ceadfb43e2a0d42 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 26 Jan 2026 16:03:22 +0000
Subject: [PATCH 1/3] feat: Update potential

---
 .../TwoHDM/Potential.lean                     | 318 ++++++++++++++++++
 1 file changed, 318 insertions(+)

diff --git a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
index 9aedc4854..2c4294fea 100644
--- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
+++ b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
@@ -184,4 +184,322 @@ 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 →
+      ‖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]
+  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,
+    Finset.sum_singleton, Prod.forall, Equiv.sumArrowEquivProdArrow_symm_apply_inl,
+    Equiv.sumArrowEquivProdArrow_symm_apply_inr]
+  rw [Equiv.forall_congr_left <| Equiv.funUnique (Fin 1) ℝ]
+  apply forall_congr'
+  intro K0
+  rw [Equiv.forall_congr_left <| (WithLp.equiv 2 ((i : Fin 3) → (fun x => ℝ) i)).symm]
+  apply forall_congr'
+  intro K
+  simp only [Fin.isValue, Equiv.funUnique_symm_apply, uniqueElim_const, Equiv.symm_symm,
+    WithLp.equiv_apply]
+  refine imp_congr_right ?_
+  intro hle
+  simp only [PiLp.norm_sq_eq_of_L2]
+  simp only [Fin.isValue, Real.norm_eq_abs, sq_abs]
+  refine imp_congr_right ?_
+  intro hle'
+  apply le_iff_le_of_cmp_eq_cmp
+  congr 1
+  simp [add_assoc, sq, Finset.sum_add_distrib]
+  ring_nf
+  simp [mul_assoc, ← Finset.mul_sum]
+  conv_lhs =>
+    enter [2, 2, 2, i]
+    rw [PotentialParameters.η_symm]
+  ring
+
+lemma potentialIsBounded_iff_forall_euclid_lt (P : PotentialParameters) :
+    PotentialIsBounded 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]
+  apply Iff.intro
+  · intro h
+    obtain ⟨c, hc⟩ := h
+    use c
+    apply And.intro
+    · simpa using hc 0 0 (by simp) (by simp)
+    · intro K0 K hk0 hle
+      exact hc K0 K hk0.le hle
+  · intro h
+    obtain ⟨c, hc₀, hc⟩ := h
+    use c
+    intro K0 K hK0 hle
+    by_cases hK0' : K0 = 0
+    · subst hK0'
+      simp_all
+    · refine hc K0 K ?_ hle
+      grind
+
+noncomputable def J2 (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ :=
+  P.ξ (Sum.inl 0) + ∑ μ, P.ξ (Sum.inr μ) * k μ
+
+lemma J2_lower_bound (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3))
+    (hk : ‖k‖ ^ 2 ≤ 1) : P.ξ (Sum.inl 0) - √(∑ a, |P.ξ (Sum.inr a)| ^ 2) ≤ J2 P k := by
+  simp only [Fin.isValue, J2]
+  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]
+
+noncomputable def J4 (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_forall_scalar_euclid_bound_one (P : PotentialParameters) :
+    PotentialIsBounded P ↔ ∃ c ≤ 0, ∀ K0 : ℝ, ∀ k : EuclideanSpace ℝ (Fin 3), 0 < K0 →
+      ‖k‖ ^ 2 ≤ 1 → c ≤ K0 * J2 P k + K0 ^ 2 * J4 P k := by
+  rw [potentialIsBounded_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 ?_)
+    · simp [norm_smul]
+      rw [abs_of_nonneg (by positivity), mul_pow]
+      nlinarith
+    · simp [add_assoc, J2, J4]
+      ring_nf
+      simp [add_assoc, mul_assoc, ← Finset.mul_sum, sq]
+      ring
+  · intro h K hK0 hle
+    refine (h ((1 / K0) • K) hK0 ?_).trans (le_of_eq ?_)
+    · simp [norm_smul]
+      field_simp
+      rw [sq_le_sq] at hle
+      simpa using hle
+    · simp [add_assoc, J2, J4]
+      ring_nf
+      simp [add_assoc, mul_assoc, ← Finset.mul_sum, sq]
+      field_simp
+      ring_nf
+      simp only [← Finset.sum_mul, Fin.isValue]
+      field_simp
+      ring
+
+
+lemma J4_nonneg_of_potentialIsBounded (P : PotentialParameters)
+    (hP : PotentialIsBounded P) (k : EuclideanSpace ℝ (Fin 3))
+    (hk : ‖k‖ ^ 2 ≤ 1) : 0 ≤ J4 P k := by
+  rw [potentialIsBounded_iff_forall_scalar_euclid_bound_one] 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
+    refine (hp (J2 P k) (J4 P k) ⟨c, hc, ?_⟩).1
+    grind
+  intro a b
+  by_cases hb : b = 0
+  /- The case of b = 0. -/
+  · subst hb
+    by_cases ha : a = 0
+    · subst ha
+      simp
+    · simp only [zero_mul, add_zero, le_refl, forall_const, true_and]
+      rintro ⟨c, hc, hx⟩
+      by_contra h2
+      simp_all
+      refine not_lt_of_ge (hx (c/a + 1) ?_) ?_
+      · exact add_pos_of_nonneg_of_pos (div_nonneg_of_nonpos hc (Std.le_of_lt h2))
+          Real.zero_lt_one
+      · field_simp
+        grind
+  /- The case of b ≠ 0. -/
+  have h1 (x : ℝ) : a * x + b * x ^ 2 = b * (x + a / (2 * b)) ^ 2 - a ^ 2 / (4 * b) := by grind
+  generalize a ^ 2 / (4 * b) = c1 at h1
+  generalize a / (2 * b) = d at h1
+  simp only [hb, IsEmpty.forall_iff, and_true]
+  have hlt (c : ℝ) (x : ℝ) : (c ≤ a * x + b * x ^ 2) ↔ c + c1 ≤ b * (x + d) ^ 2 := by grind
+  conv_lhs => enter [1, c, 2, x]; rw [hlt c]
+  trans ∃ c, ∀ x, 0 < x → c ≤ b * (x + d) ^ 2
+  · rintro ⟨c, hc, hx⟩
+    use c + c1
+  rintro ⟨c, hc⟩
+  by_contra hn
+  suffices hs : ∀ x, x ^ 2 ≤ c/b from not_lt_of_ge (hs √(|c/b| + 1)) (by grind)
+  suffices hs : ∀ x, 0 < x → (x + d) ^ 2 ≤ c/b from
+    fun x => le_trans ((Real.sqrt_le_left (by grind)).mp
+      (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_J2_J4 (P : PotentialParameters) :
+    PotentialIsBounded P ↔ ∃ c, 0 ≤ c ∧ ∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
+      0 ≤ J4 P k ∧ (J2 P k < 0 → J2 P k ^ 2 ≤ 4 * J4 P k * c)  := by
+  rw [potentialIsBounded_iff_forall_scalar_euclid_bound_one]
+  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 ≤ J4 P k := by
+      refine J4_nonneg_of_potentialIsBounded P ?_ k hk
+      rw [potentialIsBounded_iff_forall_scalar_euclid_bound_one]
+      exact ⟨c, hc, h⟩
+    have h0 : ∀ K0, 0 < K0 →  c ≤ K0 * J2 P k + K0 ^ 2 * J4 P k :=  fun K0 a =>  h K0 k a hk
+    clear h
+    generalize J2 P k = j2 at *
+    generalize J4 P k = j4 at *
+    by_cases j4_zero : j4 = 0
+    · subst j4_zero
+      simp_all
+      intro hj2
+      by_contra hn
+      specialize h0 ((c - 1) / j2) <| by
+        refine div_pos_iff.mpr (Or.inr ?_)
+        grind
+      field_simp at h0
+      linarith
+    · have hsq (K0 : ℝ) : K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) := by
+          ring_nf
+          field_simp
+          ring
+      have hj_pos : 0 < j4 := by grind
+      apply And.intro
+      · grind
+      · intro j2_neg
+        conv at h0 => enter [2]; rw [hsq]
+        specialize h0 ( - j2 / (2 * j4)) <| by
+          field_simp
+          grind
+        ring_nf at h0
+        field_simp at h0
+        grind
+  · specialize h k hk
+    generalize J2 P k = j2 at *
+    generalize J4 P k = j4 at *
+    by_cases hJ4 : j4 = 0
+    · subst j4
+      simp_all
+      trans 0
+      · grind
+      · by_cases hJ2 : j2 = 0
+        · simp_all
+        · simp_all
+    · have hJ4_pos : 0 < j4 := by grind
+      have h0 : K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) := by
+          ring_nf
+          field_simp
+          ring
+      rw [h0]
+      by_cases hJ2_neg : j2 < 0
+      · trans j4 * (K0 + j2 / (2 * j4)) ^ 2 - c
+        · nlinarith
+        · field_simp
+          ring_nf
+          grind
+      · refine neg_le_sub_iff_le_add.mpr ?_
+        trans j4 * (K0 + j2 / (2 * j4)) ^ 2
+        · nlinarith
+        · linarith
+
+lemma potentialIsBounded_iff_J2_J4 (P : PotentialParameters) :
+    PotentialIsBounded P ↔ ∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
+      0 ≤ J4 P k ∧ (J4 P k = 0 → 0 ≤ J2 P k)  := by
+  rw [potentialIsBounded_iff_exists_J2_J4]
+  apply Iff.intro
+  · sorry
+  · intro h
+    let f : EuclideanSpace ℝ (Fin 3) → ℝ := fun k => J2 P k ^ 2 / (4 * J4 P k)
+    let s : Set (EuclideanSpace ℝ (Fin 3)) := Metric.closedBall 0 1 ∩ {k | J2 P k ≤ 0}
+    have hs : IsCompact s := by
+      refine IsCompact.inter ?_ ?_
+      exact isCompact_closedBall 0 1
+      refine isCompact_of_totallyBounded_isClosed ?_ ?_
+      · sorry
+      · refine isClosed_le ?_ ?_
+        · change Continuous (fun k => J2 P k)
+          simp [J2]
+          fun_prop
+        · fun_prop
+    have ne_s : s.Nonempty := ⟨0, by simp [s]⟩
+    have hf_cont : ContinuousOn f s := by
+      simp [f, s]
+      refine continuousOn_of_forall_continuousAt ?_
+      intro x hx
+      by_cases hJ4_zero : J4 P x ≠ 0
+      · refine ContinuousAt.div₀ ?_ ?_ ?_
+        · simp [J2]
+          fun_prop
+        · simp [J4]
+          fun_prop
+        · grind
+      simp at hJ4_zero
+      have hJ2_zero : 0 ≤ J2 P x := by
+        specialize h x
+        rw [hJ4_zero] at h
+        simp at h
+        simp at hx
+
+        simp at h
+        exact (h.2 hJ4_zero).le
+      suffices h_line : ∀ v,  ContinuousAt (fun (t : ℝ) => J2 P (x + t • v) ^ 2 / (4 * J4 P (x + t • v))) 0 by
+        sorry
+      intro v
+      have J2_expand (t : ℝ) : J2 P (x + t • v) = (P.ξ (Sum.inl 0)
+          + ∑ a, P.ξ (Sum.inr a) * x a)  + t * ∑ a, P.ξ (Sum.inr a) * v a := by
+        simp [J2, mul_add, Finset.sum_add_distrib, Finset.mul_sum, add_assoc]
+        ring_nf
+        congr
+        funext x
+        ring
+      generalize (P.ξ (Sum.inl 0) + ∑ a, P.ξ (Sum.inr a) * x a) = r1 at J2_expand
+      generalize (∑ a, P.ξ (Sum.inr a) * v a) = r2 at J2_expand
+      have J4_expand' (t : ℝ) : J4 P (x + t • v) = P.η (Sum.inl 0) (Sum.inl 0) +
+         ∑ i, 2 * (x.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) +
+         t * ∑ i, 2 * ( v.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) +
+          ∑ x_1, ∑ x_2, x.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
+         t * ∑ x_1, ∑ x_2,  v.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
+          (t * ∑ x_1, ∑ x_2,  x.ofLp x_1 * v.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
+           t ^ 2 * ∑ x, ∑ x_1, v.ofLp x * v.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))
+           := by
+        simp [J4, mul_add, Finset.sum_add_distrib, mul_add, add_mul, Finset.mul_sum, add_assoc]
+        ring_nf
+      have J4_expand (t : ℝ) : J4 P (x + t • v) = (P.η (Sum.inl 0) (Sum.inl 0) +
+         ∑ i, 2 * (x.ofLp i * P.η (Sum.inl 0) (Sum.inr i))
+         + ∑ x_1, ∑ x_2, x.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) ) +
+         t * (∑ i, 2 * ( v.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) +
+         ∑ x_1, ∑ x_2,  v.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
+           ∑ x_1, ∑ x_2,  x.ofLp x_1 * v.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2)) +
+           t ^ 2 * ∑ x, ∑ x_1, v.ofLp x * v.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1)
+           := by rw [J4_expand']; ring
+      generalize (P.η (Sum.inl 0) (Sum.inl 0) +
+         ∑ i, 2 * (x.ofLp i * P.η (Sum.inl 0) (Sum.inr i))
+         + ∑ x_1, ∑ x_2, x.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) ) = s1 at J4_expand
+      generalize  (∑ i, 2 * (v.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) +
+              ∑ x_1, ∑ x_2, v.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
+            ∑ x_1, ∑ x_2, x.ofLp x_1 * v.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2)) = s2 at J4_expand
+      generalize (∑ x, ∑ x_1, v.ofLp x * v.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1)) = s3 at J4_expand
+      clear J4_expand'
+
+
+      sorry
+
+
+
 end TwoHiggsDoublet

From d3129cff354c858ec4bd30a5fa351fff4d164aa9 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 27 Jan 2026 12:20:31 +0000
Subject: [PATCH 2/3] feat: Update potential

---
 .../TwoHDM/Potential.lean                     | 174 ++++++------------
 1 file changed, 55 insertions(+), 119 deletions(-)

diff --git a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
index 2c4294fea..b72f744bb 100644
--- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
+++ b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
@@ -245,12 +245,21 @@ lemma potentialIsBounded_iff_forall_euclid_lt (P : PotentialParameters) :
     · refine hc K0 K ?_ hle
       grind
 
-noncomputable def J2 (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ :=
+/-!
+
+## 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 J2_lower_bound (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3))
-    (hk : ‖k‖ ^ 2 ≤ 1) : P.ξ (Sum.inl 0) - √(∑ a, |P.ξ (Sum.inr a)| ^ 2) ≤ J2 P k := by
-  simp only [Fin.isValue, J2]
+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))
@@ -272,15 +281,23 @@ lemma J2_lower_bound (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3))
     grind
   simp [PiLp.inner_apply, ξEuclid]
 
-noncomputable def J4 (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)
 
+/-!
+
+## 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_forall_scalar_euclid_bound_one (P : PotentialParameters) :
+lemma potentialIsBounded_iff_exists_forall_forall_reduced (P : PotentialParameters) :
     PotentialIsBounded P ↔ ∃ c ≤ 0, ∀ K0 : ℝ, ∀ k : EuclideanSpace ℝ (Fin 3), 0 < K0 →
-      ‖k‖ ^ 2 ≤ 1 → c ≤ K0 * J2 P k + K0 ^ 2 * J4 P k := by
+      ‖k‖ ^ 2 ≤ 1 → c ≤ K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P k := by
   rw [potentialIsBounded_iff_forall_euclid_lt]
   refine exists_congr <| fun c => and_congr_right <| fun hc => forall_congr' <| fun K0 => ?_
   apply Iff.intro
@@ -288,7 +305,7 @@ lemma potentialIsBounded_iff_forall_scalar_euclid_bound_one (P : PotentialParame
     · simp [norm_smul]
       rw [abs_of_nonneg (by positivity), mul_pow]
       nlinarith
-    · simp [add_assoc, J2, J4]
+    · simp [add_assoc, massTermReduced, quarticTermReduced]
       ring_nf
       simp [add_assoc, mul_assoc, ← Finset.mul_sum, sq]
       ring
@@ -298,7 +315,7 @@ lemma potentialIsBounded_iff_forall_scalar_euclid_bound_one (P : PotentialParame
       field_simp
       rw [sq_le_sq] at hle
       simpa using hle
-    · simp [add_assoc, J2, J4]
+    · simp [add_assoc, massTermReduced, quarticTermReduced]
       ring_nf
       simp [add_assoc, mul_assoc, ← Finset.mul_sum, sq]
       field_simp
@@ -307,15 +324,14 @@ lemma potentialIsBounded_iff_forall_scalar_euclid_bound_one (P : PotentialParame
       field_simp
       ring
 
-
-lemma J4_nonneg_of_potentialIsBounded (P : PotentialParameters)
+lemma quarticTermReduced_nonneg_of_potentialIsBounded (P : PotentialParameters)
     (hP : PotentialIsBounded P) (k : EuclideanSpace ℝ (Fin 3))
-    (hk : ‖k‖ ^ 2 ≤ 1) : 0 ≤ J4 P k := by
-  rw [potentialIsBounded_iff_forall_scalar_euclid_bound_one] at hP
+    (hk : ‖k‖ ^ 2 ≤ 1) : 0 ≤ quarticTermReduced P k := by
+  rw [potentialIsBounded_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
-    refine (hp (J2 P k) (J4 P k) ⟨c, hc, ?_⟩).1
+    refine (hp (massTermReduced P k) (quarticTermReduced P k) ⟨c, hc, ?_⟩).1
     grind
   intro a b
   by_cases hb : b = 0
@@ -351,20 +367,22 @@ lemma J4_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_J2_J4 (P : PotentialParameters) :
+lemma potentialIsBounded_iff_exists_forall_reduced (P : PotentialParameters) :
     PotentialIsBounded P ↔ ∃ c, 0 ≤ c ∧ ∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
-      0 ≤ J4 P k ∧ (J2 P k < 0 → J2 P k ^ 2 ≤ 4 * J4 P k * c)  := by
-  rw [potentialIsBounded_iff_forall_scalar_euclid_bound_one]
+      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]
   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 ≤ J4 P k := by
-      refine J4_nonneg_of_potentialIsBounded P ?_ k hk
-      rw [potentialIsBounded_iff_forall_scalar_euclid_bound_one]
+  · have hJ4_nonneg : 0 ≤ quarticTermReduced P k := by
+      refine quarticTermReduced_nonneg_of_potentialIsBounded P ?_ k hk
+      rw [potentialIsBounded_iff_exists_forall_forall_reduced]
       exact ⟨c, hc, h⟩
-    have h0 : ∀ K0, 0 < K0 →  c ≤ K0 * J2 P k + K0 ^ 2 * J4 P k :=  fun K0 a =>  h K0 k a hk
+    have h0 : ∀ K0, 0 < K0 →  c ≤ K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P k :=  fun K0 a =>  h K0 k a hk
     clear h
-    generalize J2 P k = j2 at *
-    generalize J4 P k = j4 at *
+    generalize massTermReduced P k = j2 at *
+    generalize quarticTermReduced P k = j4 at *
     by_cases j4_zero : j4 = 0
     · subst j4_zero
       simp_all
@@ -375,10 +393,9 @@ lemma potentialIsBounded_iff_exists_J2_J4 (P : PotentialParameters) :
         grind
       field_simp at h0
       linarith
-    · have hsq (K0 : ℝ) : K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) := by
-          ring_nf
-          field_simp
-          ring
+    · have hsq (K0 : ℝ) : K0 * j2 + K0 ^ 2 * j4 =
+            j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) := by
+        grind
       have hj_pos : 0 < j4 := by grind
       apply And.intro
       · grind
@@ -391,8 +408,8 @@ lemma potentialIsBounded_iff_exists_J2_J4 (P : PotentialParameters) :
         field_simp at h0
         grind
   · specialize h k hk
-    generalize J2 P k = j2 at *
-    generalize J4 P k = j4 at *
+    generalize massTermReduced P k = j2 at *
+    generalize quarticTermReduced P k = j4 at *
     by_cases hJ4 : j4 = 0
     · subst j4
       simp_all
@@ -403,103 +420,22 @@ lemma potentialIsBounded_iff_exists_J2_J4 (P : PotentialParameters) :
         · simp_all
     · have hJ4_pos : 0 < j4 := by grind
       have h0 : K0 * j2 + K0 ^ 2 * j4 = j4 * (K0 + j2 / (2 * j4)) ^ 2 - j2 ^ 2 / (4 * j4) := by
-          ring_nf
-          field_simp
-          ring
+          grind
       rw [h0]
       by_cases hJ2_neg : j2 < 0
       · trans j4 * (K0 + j2 / (2 * j4)) ^ 2 - c
         · nlinarith
         · field_simp
-          ring_nf
           grind
       · refine neg_le_sub_iff_le_add.mpr ?_
         trans j4 * (K0 + j2 / (2 * j4)) ^ 2
         · nlinarith
-        · linarith
-
-lemma potentialIsBounded_iff_J2_J4 (P : PotentialParameters) :
-    PotentialIsBounded P ↔ ∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
-      0 ≤ J4 P k ∧ (J4 P k = 0 → 0 ≤ J2 P k)  := by
-  rw [potentialIsBounded_iff_exists_J2_J4]
-  apply Iff.intro
-  · sorry
-  · intro h
-    let f : EuclideanSpace ℝ (Fin 3) → ℝ := fun k => J2 P k ^ 2 / (4 * J4 P k)
-    let s : Set (EuclideanSpace ℝ (Fin 3)) := Metric.closedBall 0 1 ∩ {k | J2 P k ≤ 0}
-    have hs : IsCompact s := by
-      refine IsCompact.inter ?_ ?_
-      exact isCompact_closedBall 0 1
-      refine isCompact_of_totallyBounded_isClosed ?_ ?_
-      · sorry
-      · refine isClosed_le ?_ ?_
-        · change Continuous (fun k => J2 P k)
-          simp [J2]
-          fun_prop
-        · fun_prop
-    have ne_s : s.Nonempty := ⟨0, by simp [s]⟩
-    have hf_cont : ContinuousOn f s := by
-      simp [f, s]
-      refine continuousOn_of_forall_continuousAt ?_
-      intro x hx
-      by_cases hJ4_zero : J4 P x ≠ 0
-      · refine ContinuousAt.div₀ ?_ ?_ ?_
-        · simp [J2]
-          fun_prop
-        · simp [J4]
-          fun_prop
         · grind
-      simp at hJ4_zero
-      have hJ2_zero : 0 ≤ J2 P x := by
-        specialize h x
-        rw [hJ4_zero] at h
-        simp at h
-        simp at hx
-
-        simp at h
-        exact (h.2 hJ4_zero).le
-      suffices h_line : ∀ v,  ContinuousAt (fun (t : ℝ) => J2 P (x + t • v) ^ 2 / (4 * J4 P (x + t • v))) 0 by
-        sorry
-      intro v
-      have J2_expand (t : ℝ) : J2 P (x + t • v) = (P.ξ (Sum.inl 0)
-          + ∑ a, P.ξ (Sum.inr a) * x a)  + t * ∑ a, P.ξ (Sum.inr a) * v a := by
-        simp [J2, mul_add, Finset.sum_add_distrib, Finset.mul_sum, add_assoc]
-        ring_nf
-        congr
-        funext x
-        ring
-      generalize (P.ξ (Sum.inl 0) + ∑ a, P.ξ (Sum.inr a) * x a) = r1 at J2_expand
-      generalize (∑ a, P.ξ (Sum.inr a) * v a) = r2 at J2_expand
-      have J4_expand' (t : ℝ) : J4 P (x + t • v) = P.η (Sum.inl 0) (Sum.inl 0) +
-         ∑ i, 2 * (x.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) +
-         t * ∑ i, 2 * ( v.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) +
-          ∑ x_1, ∑ x_2, x.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
-         t * ∑ x_1, ∑ x_2,  v.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
-          (t * ∑ x_1, ∑ x_2,  x.ofLp x_1 * v.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
-           t ^ 2 * ∑ x, ∑ x_1, v.ofLp x * v.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1))
-           := by
-        simp [J4, mul_add, Finset.sum_add_distrib, mul_add, add_mul, Finset.mul_sum, add_assoc]
-        ring_nf
-      have J4_expand (t : ℝ) : J4 P (x + t • v) = (P.η (Sum.inl 0) (Sum.inl 0) +
-         ∑ i, 2 * (x.ofLp i * P.η (Sum.inl 0) (Sum.inr i))
-         + ∑ x_1, ∑ x_2, x.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) ) +
-         t * (∑ i, 2 * ( v.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) +
-         ∑ x_1, ∑ x_2,  v.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
-           ∑ x_1, ∑ x_2,  x.ofLp x_1 * v.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2)) +
-           t ^ 2 * ∑ x, ∑ x_1, v.ofLp x * v.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1)
-           := by rw [J4_expand']; ring
-      generalize (P.η (Sum.inl 0) (Sum.inl 0) +
-         ∑ i, 2 * (x.ofLp i * P.η (Sum.inl 0) (Sum.inr i))
-         + ∑ x_1, ∑ x_2, x.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) ) = s1 at J4_expand
-      generalize  (∑ i, 2 * (v.ofLp i * P.η (Sum.inl 0) (Sum.inr i)) +
-              ∑ x_1, ∑ x_2, v.ofLp x_1 * x.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2) +
-            ∑ x_1, ∑ x_2, x.ofLp x_1 * v.ofLp x_2 * P.η (Sum.inr x_1) (Sum.inr x_2)) = s2 at J4_expand
-      generalize (∑ x, ∑ x_1, v.ofLp x * v.ofLp x_1 * P.η (Sum.inr x) (Sum.inr x_1)) = s3 at J4_expand
-      clear J4_expand'
-
-
-      sorry
-
 
+@[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
 
 end TwoHiggsDoublet

From 218c61d2448b288266edd02359c2a435da52380b Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 27 Jan 2026 14:17:28 +0000
Subject: [PATCH 3/3] refactor: style

---
 .../BeyondTheStandardModel/TwoHDM/Potential.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
index b72f744bb..61abb57e5 100644
--- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
+++ b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
@@ -260,7 +260,7 @@ noncomputable def massTermReduced (P : PotentialParameters) (k : EuclideanSpace
 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
+  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‖
@@ -281,7 +281,6 @@ lemma massTermReduced_lower_bound (P : PotentialParameters) (k : EuclideanSpace
     grind
   simp [PiLp.inner_apply, ξEuclid]
 
-
 /-!
 
 ## Quartic term reduced
@@ -371,15 +370,16 @@ lemma potentialIsBounded_iff_exists_forall_reduced (P : PotentialParameters) :
     PotentialIsBounded 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
+      massTermReduced P k ^ 2 ≤ 4 * quarticTermReduced P k * c) := by
   rw [potentialIsBounded_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 => ?_⟩)
+  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]
       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
+    have h0 : ∀ K0, 0 < K0 → c ≤ K0 * massTermReduced P k + K0 ^ 2 * quarticTermReduced P k :=
+      fun K0 a => h K0 k a hk
     clear h
     generalize massTermReduced P k = j2 at *
     generalize quarticTermReduced P k = j4 at *
@@ -401,7 +401,7 @@ lemma potentialIsBounded_iff_exists_forall_reduced (P : PotentialParameters) :
       · grind
       · intro j2_neg
         conv at h0 => enter [2]; rw [hsq]
-        specialize h0 ( - j2 / (2 * j4)) <| by
+        specialize h0 (- j2 / (2 * j4)) <| by
           field_simp
           grind
         ring_nf at h0
@@ -435,7 +435,7 @@ lemma potentialIsBounded_iff_exists_forall_reduced (P : PotentialParameters) :
 @[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
+      0 ≤ quarticTermReduced P k ∧ (quarticTermReduced P k = 0 → 0 ≤ massTermReduced P k) := by
   sorry
 
 end TwoHiggsDoublet