1. Physlib
  2. Particles
  3. SuperSymmetry
  4. SU5
  5. ChargeSpectrum
  6. OfPotentialTerm
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfFieldLabel public import Physlib.Particles.SuperSymmetry.SU5.Potential public import Mathlib.Tactic.Abel

Charges associated with a potential term

i. Overview

In this module we give the multiset of charges associated with a given type of potential term, given a charge spectrum.

We will define two versions of this, one based on the underlying fields on the potentials, and the charges that they carry, and one more explicit version which is faster to compute with. The former is ofPotentialTerm, and the latter is ofPotentialTerm'.

We will show that these two multisets have the same elements.

ii. Key results

    ofPotentialTerm : The multiset of charges associated with a potential term, defined in terms of the fields making up that potential term, given a charge spectrum.

    ofPotentialTerm' : The multiset of charges associated with a potential term, defined explicitly, given a charge spectrum.

iii. Table of contents

    A. Charges of a potential term from field labels

      A.1. Monotonicity of ofPotentialTerm

      A.2. Charges of potential terms for the empty charge spectrum

    B. Explicit construction of charges of a potential term

      B.1. Explicit multisets for ofPotentialTerm'

      B.2. ofPotentialTerm' on the empty charge spectrum

    C. Relation between two constructions of charges of potential terms

      C.1. Showing that ofPotentialTerm is a subset of ofPotentialTerm'

      C.2. Showing that ofPotentialTerm' is a subset of ofPotentialTerm

      C.3. Equivalence of elements of ofPotentialTerm and ofPotentialTerm'

      C.4. Induced monotonicity of ofPotentialTerm'

iv. References

There are no known references for this material.

@[expose] public section

A. Charges of a potential term from field labels

We first define ofPotentialTerm, and prover properties of it. This is slow to compute in practice.

Given a charges x : Charges associated to the representations, and a potential term T, the charges associated with instances of that potential term.

def ofPotentialTerm (x : ChargeSpectrum 𝓩) (T : PotentialTerm) : Multiset 𝓩 := let add : Multiset 𝓩 β†’ Multiset 𝓩 β†’ Multiset 𝓩 := fun a b => (a Γ—Λ’ b).map fun (x, y) => x + y (T.toFieldLabel.map fun F => (ofFieldLabel x F).val).foldl add {0}

A.1. Monotonicity of ofPotentialTerm

We show that ofPotentialTerm is monotone in its charge spectrum argument. That is if x βŠ† y then ofPotentialTerm x T βŠ† ofPotentialTerm y T.

𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10T:PotentialTermh1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm T βŠ† y.ofPotentialTerm T 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm ΞΌ βŠ† y.ofPotentialTerm μ𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm Ξ² βŠ† y.ofPotentialTerm β𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm Ξ› βŠ† y.ofPotentialTerm Λ𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm W1 βŠ† y.ofPotentialTerm W1𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm W2 βŠ† y.ofPotentialTerm W2𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm W3 βŠ† y.ofPotentialTerm W3𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm W4 βŠ† y.ofPotentialTerm W4𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm K1 βŠ† y.ofPotentialTerm K1𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm K2 βŠ† y.ofPotentialTerm K2𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm topYukawa βŠ† y.ofPotentialTerm topYukawa𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ x.ofPotentialTerm bottomYukawa βŠ† y.ofPotentialTerm bottomYukawa all_goals 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ Multiset.map (fun x => x.1 + x.2) (Multiset.map (fun x => x.1 + x.2) (Multiset.map (fun x => x.1 + x.2) ({0} Γ—Λ’ (x.ofFieldLabel FieldLabel.tenMatter).val) Γ—Λ’ (x.ofFieldLabel FieldLabel.fiveBarMatter).val) Γ—Λ’ (x.ofFieldLabel FieldLabel.fiveBarHd).val) βŠ† Multiset.map (fun x => x.1 + x.2) (Multiset.map (fun x => x.1 + x.2) (Multiset.map (fun x => x.1 + x.2) ({0} Γ—Λ’ (y.ofFieldLabel FieldLabel.tenMatter).val) Γ—Λ’ (y.ofFieldLabel FieldLabel.fiveBarMatter).val) Γ—Λ’ (y.ofFieldLabel FieldLabel.fiveBarHd).val) repeat' 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x.qHd.toFinset βŠ† y.qHd.toFinset ∧ x.qHu.toFinset βŠ† y.qHu.toFinset ∧ x.Q5 βŠ† y.Q5 ∧ x.Q10 βŠ† y.Q10h1:βˆ€ {S1 S2 T1 T2 : Multiset 𝓩}, S1 βŠ† S2 β†’ T1 βŠ† T2 β†’ S1 Γ—Λ’ T1 βŠ† S2 Γ—Λ’ T2⊒ {0} βŠ† {0} All goals completed! πŸ™

A.2. Charges of potential terms for the empty charge spectrum

For the empty charge spectrum, the charges associated with any potential term is empty.

@[simp] lemma ofPotentialTerm_empty (T : PotentialTerm) : ofPotentialTerm (βˆ… : ChargeSpectrum 𝓩) T = βˆ… := 𝓩:Typeinst✝:AddCommGroup 𝓩T:PotentialTerm⊒ βˆ….ofPotentialTerm T = βˆ… 𝓩:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm ΞΌ = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm Ξ² = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm Ξ› = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm W1 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm W2 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm W3 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm W4 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm K1 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm K2 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm topYukawa = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm bottomYukawa = βˆ… all_goals All goals completed! πŸ™

B. Explicit construction of charges of a potential term

We now turn to a more explicit construction of the charges associated with a potential term. This is faster to compute with, but less obviously connected to the underlying fields.

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 ofPotentialTerm' (y : ChargeSpectrum 𝓩) (T : PotentialTerm) : Multiset 𝓩 := let qHd := y.qHd let qHu := y.qHu let Q5 := y.Q5 let Q10 := y.Q10 match T with | ΞΌ => match qHd, qHu with | none, _ => βˆ… | _, none => βˆ… | some qHd, some qHu => {qHd - qHu} | Ξ² => match qHu with | none => βˆ… | some qHu => Q5.val.map (fun x => - qHu + x) | Ξ› => (Q5.product <| Q5.product <| Q10).val.map (fun x => x.1 + x.2.1 + x.2.2) | W1 => (Q5.product <| Q10.product <| Q10.product <| Q10).val.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) | W2 => match qHd with | none => βˆ… | some qHd => (Q10.product <| Q10.product <| Q10).val.map (fun x => qHd + x.1 + x.2.1 + x.2.2) | W3 => match qHu with | none => βˆ… | some qHu => (Q5.product <| Q5).val.map (fun x => -qHu - qHu + x.1 + x.2) | W4 => match qHd, qHu with | none, _ => βˆ… | _, none => βˆ… | some qHd, some qHu => Q5.val.map (fun x => qHd - qHu - qHu + x) | K1 => (Q5.product <| Q10.product <| Q10).val.map (fun x => - x.1 + x.2.1 + x.2.2) | K2 => match qHd, qHu with | none, _ => βˆ… | _, none => βˆ… | some qHd, some qHu => Q10.val.map (fun x => qHd + qHu + x) | topYukawa => match qHu with | none => βˆ… | some qHu => (Q10.product <| Q10).val.map (fun x => - qHu + x.1 + x.2) | bottomYukawa => match qHd with | none => βˆ… | some qHd => (Q5.product <| Q10).val.map (fun x => qHd + x.1 + x.2)

B.1. Explicit multisets for ofPotentialTerm'

For each potential term, we give an explicit form of the multiset ofPotentialTerm'.

lemma ofPotentialTerm'_ΞΌ_finset {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' ΞΌ = (x.qHd.toFinset.product <| x.qHu.toFinset).val.map (fun x => x.1 - x.2) := 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum π“©βŠ’ x.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) (x.qHd.toFinset.product x.qHu.toFinset).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' ΞΌ = Multiset.map (fun x => x.1 - x.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset).val All goals completed! πŸ™lemma ofPotentialTerm'_Ξ²_finset {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' Ξ² = (x.qHu.toFinset.product <| x.Q5).val.map (fun x => - x.1 + x.2) := 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum π“©βŠ’ x.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) (x.qHu.toFinset.product x.Q5).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' Ξ² = Multiset.map (fun x => -x.1 + x.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5).val All goals completed! πŸ™lemma ofPotentialTerm'_W2_finset {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' W2 = (x.qHd.toFinset.product <| x.Q10.product <| x.Q10.product <| x.Q10).val.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) := 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum π“©βŠ’ x.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) (x.qHd.toFinset.product (x.Q10.product (x.Q10.product x.Q10))).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10))).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10))).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10))).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10))).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10))).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10))).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10))).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10))).val All goals completed! πŸ™lemma ofPotentialTerm'_W3_finset {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' W3 = (x.qHu.toFinset.product <| x.Q5.product <| x.Q5).val.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) := 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum π“©βŠ’ x.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) (x.qHu.toFinset.product (x.Q5.product x.Q5)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W3 = Multiset.map (fun x => -x.1 - x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5)).val All goals completed! πŸ™lemma ofPotentialTerm'_W4_finset {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' W4 = (x.qHd.toFinset.product <| x.qHu.toFinset.product <| x.Q5).val.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) := 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum π“©βŠ’ x.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) (x.qHd.toFinset.product (x.qHu.toFinset.product x.Q5)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' W4 = Multiset.map (fun x => x.1 - x.2.1 - x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5)).val All goals completed! πŸ™lemma ofPotentialTerm'_K2_finset {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' K2 = (x.qHd.toFinset.product <| x.qHu.toFinset.product <| x.Q10).val.map (fun x => x.1 + x.2.1 + x.2.2) := 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum π“©βŠ’ x.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) (x.qHd.toFinset.product (x.qHu.toFinset.product x.Q10)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' K2 = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val All goals completed! πŸ™lemma ofPotentialTerm'_topYukawa_finset {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' topYukawa = (x.qHu.toFinset.product <| x.Q10.product <| x.Q10).val.map (fun x => -x.1 + x.2.1 + x.2.2) := 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum π“©βŠ’ x.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) (x.qHu.toFinset.product (x.Q10.product x.Q10)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' topYukawa = Multiset.map (fun x => -x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHu.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val All goals completed! πŸ™lemma ofPotentialTerm'_bottomYukawa_finset {x : ChargeSpectrum 𝓩} : x.ofPotentialTerm' bottomYukawa = (x.1.toFinset.product <| x.Q5.product <| x.Q10).val.map (fun x => x.1 + x.2.1 + x.2.2) := 𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum π“©βŠ’ x.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) (x.qHd.toFinset.product (x.Q5.product x.Q10)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val 𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset π“©βŠ’ { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := none, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHu:π“©βŠ’ { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := none, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:π“©βŠ’ { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := some qHd, qHu := none, Q5 := Q5, Q10 := Q10 }.Q10)).val𝓩:Typeinst✝:AddCommGroup 𝓩Q5:Finset 𝓩Q10:Finset 𝓩qHd:𝓩qHu:π“©βŠ’ { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.ofPotentialTerm' bottomYukawa = Multiset.map (fun x => x.1 + x.2.1 + x.2.2) ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.qHd.toFinset.product ({ qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q5.product { qHd := some qHd, qHu := some qHu, Q5 := Q5, Q10 := Q10 }.Q10)).val All goals completed! πŸ™

B.2. ofPotentialTerm' on the empty charge spectrum

We show that for the empty charge spectrum, the charges associated with any potential term is empty, as defined through ofPotentialTerm'.

@[simp] lemma ofPotentialTerm'_empty (T : PotentialTerm) : ofPotentialTerm' (βˆ… : ChargeSpectrum 𝓩) T = βˆ… := 𝓩:Typeinst✝:AddCommGroup 𝓩T:PotentialTerm⊒ βˆ….ofPotentialTerm' T = βˆ… 𝓩:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' ΞΌ = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' Ξ² = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' Ξ› = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' W1 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' W2 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' W3 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' W4 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' K1 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' K2 = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' topYukawa = βˆ…π“©:Typeinst✝:AddCommGroup π“©βŠ’ βˆ….ofPotentialTerm' bottomYukawa = βˆ… all_goals All goals completed! πŸ™

C. Relation between two constructions of charges of potential terms

We now give the relation between ofPotentialTerm and ofPotentialTerm'. We show that they have the same elements, by showing that they are subsets of each other.

The prove of some of these results are rather long since they involve explicit case analysis for each potential term, due to the nature of the definition of ofPotentialTerm'.

C.1. Showing that ofPotentialTerm is a subset of ofPotentialTerm'

We first show that ofPotentialTerm is a subset of ofPotentialTerm'.

𝓩:Typeinst✝:AddCommGroup 𝓩x:ChargeSpectrum 𝓩n:𝓩f2:𝓩f4:𝓩f6:𝓩f8:𝓩f2_mem:f2 ∈ x.Q5f4_mem:f4 ∈ x.Q10f6_mem:f6 ∈ x.Q10f8_mem:f8 ∈ x.Q10f1_add_f2_eq_zero:f8 + f6 + f4 + f2 = n⊒ f2 + f4 + f6 + f8 = f8 + f6 + f4 + f2 All goals completed! πŸ™

C.2. Showing that ofPotentialTerm' is a subset of ofPotentialTerm

We now show the other direction of the subset relation, that ofPotentialTerm' is a subset of ofPotentialTerm.

𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:𝓩q1:𝓩q2:𝓩q_sum:q1 - q2 = nq1_mem:x.qHd = some q1q2_mem:x.qHu = some q2⊒ q1 - q2 = q1 + -q2 try All goals completed! πŸ™

C.3. Equivalence of elements of ofPotentialTerm and ofPotentialTerm'

We now show that a charge is in ofPotentialTerm if and only if it is in ofPotentialTerm'. I.e. their underlying finite sets are equal. We do not say anything about the multiplicity of elements within the multisets, which is not important for us.

lemma mem_ofPotentialTerm_iff_mem_ofPotentialTerm [DecidableEq 𝓩] {T : PotentialTerm} {n : 𝓩} {y : ChargeSpectrum 𝓩} : n ∈ y.ofPotentialTerm T ↔ n ∈ y.ofPotentialTerm' T := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermn:𝓩y:ChargeSpectrum π“©βŠ’ n ∈ y.ofPotentialTerm T ↔ n ∈ y.ofPotentialTerm' T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermn:𝓩y:ChargeSpectrum π“©βŠ’ n ∈ y.ofPotentialTerm T β†’ n ∈ y.ofPotentialTerm' T𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermn:𝓩y:ChargeSpectrum π“©βŠ’ n ∈ y.ofPotentialTerm' T β†’ n ∈ y.ofPotentialTerm T 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermn:𝓩y:ChargeSpectrum π“©βŠ’ n ∈ y.ofPotentialTerm T β†’ n ∈ y.ofPotentialTerm' T All goals completed! πŸ™ 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩T:PotentialTermn:𝓩y:ChargeSpectrum π“©βŠ’ n ∈ y.ofPotentialTerm' T β†’ n ∈ y.ofPotentialTerm T All goals completed! πŸ™

C.4. Induced monotonicity of ofPotentialTerm'

Due to the equivalence of elements of ofPotentialTerm and ofPotentialTerm', we can now also show that ofPotentialTerm' is monotone in its charge spectrum argument.

𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x βŠ† yT:PotentialTermi:π“©βŠ’ i ∈ x.ofPotentialTerm T β†’ i ∈ y.ofPotentialTerm T All goals completed! πŸ™