Research proof index

Given a charges x : ChargeSpectrum associated to the representations, and a potential term T, the charges associated with instances of that potential term. This is a more explicit form of PotentialTerm, which has the benefit that it is quick with decide, but it is not defined based on more fundamental concepts, like ofPotentialTerm is. -/ def of...

Given a charges x : ChargeSpectrum associated to the representations, and a potential term T, the charges associated with instances of that potential term. This is a more explicit form of PotentialTerm, which has the benefit that it is quick with decide, but it is not defined based on more fundamental concepts, like ofPotentialTerm is. -/ def of...

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

The preimage of a charge Charges 𝓩1 in ofFinset S5 S10 ⊆ Charges 𝓩 under mapping charges through f : 𝓩 →+ 𝓩1. -/ def preimageOfFinset (S5 S10 : Finset 𝓩) (f : 𝓩 →+ 𝓩1) (x : ChargeSpectrum 𝓩1) : Finset (ChargeSpectrum 𝓩) := let SHd := (S5.map ⟨Option.some, Option.some_injective 𝓩⟩ ∪ {none} : Finset (Option 𝓩)).filter fun y => f <$> y = x.q...

Given a collection of charges x in ofFinset S5 S10, the minimal charges y in ofFinset S5 S10 which are a super sets of x. -/ def minimalSuperSet (S5 S10 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : Finset (ChargeSpectrum 𝓩) := let SqHd := if x.qHd.isSome then ∅ else S5.map ⟨fun y => ⟨some y, x.qHu, x.Q5, x.Q10⟩, by intro y1 y2; simp⟩ let SqHu := if x...

Given a collection of charges x in ofFinset S5 S10, the minimal charges y in ofFinset S5 S10 which are a super sets of x. -/ def minimalSuperSet (S5 S10 : Finset 𝓩) (x : ChargeSpectrum 𝓩) : Finset (ChargeSpectrum 𝓩) := let SqHd := if x.qHd.isSome then ∅ else S5.map ⟨fun y => ⟨some y, x.qHu, x.Q5, x.Q10⟩, by intro y1 y2; simp⟩ let SqHu := if x...