The MSSM with 3 families and RHNs

We define the system of ACCs for the MSSM with 3 families and RHNs. We define the system of charges for 1-species. We prove some basic lemmas about them.

def MSSMCharges : ACCSystemCharges

The vector space of charges corresponding to the MSSM fermions.

Equations

• MSSMCharges = ACCSystemChargesMk 20

@[simp]

theorem MSSMCharges_numberCharges : MSSMCharges.numberCharges = 20

def MSSMSpecies : ACCSystemCharges

The vector spaces of charges of one species of fermions in the MSSM.

Equations

• MSSMSpecies = ACCSystemChargesMk 3

@[simp]

theorem MSSMSpecies_numberCharges : MSSMSpecies.numberCharges = 3

def MSSMCharges.toSMPlusH : MSSMCharges.Charges ≃ (Fin 18 ⊕ Fin 2 → ℚ)

An equivalence between MSSMCharges.charges and the space of maps (Fin 18 ⊕ Fin 2 → ℚ). The first 18 factors corresponds to the SM fermions, while the last two are the higgsions.

Equations

• MSSMCharges.toSMPlusH = (finSumFinEquiv.arrowCongr (Equiv.refl ℚ)).symm

@[simp]

theorem MSSMCharges.toSMPlusH_symm_apply (a✝ : Fin 18 ⊕ Fin 2 → ℚ) (a✝¹ : Fin (18 + 2)) : MSSMCharges.toSMPlusH.symm a✝ a✝¹ = a✝ (finSumFinEquiv.symm a✝¹)

@[simp]

theorem MSSMCharges.toSMPlusH_apply (a✝ : Fin (18 + 2) → ℚ) (a✝¹ : Fin 18 ⊕ Fin 2) : MSSMCharges.toSMPlusH a✝ a✝¹ = a✝ (finSumFinEquiv a✝¹)

def MSSMCharges.splitSMPlusH : (Fin 18 ⊕ Fin 2 → ℚ) ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ)

An equivalence between Fin 18 ⊕ Fin 2 → ℚ and (Fin 18 → ℚ) × (Fin 2 → ℚ).

Equations

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

@[simp]

theorem MSSMCharges.splitSMPlusH_apply (f : Fin 18 ⊕ Fin 2 → ℚ) : MSSMCharges.splitSMPlusH f = (f ∘ Sum.inl, f ∘ Sum.inr)

@[simp]

theorem MSSMCharges.splitSMPlusH_symm_apply (f : (Fin 18 → ℚ) × (Fin 2 → ℚ)) (a✝ : Fin 18 ⊕ Fin 2) : MSSMCharges.splitSMPlusH.symm f a✝ = Sum.elim f.1 f.2 a✝

def MSSMCharges.toSplitSMPlusH : MSSMCharges.Charges ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ)

An equivalence between MSSMCharges.charges and (Fin 18 → ℚ) × (Fin 2 → ℚ). This splits the charges up into the SM and the additional ones for the MSSM.

Equations

• MSSMCharges.toSplitSMPlusH = MSSMCharges.toSMPlusH.trans MSSMCharges.splitSMPlusH

@[simp]

theorem MSSMCharges.toSplitSMPlusH_apply (a✝ : MSSMCharges.Charges) : MSSMCharges.toSplitSMPlusH a✝ = (MSSMCharges.toSMPlusH a✝ ∘ Sum.inl, MSSMCharges.toSMPlusH a✝ ∘ Sum.inr)

@[simp]

theorem MSSMCharges.toSplitSMPlusH_symm_apply (a✝ : (Fin 18 → ℚ) × (Fin 2 → ℚ)) : MSSMCharges.toSplitSMPlusH.symm a✝ = MSSMCharges.toSMPlusH.symm (MSSMCharges.splitSMPlusH.symm a✝)

def MSSMCharges.toSpeciesMaps' : (Fin 18 → ℚ) ≃ (Fin 6 → Fin 3 → ℚ)

An equivalence between (Fin 18 → ℚ) and (Fin 6 → Fin 3 → ℚ).

Equations

• MSSMCharges.toSpeciesMaps' = ((Equiv.curry (Fin 6) (Fin 3) ℚ).symm.trans (finProdFinEquiv.arrowCongr (Equiv.refl ℚ))).symm

@[simp]

theorem MSSMCharges.toSpeciesMaps'_apply (a✝ : Fin (6 * 3) → ℚ) (a✝¹ : Fin 6) (a✝² : Fin 3) : MSSMCharges.toSpeciesMaps' a✝ a✝¹ a✝² = a✝ (finProdFinEquiv (a✝¹, a✝²))

@[simp]

theorem MSSMCharges.toSpeciesMaps'_symm_apply (a✝ : Fin 6 → Fin 3 → ℚ) (a✝¹ : Fin (6 * 3)) : MSSMCharges.toSpeciesMaps'.symm a✝ a✝¹ = a✝ a✝¹.divNat a✝¹.modNat

def MSSMCharges.toSpecies : MSSMCharges.Charges ≃ (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)

An equivalence between MSSMCharges.charges and (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)). This splits charges up into the SM and additional fermions, and further splits the SM into species.

Equations

• MSSMCharges.toSpecies = MSSMCharges.toSplitSMPlusH.trans (MSSMCharges.toSpeciesMaps'.prodCongr (Equiv.refl (Fin 2 → ℚ)))

@[simp]

theorem MSSMCharges.toSpecies_apply (a✝ : MSSMCharges.Charges) : MSSMCharges.toSpecies a✝ = (MSSMCharges.toSpeciesMaps' (MSSMCharges.toSMPlusH a✝ ∘ Sum.inl), MSSMCharges.toSMPlusH a✝ ∘ Sum.inr)

@[simp]

theorem MSSMCharges.toSpecies_symm_apply (a✝ : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) : MSSMCharges.toSpecies.symm a✝ = MSSMCharges.toSMPlusH.symm (MSSMCharges.splitSMPlusH.symm (Prod.map (⇑MSSMCharges.toSpeciesMaps'.symm) id a✝))

def MSSMCharges.toSMSpecies (i : Fin 6) : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charges

For a given i ∈ Fin 6 the projection of MSSMCharges.charges down to the corresponding SM species of charges.

Equations

• MSSMCharges.toSMSpecies i = { toFun := fun (S : MSSMCharges.Charges) => (Prod.fst ∘ ⇑MSSMCharges.toSpecies) S i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MSSMCharges.toSMSpecies_apply (i : Fin 6) (S : MSSMCharges.Charges) (a✝ : Fin 3) : (MSSMCharges.toSMSpecies i) S a✝ = S (Fin.castAdd 2 (finProdFinEquiv (i, a✝)))

theorem MSSMCharges.toSMSpecies_toSpecies_inv (i : Fin 6) (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) : (MSSMCharges.toSMSpecies i) (MSSMCharges.toSpecies.symm f) = f.1 i

@[reducible, inline]

abbrev MSSMCharges.Q : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charges

The Q charges as a map Fin 3 → ℚ.

Equations

• MSSMCharges.Q = MSSMCharges.toSMSpecies 0

@[reducible, inline]

abbrev MSSMCharges.U : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charges

The U charges as a map Fin 3 → ℚ.

Equations

• MSSMCharges.U = MSSMCharges.toSMSpecies 1

@[reducible, inline]

abbrev MSSMCharges.D : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charges

The D charges as a map Fin 3 → ℚ.

Equations

• MSSMCharges.D = MSSMCharges.toSMSpecies 2

@[reducible, inline]

abbrev MSSMCharges.L : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charges

The L charges as a map Fin 3 → ℚ.

Equations

• MSSMCharges.L = MSSMCharges.toSMSpecies 3

@[reducible, inline]

abbrev MSSMCharges.E : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charges

The E charges as a map Fin 3 → ℚ.

Equations

• MSSMCharges.E = MSSMCharges.toSMSpecies 4

@[reducible, inline]

abbrev MSSMCharges.N : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charges

The N charges as a map Fin 3 → ℚ.

Equations

• MSSMCharges.N = MSSMCharges.toSMSpecies 5

def MSSMCharges.Hd : MSSMCharges.Charges →ₗ[ℚ] ℚ

The charge Hd.

Equations

• MSSMCharges.Hd = { toFun := fun (S : MSSMCharges.Charges) => S ⟨18, MSSMCharges.Hd.proof_1⟩, map_add' := MSSMCharges.Hd.proof_2, map_smul' := MSSMCharges.Hd.proof_3 }

@[simp]

theorem MSSMCharges.Hd_apply (S : MSSMCharges.Charges) : MSSMCharges.Hd S = S ⟨18, MSSMCharges.Hd.proof_1⟩

def MSSMCharges.Hu : MSSMCharges.Charges →ₗ[ℚ] ℚ

The charge Hu.

Equations

• MSSMCharges.Hu = { toFun := fun (S : MSSMCharges.Charges) => S ⟨19, MSSMCharges.Hu.proof_1⟩, map_add' := MSSMCharges.Hu.proof_2, map_smul' := MSSMCharges.Hu.proof_3 }

@[simp]

theorem MSSMCharges.Hu_apply (S : MSSMCharges.Charges) : MSSMCharges.Hu S = S ⟨19, MSSMCharges.Hu.proof_1⟩

theorem MSSMCharges.charges_eq_toSpecies_eq (S T : MSSMCharges.Charges) : S = T ↔ (∀ (i : Fin 6), (MSSMCharges.toSMSpecies i) S = (MSSMCharges.toSMSpecies i) T) ∧ MSSMCharges.Hd S = MSSMCharges.Hd T ∧ MSSMCharges.Hu S = MSSMCharges.Hu T

theorem MSSMCharges.Hd_toSpecies_inv (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) : MSSMCharges.Hd (MSSMCharges.toSpecies.symm f) = f.2 0

theorem MSSMCharges.Hu_toSpecies_inv (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) : MSSMCharges.Hu (MSSMCharges.toSpecies.symm f) = f.2 1

def MSSMACCs.accGrav : MSSMCharges.Charges →ₗ[ℚ] ℚ

The gravitational anomaly equation.

Equations

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

theorem MSSMACCs.accGrav_ext {S T : MSSMCharges.Charges} (hj : ∀ (j : Fin 6), ∑ i : Fin MSSMSpecies.numberCharges, (MSSMCharges.toSMSpecies j) S i = ∑ i : Fin MSSMSpecies.numberCharges, (MSSMCharges.toSMSpecies j) T i) (hd : MSSMCharges.Hd S = MSSMCharges.Hd T) (hu : MSSMCharges.Hu S = MSSMCharges.Hu T) : MSSMACCs.accGrav S = MSSMACCs.accGrav T

Extensionality lemma for accGrav.

def MSSMACCs.accSU2 : MSSMCharges.Charges →ₗ[ℚ] ℚ

The anomaly cancellation condition for SU(2) anomaly.

Equations

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

theorem MSSMACCs.accSU2_ext {S T : MSSMCharges.Charges} (hj : ∀ (j : Fin 6), ∑ i : Fin MSSMSpecies.numberCharges, (MSSMCharges.toSMSpecies j) S i = ∑ i : Fin MSSMSpecies.numberCharges, (MSSMCharges.toSMSpecies j) T i) (hd : MSSMCharges.Hd S = MSSMCharges.Hd T) (hu : MSSMCharges.Hu S = MSSMCharges.Hu T) : MSSMACCs.accSU2 S = MSSMACCs.accSU2 T

Extensionality lemma for accSU2.

def MSSMACCs.accSU3 : MSSMCharges.Charges →ₗ[ℚ] ℚ

The anomaly cancellation condition for SU(3) anomaly.

Equations

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

theorem MSSMACCs.accSU3_ext {S T : MSSMCharges.Charges} (hj : ∀ (j : Fin 6), ∑ i : Fin MSSMSpecies.numberCharges, (MSSMCharges.toSMSpecies j) S i = ∑ i : Fin MSSMSpecies.numberCharges, (MSSMCharges.toSMSpecies j) T i) : MSSMACCs.accSU3 S = MSSMACCs.accSU3 T

Extensionality lemma for accSU3.

def MSSMACCs.accYY : MSSMCharges.Charges →ₗ[ℚ] ℚ

The ACC for Y².

Equations

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

theorem MSSMACCs.accYY_ext {S T : MSSMCharges.Charges} (hj : ∀ (j : Fin 6), ∑ i : Fin MSSMSpecies.numberCharges, (MSSMCharges.toSMSpecies j) S i = ∑ i : Fin MSSMSpecies.numberCharges, (MSSMCharges.toSMSpecies j) T i) (hd : MSSMCharges.Hd S = MSSMCharges.Hd T) (hu : MSSMCharges.Hu S = MSSMCharges.Hu T) : MSSMACCs.accYY S = MSSMACCs.accYY T

Extensionality lemma for accGrav.

def MSSMACCs.quadBiLin : BiLinearSymm MSSMCharges.Charges

The symmetric bilinear function used to define the quadratic ACC.

Equations

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

@[simp]

theorem MSSMACCs.quadBiLin_toFun_apply (S T : MSSMCharges.Charges) : (MSSMACCs.quadBiLin S) T = ∑ x : Fin 3, (S (Fin.castAdd 2 (finProdFinEquiv (0, x))) * T (Fin.castAdd 2 (finProdFinEquiv (0, x))) + -(2 * (S (Fin.castAdd 2 (finProdFinEquiv (1, x))) * T (Fin.castAdd 2 (finProdFinEquiv (1, x))))) + S (Fin.castAdd 2 (finProdFinEquiv (2, x))) * T (Fin.castAdd 2 (finProdFinEquiv (2, x))) + -(S (Fin.castAdd 2 (finProdFinEquiv (3, x))) * T (Fin.castAdd 2 (finProdFinEquiv (3, x)))) + S (Fin.castAdd 2 (finProdFinEquiv (4, x))) * T (Fin.castAdd 2 (finProdFinEquiv (4, x)))) + (-(S ⟨18, MSSMCharges.Hd.proof_1⟩ * T ⟨18, MSSMCharges.Hd.proof_1⟩) + S ⟨19, MSSMCharges.Hu.proof_1⟩ * T ⟨19, MSSMCharges.Hu.proof_1⟩)

def MSSMACCs.accQuad : HomogeneousQuadratic MSSMCharges.Charges

The quadratic ACC.

Equations

• MSSMACCs.accQuad = MSSMACCs.quadBiLin.toHomogeneousQuad

theorem MSSMACCs.accQuad_ext {S T : MSSMCharges.Charges} (h : ∀ (j : Fin 6), ∑ i : Fin MSSMSpecies.numberCharges, ((fun (a : ℚ) => a ^ 2) ∘ (MSSMCharges.toSMSpecies j) S) i = ∑ i : Fin MSSMSpecies.numberCharges, ((fun (a : ℚ) => a ^ 2) ∘ (MSSMCharges.toSMSpecies j) T) i) (hd : MSSMCharges.Hd S = MSSMCharges.Hd T) (hu : MSSMCharges.Hu S = MSSMCharges.Hu T) : MSSMACCs.accQuad S = MSSMACCs.accQuad T

Extensionality lemma for accQuad.

def MSSMACCs.cubeTriLinToFun (S : MSSMCharges.Charges × MSSMCharges.Charges × MSSMCharges.Charges) : ℚ

The function underlying the symmetric trilinear form used to define the cubic ACC.

Equations

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

theorem MSSMACCs.cubeTriLinToFun_map_smul₁ (a : ℚ) (S T R : MSSMCharges.Charges) : MSSMACCs.cubeTriLinToFun (a • S, T, R) = a * MSSMACCs.cubeTriLinToFun (S, T, R)

theorem MSSMACCs.cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) : MSSMACCs.cubeTriLinToFun (S + T, R, L) = MSSMACCs.cubeTriLinToFun (S, R, L) + MSSMACCs.cubeTriLinToFun (T, R, L)

theorem MSSMACCs.cubeTriLinToFun_swap1 (S T R : MSSMCharges.Charges) : MSSMACCs.cubeTriLinToFun (S, T, R) = MSSMACCs.cubeTriLinToFun (T, S, R)

theorem MSSMACCs.cubeTriLinToFun_swap2 (S T R : MSSMCharges.Charges) : MSSMACCs.cubeTriLinToFun (S, T, R) = MSSMACCs.cubeTriLinToFun (S, R, T)

def MSSMACCs.cubeTriLin : TriLinearSymm MSSMCharges.Charges

The symmetric trilinear form used to define the cubic ACC.

Equations

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

@[simp]

theorem MSSMACCs.cubeTriLin_toFun_apply_apply (S S✝ T : MSSMCharges.Charges) : ((MSSMACCs.cubeTriLin S) S✝) T = ∑ i : Fin 3, (6 * (S (Fin.castAdd 2 (finProdFinEquiv (0, i))) * S✝ (Fin.castAdd 2 (finProdFinEquiv (0, i))) * T (Fin.castAdd 2 (finProdFinEquiv (0, i)))) + 3 * (S (Fin.castAdd 2 (finProdFinEquiv (1, i))) * S✝ (Fin.castAdd 2 (finProdFinEquiv (1, i))) * T (Fin.castAdd 2 (finProdFinEquiv (1, i)))) + 3 * (S (Fin.castAdd 2 (finProdFinEquiv (2, i))) * S✝ (Fin.castAdd 2 (finProdFinEquiv (2, i))) * T (Fin.castAdd 2 (finProdFinEquiv (2, i)))) + 2 * (S (Fin.castAdd 2 (finProdFinEquiv (3, i))) * S✝ (Fin.castAdd 2 (finProdFinEquiv (3, i))) * T (Fin.castAdd 2 (finProdFinEquiv (3, i)))) + S (Fin.castAdd 2 (finProdFinEquiv (4, i))) * S✝ (Fin.castAdd 2 (finProdFinEquiv (4, i))) * T (Fin.castAdd 2 (finProdFinEquiv (4, i))) + S (Fin.castAdd 2 (finProdFinEquiv (5, i))) * S✝ (Fin.castAdd 2 (finProdFinEquiv (5, i))) * T (Fin.castAdd 2 (finProdFinEquiv (5, i)))) + (2 * S ⟨18, MSSMCharges.Hd.proof_1⟩ * S✝ ⟨18, MSSMCharges.Hd.proof_1⟩ * T ⟨18, MSSMCharges.Hd.proof_1⟩ + 2 * S ⟨19, MSSMCharges.Hu.proof_1⟩ * S✝ ⟨19, MSSMCharges.Hu.proof_1⟩ * T ⟨19, MSSMCharges.Hu.proof_1⟩)

def MSSMACCs.accCube : HomogeneousCubic MSSMCharges.Charges

The cubic ACC.

Equations

• MSSMACCs.accCube = MSSMACCs.cubeTriLin.toCubic

theorem MSSMACCs.accCube_ext {S T : MSSMCharges.Charges} (h : ∀ (j : Fin 6), ∑ i : Fin MSSMSpecies.numberCharges, ((fun (a : ℚ) => a ^ 3) ∘ (MSSMCharges.toSMSpecies j) S) i = ∑ i : Fin MSSMSpecies.numberCharges, ((fun (a : ℚ) => a ^ 3) ∘ (MSSMCharges.toSMSpecies j) T) i) (hd : MSSMCharges.Hd S = MSSMCharges.Hd T) (hu : MSSMCharges.Hu S = MSSMCharges.Hu T) : MSSMACCs.accCube S = MSSMACCs.accCube T

Extensionality lemma for accCube.

def MSSMACC : ACCSystem

The ACCSystem for the MSSM without RHN.

Equations

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

@[simp]

theorem MSSMACC_quadraticACCs (i : Fin 1) : MSSMACC.quadraticACCs i = match i with | 0 => MSSMACCs.quadBiLin.toHomogeneousQuad

@[simp]

theorem MSSMACC_numberQuadratic : MSSMACC.numberQuadratic = 1

@[simp]

theorem MSSMACC_cubicACC_apply (S : MSSMCharges.Charges) : MSSMACC.cubicACC S = ∑ i : Fin 3, (6 * (S (Fin.castAdd 2 (finProdFinEquiv (0, i))) * S (Fin.castAdd 2 (finProdFinEquiv (0, i))) * S (Fin.castAdd 2 (finProdFinEquiv (0, i)))) + 3 * (S (Fin.castAdd 2 (finProdFinEquiv (1, i))) * S (Fin.castAdd 2 (finProdFinEquiv (1, i))) * S (Fin.castAdd 2 (finProdFinEquiv (1, i)))) + 3 * (S (Fin.castAdd 2 (finProdFinEquiv (2, i))) * S (Fin.castAdd 2 (finProdFinEquiv (2, i))) * S (Fin.castAdd 2 (finProdFinEquiv (2, i)))) + 2 * (S (Fin.castAdd 2 (finProdFinEquiv (3, i))) * S (Fin.castAdd 2 (finProdFinEquiv (3, i))) * S (Fin.castAdd 2 (finProdFinEquiv (3, i)))) + S (Fin.castAdd 2 (finProdFinEquiv (4, i))) * S (Fin.castAdd 2 (finProdFinEquiv (4, i))) * S (Fin.castAdd 2 (finProdFinEquiv (4, i))) + S (Fin.castAdd 2 (finProdFinEquiv (5, i))) * S (Fin.castAdd 2 (finProdFinEquiv (5, i))) * S (Fin.castAdd 2 (finProdFinEquiv (5, i)))) + (2 * S ⟨18, MSSMCharges.Hd.proof_1⟩ * S ⟨18, MSSMCharges.Hd.proof_1⟩ * S ⟨18, MSSMCharges.Hd.proof_1⟩ + 2 * S ⟨19, MSSMCharges.Hu.proof_1⟩ * S ⟨19, MSSMCharges.Hu.proof_1⟩ * S ⟨19, MSSMCharges.Hu.proof_1⟩)

@[simp]

theorem MSSMACC_numberCharges : MSSMACC.numberCharges = 20

@[simp]

theorem MSSMACC_numberLinear : MSSMACC.numberLinear = 4

@[simp]

theorem MSSMACC_linearACCs (i : Fin 4) : MSSMACC.linearACCs i = match i with | 0 => { toFun := fun (S : MSSMCharges.Charges) => ∑ i : Fin 3, (6 * S (Fin.castAdd 2 (finProdFinEquiv (0, i))) + 3 * S (Fin.castAdd 2 (finProdFinEquiv (1, i))) + 3 * S (Fin.castAdd 2 (finProdFinEquiv (2, i))) + 2 * S (Fin.castAdd 2 (finProdFinEquiv (3, i))) + S (Fin.castAdd 2 (finProdFinEquiv (4, i))) + S (Fin.castAdd 2 (finProdFinEquiv (5, i)))) + 2 * (S ⟨18, MSSMCharges.Hd.proof_1⟩ + S ⟨19, MSSMCharges.Hu.proof_1⟩), map_add' := MSSMACCs.accGrav.proof_1, map_smul' := MSSMACCs.accGrav.proof_2 } | 1 => { toFun := fun (S : MSSMCharges.Charges) => ∑ i : Fin 3, (3 * S (Fin.castAdd 2 (finProdFinEquiv (0, i))) + S (Fin.castAdd 2 (finProdFinEquiv (3, i)))) + S ⟨18, MSSMCharges.Hd.proof_1⟩ + S ⟨19, MSSMCharges.Hu.proof_1⟩, map_add' := MSSMACCs.accSU2.proof_1, map_smul' := MSSMACCs.accSU2.proof_2 } | 2 => { toFun := fun (S : MSSMCharges.Charges) => ∑ i : Fin 3, (2 * S (Fin.castAdd 2 (finProdFinEquiv (0, i))) + S (Fin.castAdd 2 (finProdFinEquiv (1, i))) + S (Fin.castAdd 2 (finProdFinEquiv (2, i)))), map_add' := MSSMACCs.accSU3.proof_1, map_smul' := MSSMACCs.accSU3.proof_2 } | 3 => { toFun := fun (S : MSSMCharges.Charges) => ∑ i : Fin 3, (S (Fin.castAdd 2 (finProdFinEquiv (0, i))) + 8 * S (Fin.castAdd 2 (finProdFinEquiv (1, i))) + 2 * S (Fin.castAdd 2 (finProdFinEquiv (2, i))) + 3 * S (Fin.castAdd 2 (finProdFinEquiv (3, i))) + 6 * S (Fin.castAdd 2 (finProdFinEquiv (4, i)))) + 3 * (S ⟨18, MSSMCharges.Hd.proof_1⟩ + S ⟨19, MSSMCharges.Hu.proof_1⟩), map_add' := MSSMACCs.accYY.proof_1, map_smul' := MSSMACCs.accYY.proof_2 }

theorem MSSMACC.quadSol (S : MSSMACC.QuadSols) : MSSMACCs.accQuad S.val = 0

def MSSMACC.AnomalyFreeMk (S : MSSMACC.Charges) (hg : MSSMACCs.accGrav S = 0) (hsu2 : MSSMACCs.accSU2 S = 0) (hsu3 : MSSMACCs.accSU3 S = 0) (hyy : MSSMACCs.accYY S = 0) (hquad : MSSMACCs.accQuad S = 0) (hcube : MSSMACCs.accCube S = 0) : MSSMACC.Sols

A solution from a charge satisfying the ACCs.

Equations

• MSSMACC.AnomalyFreeMk S hg hsu2 hsu3 hyy hquad hcube = { val := S, linearSol := ⋯, quadSol := ⋯, cubicSol := hcube }

theorem MSSMACC.AnomalyFreeMk_val (S : MSSMACC.Charges) (hg : MSSMACCs.accGrav S = 0) (hsu2 : MSSMACCs.accSU2 S = 0) (hsu3 : MSSMACCs.accSU3 S = 0) (hyy : MSSMACCs.accYY S = 0) (hquad : MSSMACCs.accQuad S = 0) (hcube : MSSMACCs.accCube S = 0) : (MSSMACC.AnomalyFreeMk S hg hsu2 hsu3 hyy hquad hcube).val = S

def MSSMACC.AnomalyFreeQuadMk' (S : MSSMACC.LinSols) (hquad : MSSMACCs.accQuad S.val = 0) : MSSMACC.QuadSols

A QuadSol from a LinSol satisfying the quadratic ACC.

Equations

• MSSMACC.AnomalyFreeQuadMk' S hquad = { toLinSols := S, quadSol := ⋯ }

def MSSMACC.AnomalyFreeMk' (S : MSSMACC.LinSols) (hquad : MSSMACCs.accQuad S.val = 0) (hcube : MSSMACCs.accCube S.val = 0) : MSSMACC.Sols

A Sol from a LinSol satisfying the quadratic and cubic ACCs.

Equations

• MSSMACC.AnomalyFreeMk' S hquad hcube = { toLinSols := S, quadSol := ⋯, cubicSol := hcube }

def MSSMACC.AnomalyFreeMk'' (S : MSSMACC.QuadSols) (hcube : MSSMACCs.accCube S.val = 0) : MSSMACC.Sols

A Sol from a QuadSol satisfying the cubic ACCs.

Equations

• MSSMACC.AnomalyFreeMk'' S hcube = { toQuadSols := S, cubicSol := hcube }

theorem MSSMACC.AnomalyFreeMk''_val (S : MSSMACC.QuadSols) (hcube : MSSMACCs.accCube S.val = 0) : (MSSMACC.AnomalyFreeMk'' S hcube).val = S.val

def MSSMACC.dot : BiLinearSymm MSSMCharges.Charges

The dot product on the vector space of charges.

Equations

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

@[simp]

theorem MSSMACC.dot_toFun_apply (S T : MSSMCharges.Charges) : (MSSMACC.dot S) T = ∑ i : Fin 3, (S (Fin.castAdd 2 (finProdFinEquiv (0, i))) * T (Fin.castAdd 2 (finProdFinEquiv (0, i))) + S (Fin.castAdd 2 (finProdFinEquiv (1, i))) * T (Fin.castAdd 2 (finProdFinEquiv (1, i))) + S (Fin.castAdd 2 (finProdFinEquiv (2, i))) * T (Fin.castAdd 2 (finProdFinEquiv (2, i))) + S (Fin.castAdd 2 (finProdFinEquiv (3, i))) * T (Fin.castAdd 2 (finProdFinEquiv (3, i))) + S (Fin.castAdd 2 (finProdFinEquiv (4, i))) * T (Fin.castAdd 2 (finProdFinEquiv (4, i))) + S (Fin.castAdd 2 (finProdFinEquiv (5, i))) * T (Fin.castAdd 2 (finProdFinEquiv (5, i)))) + S ⟨18, MSSMCharges.Hd.proof_1⟩ * T ⟨18, MSSMCharges.Hd.proof_1⟩ + S ⟨19, MSSMCharges.Hu.proof_1⟩ * T ⟨19, MSSMCharges.Hu.proof_1⟩