Research proof index

The charges of those terms which can be regenerated with up-to n insertions of singlets needed to regenerate the Yukawa terms. Equivalently, the sum of up-to n integers each corresponding to a charge of the Yukawa terms. -/ def ofYukawaTermsNSum (x : ChargeSpectrum 𝓩) : ℕ → Multiset 𝓩 | 0 => {0} | n + 1 => x.ofYukawaTermsNSum n + (x.ofYukawaTermsNSu...

For charges x : Charges, the proposition which states that the singlets needed to regenerate the Yukawa couplings regenerate a dangerous coupling (in the superpotential) with up-to n insertions of the scalars. Note: If defined as (x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset ≠ ∅ the execution time is greatly increased. -/ de...