Forall reduced exists not potential Is Stable

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. -/  refine ⟨.stabilityCounterExample, stabilityCounterExample_not_potentialIsStable,    fun k hk => ⟨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]