PhysLean Documentation

PhysLean.StringTheory.FTheory.SU5U1.Charges.Tree

Trees of charges #

It is convient to use FourTree to store charges. In this file we make some auxillary definitions and lemmas which will help us in proofs and make things faster.

In particular we define the root, trunk, branch, twig and leaf specifically for FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ), this allows Lean to read in large trees of charges more quickly.

We also prove some results related to (T.uniqueMap3 (insert q5.1)) and (T.uniqueMap4 (insert q10.1)), and their filters by a predicate p : Charges → Prop.

source
instance FTheory.SU5U1.Charges.Tree.instDecidableMemFourTreeOptionIntFinset (T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : Charges) :
Decidable (x ∈ T)
Equations
source
def FTheory.SU5U1.Charges.Tree.root :
Multiset (PhysLean.FourTree.Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) → PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

An explicit form of FourTree.root for charges.

Equations
Instances For
    source
    def FTheory.SU5U1.Charges.Tree.trunk :
    Option ℤ → Multiset (PhysLean.FourTree.Branch (Option ℤ) (Finset ℤ) (Finset ℤ)) → PhysLean.FourTree.Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

    An explicit form of FourTree.Trunk.trunk for charges.

    Equations
    Instances For
      source
      def FTheory.SU5U1.Charges.Tree.branch :
      Option ℤ → Multiset (PhysLean.FourTree.Twig (Finset ℤ) (Finset ℤ)) → PhysLean.FourTree.Branch (Option ℤ) (Finset ℤ) (Finset ℤ)

      An explicit form of FourTree.Branch.branch for charges.

      Equations
      Instances For
        source
        def FTheory.SU5U1.Charges.Tree.twig :
        Finset ℤ → Multiset (PhysLean.FourTree.Leaf (Finset ℤ)) → PhysLean.FourTree.Twig (Finset ℤ) (Finset ℤ)

        An explicit form of FourTree.Twig.twig for charges.

        Equations
        Instances For
          source
          def FTheory.SU5U1.Charges.Tree.leaf :
          Finset ℤ → PhysLean.FourTree.Leaf (Finset ℤ)

          An explicit form of FourTree.Leaf.leaf for charges.

          Equations
          Instances For

            Inserting charges and minimal super sets #

            source
            theorem FTheory.SU5U1.Charges.Tree.insert_filter_card_zero (T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (S5 S10 : Finset ℤ) (p : Charges → Prop) [DecidablePred p] (hComplet : ∀ x ∈ T, IsComplete x) (h10 : ∀ (q10 : { x : ℤ // x ∈ S10 }), Multiset.filter p (PhysLean.FourTree.uniqueMap4 (insert ↑q10) T).toMultiset = ∅) (h5 : ∀ (q5 : { x : ℤ // x ∈ S5 }), Multiset.filter p (PhysLean.FourTree.uniqueMap3 (insert ↑q5) T).toMultiset = ∅) (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) :
            x ∈ T → ∀ y ∈ minimalSuperSet S5 S10 x, y ∉ T → ¬p y
            source
            theorem FTheory.SU5U1.Charges.Tree.subset_insert_filter_card_zero_inductive (T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (S5 S10 : Finset ℤ) (p : Charges → Prop) [DecidablePred p] (hnotSubset : ∀ (x y : Charges), x ⊆ y → ¬p x → ¬p y) (hComplet : ∀ x ∈ T, IsComplete x) (x : Charges) (hx : x ∈ T) (y : Charges) (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (h10 : ∀ (q10 : { x : ℤ // x ∈ S10 }), Multiset.filter p (PhysLean.FourTree.uniqueMap4 (insert ↑q10) T).toMultiset = ∅) (h5 : ∀ (q5 : { x : ℤ // x ∈ S5 }), Multiset.filter p (PhysLean.FourTree.uniqueMap3 (insert ↑q5) T).toMultiset = ∅) (n : ℕ) (hn : n = y.card - x.card) :
            y ∉ T → ¬p y
            source
            theorem FTheory.SU5U1.Charges.Tree.subset_insert_filter_card_zero (T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (S5 S10 : Finset ℤ) (p : Charges → Prop) [DecidablePred p] (hnotSubset : ∀ (x y : Charges), x ⊆ y → ¬p x → ¬p y) (hComplet : ∀ x ∈ T, IsComplete x) (x : Charges) (hx : x ∈ T) (y : Charges) (hsubset : x ⊆ y) (hy : y ∈ ofFinset S5 S10) (h10 : ∀ (q10 : { x : ℤ // x ∈ S10 }), Multiset.filter p (PhysLean.FourTree.uniqueMap4 (insert ↑q10) T).toMultiset = ∅) (h5 : ∀ (q5 : { x : ℤ // x ∈ S5 }), Multiset.filter p (PhysLean.FourTree.uniqueMap3 (insert ↑q5) T).toMultiset = ∅) :
            y ∉ T → ¬p y

            For a proposition p if (T.uniqueMap4 (insert q10.1)).toMultiset.filter p and (T.uniqueMap3 (insert q5.1)).toMultiset.filter p for all q5 ∈ S5 and q10 ∈ S10 then if x ∈ T and x ⊆ y if y ∉ T then ¬ p y. This assumes that all charges in T are complete, and that p satisfies x ⊆ y → ¬ p x → ¬ p y.