feat(strings): update charges defns in SU(5) x U(1) (#601)

* feat: Update chargeProfile

* refactor: Remove charge profile

* feat: Change R-parity

* feat: ofFinset_of_mem_irreducibleOfFinset

* feat: Split up charges file

* chore: Rename IsPresent -> AllowsTerm

* refactor: AllowsTerm file

* feat: MinimallyAllowsTerm

* refactor: Style lint

* refactor: style lint

* feat: Delete all files

* refactor: LInt

Author: jstoobysmith

PhysLean.lean

@@ -257,7 +257,12 @@ import PhysLean.Relativity.Tensors.TensorSpecies.Basic
 import PhysLean.Relativity.Tensors.UnitTensor
 import PhysLean.StatisticalMechanics.Basic
 import PhysLean.StringTheory.Basic
+import PhysLean.StringTheory.FTheory.SU5U1.Charges.AllowsTerm
 import PhysLean.StringTheory.FTheory.SU5U1.Charges.Basic
+import PhysLean.StringTheory.FTheory.SU5U1.Charges.MinimallyAllowsTerm.Basic
+import PhysLean.StringTheory.FTheory.SU5U1.Charges.MinimallyAllowsTerm.OfFinset
+import PhysLean.StringTheory.FTheory.SU5U1.Charges.OfFieldLabel
+import PhysLean.StringTheory.FTheory.SU5U1.Charges.OfPotentialTerm
 import PhysLean.StringTheory.FTheory.SU5U1.Charges.OfRationalSection
 import PhysLean.StringTheory.FTheory.SU5U1.Charges.PhenoConstrained.Basic
 import PhysLean.StringTheory.FTheory.SU5U1.Charges.PhenoConstrained.Completeness
@@ -278,10 +283,6 @@ import PhysLean.StringTheory.FTheory.SU5U1.Fluxes.NoExotics.Completeness
 import PhysLean.StringTheory.FTheory.SU5U1.Fluxes.NoExotics.Elems
 import PhysLean.StringTheory.FTheory.SU5U1.Fluxes.NoExotics.ToList
 import PhysLean.StringTheory.FTheory.SU5U1.Potential.Basic
-import PhysLean.StringTheory.FTheory.SU5U1.Potential.ChargeProfile.Basic
-import PhysLean.StringTheory.FTheory.SU5U1.Potential.ChargeProfile.Irreducible.Basic
-import PhysLean.StringTheory.FTheory.SU5U1.Potential.ChargeProfile.Irreducible.Completeness
-import PhysLean.StringTheory.FTheory.SU5U1.Potential.ChargeProfile.Irreducible.Elems
 import PhysLean.StringTheory.FTheory.SU5U1.Quanta.AnomalyCancellation
 import PhysLean.StringTheory.FTheory.SU5U1.Quanta.Basic
 import PhysLean.StringTheory.FTheory.SU5U1.Quanta.FromParts

PhysLean/Mathematics/DataStructures/FourTree/Basic.lean

@@ -208,23 +208,23 @@ def Trunk.mem (T : Trunk α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Prop
   | .trunk xo branches => xo = x.1 ∧ ∃ branch ∈ branches, branch.mem x.2
 
 instance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4]
-    (T : Trunk α1 α2 α3 α4) (x :  α1 × α2 × α3 × α4) : Decidable (T.mem x) :=
+    (T : Trunk α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (T.mem x) :=
   match T with
   | .trunk _ branches =>
     haveI : Decidable (∃ branch ∈ branches, branch.mem x.2) := Multiset.decidableExistsMultiset
     instDecidableAnd
 
 /-- An element of `a : α1 × α2 × α3 × α4` is a member of `FourTree α1 α2 α3 α4` if
   `a` is a member of one of the `Trunk`. -/
-def mem (T : FourTree α1 α2 α3 α4) (x :  α1 × α2 × α3 × α4) : Prop :=
+def mem (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Prop :=
   match T with
   | .root trunks => ∃ trunk ∈ trunks, trunk.mem x
 
 instance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4]
-    (T : FourTree α1 α2 α3 α4) (x :  α1 × α2 × α3 × α4) : Decidable (T.mem x) :=
+    (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (T.mem x) :=
   Multiset.decidableExistsMultiset
 
-instance : Membership ( α1 × α2 × α3 × α4) (FourTree α1 α2 α3 α4)where
+instance : Membership (α1 × α2 × α3 × α4) (FourTree α1 α2 α3 α4) where
   mem := mem
 
 instance [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4]

PhysLean/Mathematics/DataStructures/FourTree/UniqueMap.lean

@@ -36,7 +36,7 @@ def Leaf.uniqueMap4 : Leaf α4 → Leaf α4
 
 /-- Given a map `f : α4 → α4` the map from `Twig α3 α4 → Twig α3 α4` mapping the underlying
   leafs and deleting any that appear in the original Twig. -/
-def Twig.uniqueMap4 (T : Twig α3 α4)  : Twig α3 α4 :=
+def Twig.uniqueMap4 (T : Twig α3 α4) : Twig α3 α4 :=
   match T with
   | .twig xs leafs =>
     let leafFinst := leafs.map (fun l => match l with
@@ -66,7 +66,7 @@ def Trunk.uniqueMap4 (T : Trunk α1 α2 α3 α4) : Trunk α1 α2 α3 α4 :=
 /-- Given a map `f : α4 → α4` the map from `FourTree α1 α2 α3 α4 → FourTree α1 α2 α3 α4`
   mapping the underlying leafs and deleting any that appear in the original twig of that
   leaf. -/
-def uniqueMap4 (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4  :=
+def uniqueMap4 (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4 :=
   match T with
   | .root trunks =>
     .root (trunks.map fun ts => (ts.uniqueMap4 f))
@@ -163,7 +163,6 @@ lemma exists_of_mem_uniqueMap4 {T : FourTree α1 α2 α3 α4}
 
 end uniqueMap4
 
-
 /-!
 
 ## uniqueMap3
@@ -174,14 +173,12 @@ section uniqueMap3
 
 variable {α1 α2 α3 α4 : Type} [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (f : α3 → α3)
 
-
 /-- Given a map `f : α3 → α3` the map from `Twig α3 α4 → Twig α3 α4` mapping the underlying
   first value of the twig. -/
 def Twig.uniqueMap3 (T : Twig α3 α4) : Twig α3 α4 :=
   match T with
   | .twig xs leafs => .twig (f xs) leafs
 
-
 /-- Given a map `f : α3 → α3` the map from `Branch α2 α3 α4 → Branch α2 α3 α4` mapping the
   underlying first value of the twig, and deleting any new leafs that appeared
   in the old branch. -/
@@ -210,7 +207,7 @@ def uniqueMap3 (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4:=
     .root (trunks.map fun ts => (ts.uniqueMap3 f))
 
 lemma map_mem_uniqueMap3 {T : FourTree α1 α2 α3 α4}
-    (x : α1 × α2 × α3 × α4) (hx : x ∈ T) (f : α3 → α3):
+    (x : α1 × α2 × α3 × α4) (hx : x ∈ T) (f : α3 → α3) :
     (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T.uniqueMap3 f ∨
     (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T := by
   by_cases hnotMem : (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T
@@ -296,7 +293,6 @@ lemma exists_of_mem_uniqueMap3 {T : FourTree α1 α2 α3 α4}
   apply mem_of_parts trunkT branchT twigT leafI
   all_goals simp_all
 
-
 end uniqueMap3
 
 end FourTree