feat: bounded properties of Higgs potential

HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean

@@ -22,6 +22,7 @@ open HiggsField
 
 noncomputable section
 
+/-! TODO: Make the potential a structure. -/
 /-- The potential of the two Higgs doublet model. -/
 def potential (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ)
     (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ) (Φ1 Φ2 : HiggsField) (x : SpaceTime) : ℝ :=
@@ -88,6 +89,40 @@ lemma left_zero : potential m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m
 def IsBounded (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ) (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ) : Prop :=
   ∃ c, ∀ Φ1 Φ2 x, c ≤ potential m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ Φ1 Φ2 x
 
+lemma isBounded_right_zero {m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ} {m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ}
+    (h : IsBounded m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇) :
+    StandardModel.HiggsField.potential.IsBounded (- m₁₁2) (𝓵₁/2) := by
+  obtain ⟨c, hc⟩ := h
+  use c
+  intro Φ x
+  have hc1 :=  hc Φ 0 x
+  rw [right_zero] at hc1
+  exact hc1
+
+lemma isBounded_left_zero {m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ} {m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ}
+    (h : IsBounded m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇) :
+    StandardModel.HiggsField.potential.IsBounded (- m₂₂2) (𝓵₂/2) := by
+  obtain ⟨c, hc⟩ := h
+  use c
+  intro Φ x
+  have hc1 := hc 0 Φ x
+  rw [left_zero] at hc1
+  exact hc1
+
+lemma isBounded_𝓵₁_nonneg {m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ} {m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ}
+    (h : IsBounded m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇) :
+    0 ≤ 𝓵₁ := by
+  have h1 := isBounded_right_zero h
+  have h2 := StandardModel.HiggsField.potential.isBounded_𝓵_nonneg h1
+  linarith
+
+lemma isBounded_𝓵₂_nonneg {m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ} {m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ}
+    (h : IsBounded m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇) :
+    0 ≤ 𝓵₂ := by
+  have h1 := isBounded_left_zero h
+  have h2 := StandardModel.HiggsField.potential.isBounded_𝓵_nonneg h1
+  linarith
+
 /-! TODO: Show that if the potential is bounded then `0 ≤ 𝓵₁` and `0 ≤ 𝓵₂`. -/
 /-!
 

HepLean/StandardModel/HiggsBoson/Basic.lean

@@ -59,6 +59,18 @@ lemma smooth_toFin2ℂ : Smooth 𝓘(ℝ, HiggsVec) 𝓘(ℝ, Fin 2 → ℂ) toF
 def orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec :=
   EuclideanSpace.basisFun (Fin 2) ℂ
 
+def ofReal (a : ℝ) : HiggsVec :=
+  ![Real.sqrt a, 0]
+
+@[simp]
+lemma ofReal_normSq {a : ℝ} (ha : 0 ≤ a) : ‖ofReal a‖ ^ 2 = a := by
+  simp only [ofReal]
+  rw [PiLp.norm_sq_eq_of_L2]
+  rw [@Fin.sum_univ_two]
+  simp only [Fin.isValue, cons_val_zero, norm_real, Real.norm_eq_abs, _root_.sq_abs, cons_val_one,
+    head_cons, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero]
+  exact Real.sq_sqrt ha
+
 end HiggsVec
 
 /-!
@@ -90,6 +102,9 @@ def HiggsVec.toField (φ : HiggsVec) : HiggsField where
     rw [Bundle.contMDiffAt_section]
     exact smoothAt_const
 
+@[simp]
+lemma HiggsVec.toField_apply (φ : HiggsVec) (x : SpaceTime) : (φ.toField x) = φ := rfl
+
 namespace HiggsField
 open HiggsVec
 
@@ -149,6 +164,8 @@ lemma isConst_of_higgsVec (φ : HiggsVec) : φ.toField.IsConst := fun _ => congr
 lemma isConst_iff_of_higgsVec (Φ : HiggsField) : Φ.IsConst ↔ ∃ (φ : HiggsVec), Φ = φ.toField :=
   Iff.intro (fun h ↦ ⟨Φ 0, by ext x y; rw [← h x 0]; rfl⟩) (fun ⟨φ, hφ⟩ x y ↦ by subst hφ; rfl)
 
+def ofReal (a : ℝ) : HiggsField := (HiggsVec.ofReal a).toField
+
 end HiggsField
 
 end

HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean

@@ -146,6 +146,9 @@ lemma normSq_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ,
     exact ((φ.apply_re_smooth 1).smul (φ.apply_re_smooth 1)).add $
       (φ.apply_im_smooth 1).smul (φ.apply_im_smooth 1)
 
+lemma ofReal_normSq {a : ℝ} (ha : 0 ≤ a) (x : SpaceTime) : (ofReal a).normSq x = a := by
+  simp only [normSq, ofReal, HiggsVec.toField_apply, ha, HiggsVec.ofReal_normSq]
+
 end HiggsField
 
 end StandardModel

HepLean/StandardModel/HiggsBoson/Potential.lean

@@ -62,55 +62,27 @@ lemma complete_square (μ2 𝓵 : ℝ) (h : 𝓵 ≠ 0) (φ : HiggsField) (x : S
   field_simp
   ring
 
-/-!
-
-## Boundness of the potential
-
--/
-
-/-- The proposition on the coefficents for a potential to be bounded. -/
-def IsBounded (μ2 𝓵 : ℝ) : Prop :=
-  ∃ c, ∀ Φ x, c ≤ potential μ2 𝓵 Φ x
-
-/-! TODO: Show when 𝓵 < 0, the potential is not bounded. -/
-
-section lowerBound
-/-!
-
-## Lower bound on potential
-
--/
-
-variable {𝓵 : ℝ}
-variable (μ2 : ℝ)
-variable (h𝓵 : 0 < 𝓵)
-
-include h𝓵
-/-- The second term of the potential is non-negative. -/
-lemma snd_term_nonneg (φ : HiggsField) (x : SpaceTime) :
-    0 ≤ 𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x := by
-  rw [mul_nonneg_iff]
-  apply Or.inl
-  simp_all only [normSq, gt_iff_lt, mul_nonneg_iff_of_pos_left, ge_iff_le, norm_nonneg, pow_nonneg,
-    and_self]
-
-omit h𝓵
 lemma as_quad (μ2 𝓵 : ℝ) (φ : HiggsField) (x : SpaceTime) :
     𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x + (- μ2) * ‖φ‖_H ^ 2 x + (- potential μ2 𝓵 φ x) = 0 := by
   simp only [normSq, neg_mul, potential, neg_add_rev, neg_neg]
   ring
 
-include h𝓵
 /-- The discriminant of the quadratic formed by the potential is non-negative. -/
-lemma discrim_nonneg (φ : HiggsField) (x : SpaceTime) :
+lemma discrim_nonneg (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
     0 ≤ discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) := by
   have h1 := as_quad μ2 𝓵 φ x
   rw [quadratic_eq_zero_iff_discrim_eq_sq] at h1
   · simp only [h1, ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
-    exact sq_nonneg (2 * 𝓵 * ‖φ‖_H ^ 2 x+ - μ2)
-  · exact ne_of_gt h𝓵
+    exact sq_nonneg (2 * 𝓵 * ‖φ‖_H ^ 2 x + - μ2)
+  · exact h
 
-lemma eq_zero_at (φ : HiggsField) (x : SpaceTime)
+lemma discrim_eq_sqrt_discrim_mul_self (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
+    discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) = Real.sqrt (discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x)) *
+      Real.sqrt (discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x)) := by
+  refine Eq.symm (Real.mul_self_sqrt ?h)
+  exact discrim_nonneg μ2 h φ x
+
+lemma eq_zero_at (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime)
     (hV : potential μ2 𝓵 φ x = 0) : φ x = 0 ∨ ‖φ‖_H ^ 2 x = μ2 / 𝓵 := by
   have h1 := as_quad μ2 𝓵 φ x
   rw [hV] at h1
@@ -124,9 +96,191 @@ lemma eq_zero_at (φ : HiggsField) (x : SpaceTime)
     ring_nf
     linear_combination h2
 
+/-- When `0 < 𝓵`, the potential has a lower bound. -/
+lemma bounded_below (μ2 : ℝ) {𝓵 : ℝ} (h𝓵 : 0 < 𝓵) (φ : HiggsField) (x : SpaceTime) :
+    - μ2 ^ 2 / (4 * 𝓵) ≤ potential μ2 𝓵 φ x := by
+  have h1 := discrim_nonneg μ2 (ne_of_lt h𝓵).symm φ x
+  simp only [discrim, even_two, Even.neg_pow, normSq, neg_mul, neg_add_rev, neg_neg] at h1
+  ring_nf at h1
+  rw [← neg_le_iff_add_nonneg'] at h1
+  rw [show 𝓵 * potential μ2 𝓵 φ x * 4 = (4 * 𝓵) * potential μ2 𝓵 φ x by ring] at h1
+  have h2 := (div_le_iff₀' (by simp [h𝓵] : 0 < 4 * 𝓵)).mpr h1
+  ring_nf at h2 ⊢
+  exact h2
+
+/-- When `𝓵 < 0`, the potential has an upper bound. -/
+lemma bounded_above (μ2 : ℝ) {𝓵 : ℝ} (h𝓵 : 𝓵 < 0) (φ : HiggsField) (x : SpaceTime) :
+    potential μ2 𝓵 φ x ≤ - μ2 ^ 2 / (4 * 𝓵) := by
+  have h1 := discrim_nonneg μ2 (ne_of_lt h𝓵) φ x
+  simp only [discrim, even_two, Even.neg_pow, normSq, neg_mul, neg_add_rev, neg_neg] at h1
+  ring_nf at h1
+  rw [← neg_le_iff_add_nonneg'] at h1
+  rw [show 𝓵 * potential μ2 𝓵 φ x * 4 = (- 4 * 𝓵) * (- potential μ2 𝓵 φ x) by ring] at h1
+  have h2 := le_neg_of_le_neg <| (div_le_iff₀' (by linarith : 0 < - 4 * 𝓵)).mpr h1
+  ring_nf at h2 ⊢
+  exact h2
+
+lemma discrim_eq_zero_of_eq_bound (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime)
+    (hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
+    discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) = 0 := by
+  rw [discrim, hV]
+  field_simp
+
+lemma discrim_ge_zero_of_neg_𝓵 (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 < 0) (c : ℝ) :
+    0 ≤ discrim 𝓵 (- μ2) (- c) ↔ c ≤ - μ2 ^ 2 / (4 * 𝓵) := by
+  rw [discrim]
+  simp only [even_two, Even.neg_pow, mul_neg, sub_neg_eq_add]
+  rw [← neg_le_iff_add_nonneg', show 4 * 𝓵 * c = (- 4 * 𝓵) * (- c) by ring,
+    ← (div_le_iff₀' (by linarith : 0 < - 4 * 𝓵)), le_neg]
+  ring_nf
+
+example (a b c : ℝ ) (hc : c < 0) :  a ≤ b / c ↔ b ≤ c * a := by
+  exact le_div_iff_of_neg' hc
+lemma pot_le_zero_of_neg_𝓵 (μ2 : ℝ) {𝓵 : ℝ} (h : 𝓵 < 0) (φ : HiggsField) (x : SpaceTime) :
+    (0 < μ2 ∧ potential μ2 𝓵 φ x ≤ 0) ∨ μ2 ≤ 0 := by
+  by_cases hμ2 : μ2 ≤ 0
+  · simp [hμ2]
+  simp [potential, hμ2]
+  apply And.intro (lt_of_not_ge hμ2)
+  have h1 : 0 ≤  μ2 * ‖φ x‖ ^ 2 := by
+    refine Left.mul_nonneg ?ha ?hb
+    · exact le_of_not_ge hμ2
+    · exact sq_nonneg ‖φ x‖
+  refine le_trans ?_ h1
+  exact mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg (le_of_lt h)
+    (sq_nonneg ‖φ x‖)) (sq_nonneg ‖φ x‖)
+
+lemma exist_sol_iff_of_neg_𝓵 (μ2 : ℝ) {𝓵 : ℝ} (h𝓵 : 𝓵 < 0) (c : ℝ) :
+    (∃ φ x, potential μ2 𝓵 φ x = c) ↔ (0 < μ2 ∧ c ≤ 0) ∨
+    (μ2 ≤ 0 ∧ c ≤ - μ2 ^ 2 / (4 * 𝓵)) := by
+  refine Iff.intro (fun ⟨φ, x, hV⟩ => ?_) (fun h => ?_)
+  · rcases pot_le_zero_of_neg_𝓵 μ2 h𝓵 φ x with hr | hr
+    · rw [← hV]
+      exact Or.inl hr
+    · rw [← hV]
+      exact Or.inr (And.intro hr (bounded_above μ2 h𝓵 φ x))
+  · simp only [potential, neg_mul]
+    simp only [← sub_eq_zero, sub_zero]
+    ring_nf
+    let a := (μ2 - Real.sqrt (discrim 𝓵 (- μ2) (- c))) / (2 * 𝓵)
+    have ha : 0 ≤ a := by
+      simp [a, discrim]
+      rw [div_nonneg_iff]
+      refine Or.inr (And.intro ?_ ?_)
+      · rw [sub_nonpos]
+        by_cases hμ : μ2 < 0
+        · have h1 : 0 ≤ √(μ2 ^ 2 + 4 * 𝓵 * c) := Real.sqrt_nonneg (μ2 ^ 2 + 4 * 𝓵 * c)
+          linarith
+        · refine Real.le_sqrt_of_sq_le ?_
+          rw [le_add_iff_nonneg_right]
+          refine mul_nonneg_of_nonpos_of_nonpos ?_ ?_
+          · refine mul_nonpos_of_nonneg_of_nonpos ?_ ?_
+            · linarith
+            · linarith
+          · rcases h with h | h
+            · linarith
+            · have h1 : μ2 = 0 := by linarith
+              rw [h1] at h
+              simpa using h.2
+      · linarith
+    use (ofReal a)
+    use 0
+    rw [ofReal_normSq ha]
+    trans 𝓵 * a * a + (- μ2) * a + (- c)
+    · ring
+    have hd : 0 ≤ (discrim 𝓵 (-μ2) (-c)) := by
+      simp [discrim]
+      rcases h with h | h
+      · refine Left.add_nonneg (sq_nonneg μ2) ?_
+        refine mul_nonneg_of_nonpos_of_nonpos ?_ h.2
+        linarith
+      · rw [← @neg_le_iff_add_nonneg']
+        rw [← le_div_iff_of_neg']
+        · exact h.2
+        · linarith
+    have hdd : discrim 𝓵 (-μ2) (-c) = Real.sqrt (discrim 𝓵 (-μ2) (-c)) * Real.sqrt (discrim 𝓵 (-μ2) (-c)) := by
+      exact (Real.mul_self_sqrt hd).symm
+    refine (quadratic_eq_zero_iff (ne_of_gt h𝓵).symm hdd _).mpr ?_
+    simp only [neg_neg, or_true, a]
+
+/-!
+
+## Boundness of the potential
+
+-/
+
+/-- The proposition on the coefficents for a potential to be bounded. -/
+def IsBounded (μ2 𝓵 : ℝ) : Prop :=
+  ∃ c, ∀ Φ x, c ≤ potential μ2 𝓵 Φ x
+
+lemma isBounded_𝓵_nonneg {μ2 𝓵 : ℝ} (h : IsBounded μ2 𝓵) :
+    0 ≤ 𝓵 := by
+  by_contra hl
+  simp at hl
+  obtain ⟨c, hc⟩ := h
+  by_cases hμ : μ2 ≤ 0
+  · by_cases hcz : c ≤ -μ2 ^ 2 / (4 * 𝓵)
+    · have hcm1 : ∃ φ x, potential μ2 𝓵 φ x = c - 1 := by
+        rw [propext (exist_sol_iff_of_neg_𝓵 μ2 hl (c - 1))]
+        apply Or.inr
+        simp_all
+        linarith
+      obtain ⟨φ, x, hφ⟩ := hcm1
+      have hc2 := hc φ x
+      rw [hφ] at hc2
+      linarith
+    · simp at hcz
+      have hcm1 : ∃ φ x, potential μ2 𝓵 φ x = -μ2 ^ 2 / (4 * 𝓵) - 1 := by
+        rw [propext (exist_sol_iff_of_neg_𝓵 μ2 hl _)]
+        apply Or.inr
+        simp_all
+      obtain ⟨φ, x, hφ⟩ := hcm1
+      have hc2 := hc φ x
+      rw [hφ] at hc2
+      linarith
+  · simp at hμ
+    by_cases hcz : c ≤ 0
+    · have hcm1 : ∃ φ x, potential μ2 𝓵 φ x = c - 1 := by
+        rw [propext (exist_sol_iff_of_neg_𝓵 μ2 hl (c - 1))]
+        apply Or.inl
+        simp_all
+        linarith
+      obtain ⟨φ, x, hφ⟩ := hcm1
+      have hc2 := hc φ x
+      rw [hφ] at hc2
+      linarith
+    · have hcm1 : ∃ φ x, potential μ2 𝓵 φ x = 0 := by
+        rw [propext (exist_sol_iff_of_neg_𝓵 μ2 hl 0)]
+        apply Or.inl
+        simp_all
+      obtain ⟨φ, x, hφ⟩ := hcm1
+      have hc2 := hc φ x
+      rw [hφ] at hc2
+      linarith
+
+
+
+section lowerBound
+/-!
+
+## Lower bound on potential
+
+-/
+
+variable (μ2 : ℝ) {𝓵 : ℝ} (h𝓵 : 0 < 𝓵)
+
+include h𝓵
+/-- The second term of the potential is non-negative. -/
+lemma snd_term_nonneg (φ : HiggsField) (x : SpaceTime) :
+    0 ≤ 𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x := by
+  rw [mul_nonneg_iff]
+  apply Or.inl
+  simp_all only [normSq, gt_iff_lt, mul_nonneg_iff_of_pos_left, ge_iff_le, norm_nonneg, pow_nonneg,
+    and_self]
+
 lemma eq_zero_at_of_μSq_nonpos {μ2 : ℝ} (hμ2 : μ2 ≤ 0)
     (φ : HiggsField) (x : SpaceTime) (hV : potential μ2 𝓵 φ x = 0) : φ x = 0 := by
-  cases' (eq_zero_at μ2 h𝓵 φ x hV) with h1 h1
+  cases' (eq_zero_at μ2 (ne_of_lt h𝓵).symm φ x hV) with h1 h1
   · exact h1
   · by_cases hμSqZ : μ2 = 0
     · simpa [hμSqZ] using h1
@@ -137,17 +291,6 @@ lemma eq_zero_at_of_μSq_nonpos {μ2 : ℝ} (hμ2 : μ2 ≤ 0)
       · rw [← h1]
         exact normSq_nonneg φ x
 
-lemma bounded_below (φ : HiggsField) (x : SpaceTime) :
-    - μ2 ^ 2 / (4 * 𝓵) ≤ potential μ2 𝓵 φ x := by
-  have h1 := discrim_nonneg μ2 h𝓵 φ x
-  simp only [discrim, even_two, Even.neg_pow, normSq, neg_mul, neg_add_rev, neg_neg] at h1
-  ring_nf at h1
-  rw [← neg_le_iff_add_nonneg'] at h1
-  rw [show 𝓵 * potential μ2 𝓵 φ x * 4 = (4 * 𝓵) * potential μ2 𝓵 φ x by ring] at h1
-  have h2 := (div_le_iff₀' (by simp [h𝓵] : 0 < 4 * 𝓵)).mpr h1
-  ring_nf at h2 ⊢
-  exact h2
-
 lemma bounded_below_of_μSq_nonpos {μ2 : ℝ}
     (hμSq : μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) : 0 ≤ potential μ2 𝓵 φ x := by
   refine add_nonneg ?_ (snd_term_nonneg h𝓵 φ x)
@@ -167,12 +310,6 @@ variable (h𝓵 : 0 < 𝓵)
 
 -/
 
-include h𝓵
-lemma discrim_eq_zero_of_eq_bound (φ : HiggsField) (x : SpaceTime)
-    (hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
-    discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) = 0 := by
-  rw [discrim, hV]
-  field_simp
 
 include h𝓵
 lemma normSq_of_eq_bound (φ : HiggsField) (x : SpaceTime)
@@ -180,7 +317,7 @@ lemma normSq_of_eq_bound (φ : HiggsField) (x : SpaceTime)
     ‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) := by
   have h1 := as_quad μ2 𝓵 φ x
   rw [quadratic_eq_zero_iff_of_discrim_eq_zero _
-    (discrim_eq_zero_of_eq_bound μ2 h𝓵 φ x hV)] at h1
+    (discrim_eq_zero_of_eq_bound μ2 (ne_of_lt h𝓵).symm φ x hV)] at h1
   · simp_rw [h1, neg_neg]
   · exact ne_of_gt h𝓵