Research proof index

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 *...

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.

The potential stabilityCounterExample is not stable.

The lemma that the proposition EnergyMass is dimensionally correct

Gives a factor of - 1 for every fermion-fermion (q is 1) crossing that occurs when sorting a list of based on r. -/ def koszulSign (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] : List 𝓕 → ℂ | [] => 1 | a :: l => koszulSignInsert q le a l * koszulSign q le l @[simp] lemma koszulSign_singleton (q : 𝓕 → FieldStatistic) (le : 𝓕...

Given a Wick contraction φsΛ for a list φs of 𝓕.FieldOp, an element φ of 𝓕.FieldOp, an i ≤ φs.length and a k in Option φsΛ.uncontracted i.e. is either none or some element of φsΛ.uncontracted, the new Wick contraction φsΛ.insertAndContract φ i k is defined by inserting φ into φs after the first i-elements and moving the value...