Pheno constrained charges

We say a charge is pheno-constrained if it leads to allows proton decay or R-parity violating terms.

We are actually intrested in the charges which are not pheno-constrained.

def FTheory.SU5U1.Charges.IsPhenoConstrained (x : Charges) : Prop

A charge is pheno-constrained if it leads to the presence of any term causing proton decay {W1, Λ, W2, K1} or R-parity violation {β, Λ, W2, W4, K1, K2}.

Equations

• One or more equations did not get rendered due to their size.

instance FTheory.SU5U1.Charges.decidableIsPhenoConstrained (x : Charges) : Decidable x.IsPhenoConstrained

Equations

• One or more equations did not get rendered due to their size.

theorem FTheory.SU5U1.Charges.isPhenoConstrained_of_subset {x y : Charges} (h : x ⊆ y) (hx : x.IsPhenoConstrained) : y.IsPhenoConstrained

def FTheory.SU5U1.Charges.phenoConstrainingChargesSP (x : Charges) : Multiset ℤ

The collection of charges of super-potential terms leading to a pheno-constrained model.

Equations

• One or more equations did not get rendered due to their size.

Inserting charges into trees, with pheno constraints

We define two functions phenoInsertQ10 and phenoInsertQ5 which for a tree T respectively give all not pheno-constrained new charges obtained by inserting a q10 or q5 charge into the charges in T.

This is related to the insertQ10 and insertQ5 functions, which insert a charge into a tree T, but do not check if the new charges is pheno-constrained.

Inserting q10 charges into trees

def FTheory.SU5U1.Charges.Tree.Twig.phenoInsertQ10 (t : PhysLean.FourTree.Twig (Finset ℤ) (Finset ℤ)) (qHd : Option ℤ) (x : ℤ) : PhysLean.FourTree.Twig (Finset ℤ) (Finset ℤ)

The twig obtained by taking the new, not pheno-constrained, charges obtained by inserting q10 into all leafs of a twig. This assumes that all existing charges in the twig are already not pheno constrained.

Equations

• One or more equations did not get rendered due to their size.

def FTheory.SU5U1.Charges.Tree.Branch.phenoInsertQ10 (b : PhysLean.FourTree.Branch (Option ℤ) (Finset ℤ) (Finset ℤ)) (qHd : Option ℤ) (x : ℤ) : PhysLean.FourTree.Branch (Option ℤ) (Finset ℤ) (Finset ℤ)

The branch obtained by taking the new, not pheno-constrained, charges obtained by inserting q10 into all leafs of a branch. This assumes that all existing charges in the branch are already not pheno constrained.

Equations

• One or more equations did not get rendered due to their size.

def FTheory.SU5U1.Charges.Tree.Trunk.phenoInsertQ10 (T : PhysLean.FourTree.Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : ℤ) : PhysLean.FourTree.Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

The trunk obtained by taking the new, not pheno-constrained, charges obtained by inserting q10 into all leafs of a trunk. This assumes that all existing charges in the trunk are already not pheno constrained.

Equations

• One or more equations did not get rendered due to their size.

def FTheory.SU5U1.Charges.Tree.phenoInsertQ10 (T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : ℤ) : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

The tree obtained by taking the new, not pheno-constrained, charges obtained by inserting q10 into all leafs of a tree. This assumes that all existing charges in the tree are already not pheno constrained.

Equations

• One or more equations did not get rendered due to their size.

theorem FTheory.SU5U1.Charges.Tree.mem_phenoInsertQ10_of_mem_allowsTerm (T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (q10 : ℤ) (C : Charges) (h : C ∈ PhysLean.FourTree.uniqueMap4 (insert q10) T) (hC : ¬AllowsTerm (C.1, C.2.1, ∅, {q10}) SuperSymmetry.SU5.PotentialTerm.K2 ∧ ¬AllowsTerm (none, none, C.2.2.1, {q10}) SuperSymmetry.SU5.PotentialTerm.Λ ∧ ¬AllowsTerm (none, none, C.2.2.1, C.2.2.2) SuperSymmetry.SU5.PotentialTerm.W1 ∧ ¬AllowsTerm (none, none, C.2.2.1, C.2.2.2) SuperSymmetry.SU5.PotentialTerm.K1 ∧ ¬AllowsTerm (C.1, none, ∅, C.2.2.2) SuperSymmetry.SU5.PotentialTerm.W2) : C ∈ phenoInsertQ10 T q10

Inserting q5 charges into trees

def FTheory.SU5U1.Charges.Tree.Branch.phenoInsertQ5 (b : PhysLean.FourTree.Branch (Option ℤ) (Finset ℤ) (Finset ℤ)) (qHd : Option ℤ) (x : ℤ) : PhysLean.FourTree.Branch (Option ℤ) (Finset ℤ) (Finset ℤ)

The branch obtained by taking the new, not pheno-constrained, charges obtained by inserting q5 into all leafs of a branch. This assumes that all existing charges in the branch are already not pheno constrained.

Equations

• One or more equations did not get rendered due to their size.

def FTheory.SU5U1.Charges.Tree.Trunk.phenoInsertQ5 (T : PhysLean.FourTree.Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : ℤ) : PhysLean.FourTree.Trunk (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

The trunk obtained by taking the new, not pheno-constrained, charges obtained by inserting q5 into all leafs of a trunk. This assumes that all existing charges in the trunk are already not pheno constrained.

Equations

• One or more equations did not get rendered due to their size.

def FTheory.SU5U1.Charges.Tree.phenoInsertQ5 (T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (x : ℤ) : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)

The tree obtained by taking the new, not pheno-constrained, charges obtained by inserting q5 into all leafs of a tree. This assumes that all existing charges in the tree are already not pheno constrained.

Equations

• One or more equations did not get rendered due to their size.

theorem FTheory.SU5U1.Charges.Tree.mem_phenoInsertQ5_of_mem_allowsTerm (T : PhysLean.FourTree (Option ℤ) (Option ℤ) (Finset ℤ) (Finset ℤ)) (q5 : ℤ) (C : Charges) (h : C ∈ PhysLean.FourTree.uniqueMap3 (insert q5) T) (hC : ¬AllowsTerm (none, C.2.1, {q5}, ∅) SuperSymmetry.SU5.PotentialTerm.β ∧ ¬AllowsTerm (C.1, C.2.1, {q5}, ∅) SuperSymmetry.SU5.PotentialTerm.W4 ∧ ¬AllowsTerm (none, none, {q5}, C.2.2.2) SuperSymmetry.SU5.PotentialTerm.W1 ∧ ¬AllowsTerm (none, none, {q5}, C.2.2.2) SuperSymmetry.SU5.PotentialTerm.K1 ∧ ¬AllowsTerm (none, none, C.2.2.1, C.2.2.2) SuperSymmetry.SU5.PotentialTerm.Λ) : C ∈ phenoInsertQ5 T q5