Anomaly cancellation conditions for n family SM.

We define the ACC system for the Standard Model withn-families and no RHN.

def SMCharges (n : ℕ) : ACCSystemCharges

Associate to each (including RHN) SM fermion a set of charges

Equations

• SMCharges n = ACCSystemChargesMk (5 * n)

@[simp]

theorem SMCharges_numberCharges (n : ℕ) : (SMCharges n).numberCharges = 5 * n

def SMSpecies (n : ℕ) : ACCSystemCharges

The vector space associated with a single species of fermions.

Equations

• SMSpecies n = ACCSystemChargesMk n

@[simp]

theorem SMSpecies_numberCharges (n : ℕ) : (SMSpecies n).numberCharges = n

def SMCharges.toSpeciesEquiv {n : ℕ} : (SMCharges n).Charges ≃ (Fin 5 → Fin n → ℚ)

An equivalence between the set (SMCharges n).charges and the set (Fin 5 → Fin n → ℚ).

Equations

• SMCharges.toSpeciesEquiv = ((Equiv.curry (Fin 5) (Fin n) ℚ).symm.trans (finProdFinEquiv.arrowCongr (Equiv.refl ℚ))).symm

@[simp]

theorem SMCharges.toSpeciesEquiv_apply {n : ℕ} (a✝ : Fin (5 * n) → ℚ) (a✝¹ : Fin 5) (a✝² : Fin n) : toSpeciesEquiv a✝ a✝¹ a✝² = a✝ (finProdFinEquiv (a✝¹, a✝²))

@[simp]

theorem SMCharges.toSpeciesEquiv_symm_apply {n : ℕ} (a✝ : Fin 5 → Fin n → ℚ) (a✝¹ : Fin (5 * n)) : toSpeciesEquiv.symm a✝ a✝¹ = a✝ a✝¹.divNat a✝¹.modNat

def SMCharges.toSpecies {n : ℕ} (i : Fin 5) : (SMCharges n).Charges →ₗ[ℚ] (SMSpecies n).Charges

For a given i ∈ Fin 5, the projection of a charge onto that species.

Equations

• SMCharges.toSpecies i = { toFun := fun (S : (SMCharges n).Charges) => SMCharges.toSpeciesEquiv S i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SMCharges.toSpecies_apply {n : ℕ} (i : Fin 5) (S : (SMCharges n).Charges) (a✝ : Fin (SMSpecies n).numberCharges) : (toSpecies i) S a✝ = S (finProdFinEquiv (i, a✝))

theorem SMCharges.charges_eq_toSpecies_eq {n : ℕ} (S T : (SMCharges n).Charges) : S = T ↔ ∀ (i : Fin 5), (toSpecies i) S = (toSpecies i) T

theorem SMCharges.toSMSpecies_toSpecies_inv {n : ℕ} (i : Fin 5) (f : Fin 5 → Fin n → ℚ) : (toSpecies i) (toSpeciesEquiv.symm f) = f i

@[reducible, inline]

abbrev SMCharges.Q {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] (SMSpecies n).Charges

The Q charges as a map Fin n → ℚ.

Equations

• SMCharges.Q = SMCharges.toSpecies 0

@[reducible, inline]

abbrev SMCharges.U {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] (SMSpecies n).Charges

The U charges as a map Fin n → ℚ.

Equations

• SMCharges.U = SMCharges.toSpecies 1

@[reducible, inline]

abbrev SMCharges.D {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] (SMSpecies n).Charges

The D charges as a map Fin n → ℚ.

Equations

• SMCharges.D = SMCharges.toSpecies 2

@[reducible, inline]

abbrev SMCharges.L {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] (SMSpecies n).Charges

The L charges as a map Fin n → ℚ.

Equations

• SMCharges.L = SMCharges.toSpecies 3

@[reducible, inline]

abbrev SMCharges.E {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] (SMSpecies n).Charges

The E charges as a map Fin n → ℚ.

Equations

• SMCharges.E = SMCharges.toSpecies 4

def SMACCs.accGrav {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] ℚ

The gravitational anomaly equation.

Equations

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

theorem SMACCs.accGrav_ext {n : ℕ} {S T : (SMCharges n).Charges} (hj : ∀ (j : Fin 5), ∑ i : Fin (SMSpecies n).numberCharges, (SMCharges.toSpecies j) S i = ∑ i : Fin (SMSpecies n).numberCharges, (SMCharges.toSpecies j) T i) : accGrav S = accGrav T

Extensionality lemma for accGrav.

def SMACCs.accSU2 {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] ℚ

The SU(2) anomaly equation.

Equations

• SMACCs.accSU2 = { toFun := fun (S : (SMCharges n).Charges) => ∑ i : Fin (SMSpecies n).numberCharges, (3 * SMCharges.Q S i + SMCharges.L S i), map_add' := ⋯, map_smul' := ⋯ }

theorem SMACCs.accSU2_ext {n : ℕ} {S T : (SMCharges n).Charges} (hj : ∀ (j : Fin 5), ∑ i : Fin (SMSpecies n).numberCharges, (SMCharges.toSpecies j) S i = ∑ i : Fin (SMSpecies n).numberCharges, (SMCharges.toSpecies j) T i) : accSU2 S = accSU2 T

Extensionality lemma for accSU2.

def SMACCs.accSU3 {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] ℚ

The SU(3) anomaly equations.

Equations

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

theorem SMACCs.accSU3_ext {n : ℕ} {S T : (SMCharges n).Charges} (hj : ∀ (j : Fin 5), ∑ i : Fin (SMSpecies n).numberCharges, (SMCharges.toSpecies j) S i = ∑ i : Fin (SMSpecies n).numberCharges, (SMCharges.toSpecies j) T i) : accSU3 S = accSU3 T

Extensionality lemma for accSU3.

def SMACCs.accYY {n : ℕ} : (SMCharges n).Charges →ₗ[ℚ] ℚ

The Y² anomaly equation.

Equations

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

theorem SMACCs.accYY_ext {n : ℕ} {S T : (SMCharges n).Charges} (hj : ∀ (j : Fin 5), ∑ i : Fin (SMSpecies n).numberCharges, (SMCharges.toSpecies j) S i = ∑ i : Fin (SMSpecies n).numberCharges, (SMCharges.toSpecies j) T i) : accYY S = accYY T

Extensionality lemma for accYY.

def SMACCs.quadBiLin {n : ℕ} : BiLinearSymm (SMCharges n).Charges

The quadratic bilinear map.

Equations

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

@[simp]

theorem SMACCs.quadBiLin_toFun_apply {n : ℕ} (S T : (SMCharges n).Charges) : (quadBiLin S) T = ∑ x : Fin n, (S (finProdFinEquiv (0, x)) * T (finProdFinEquiv (0, x)) + -(2 * (S (finProdFinEquiv (1, x)) * T (finProdFinEquiv (1, x)))) + S (finProdFinEquiv (2, x)) * T (finProdFinEquiv (2, x)) + -(S (finProdFinEquiv (3, x)) * T (finProdFinEquiv (3, x))) + S (finProdFinEquiv (4, x)) * T (finProdFinEquiv (4, x)))

def SMACCs.accQuad {n : ℕ} : HomogeneousQuadratic (SMCharges n).Charges

The quadratic anomaly cancellation condition.

Equations

• SMACCs.accQuad = SMACCs.quadBiLin.toHomogeneousQuad

theorem SMACCs.accQuad_ext {n : ℕ} {S T : (SMCharges n).Charges} (h : ∀ (j : Fin 5), ∑ i : Fin (SMSpecies n).numberCharges, ((fun (a : ℚ) => a ^ 2) ∘ (SMCharges.toSpecies j) S) i = ∑ i : Fin (SMSpecies n).numberCharges, ((fun (a : ℚ) => a ^ 2) ∘ (SMCharges.toSpecies j) T) i) : accQuad S = accQuad T

Extensionality lemma for accQuad.

def SMACCs.cubeTriLin {n : ℕ} : TriLinearSymm (SMCharges n).Charges

The trilinear function defining the cubic.

Equations

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

@[simp]

theorem SMACCs.cubeTriLin_toFun_apply_apply {n : ℕ} (S S✝ T : (SMCharges n).Charges) : ((cubeTriLin S) S✝) T = ∑ i : Fin n, (6 * (S (finProdFinEquiv (0, i)) * S✝ (finProdFinEquiv (0, i)) * T (finProdFinEquiv (0, i))) + 3 * (S (finProdFinEquiv (1, i)) * S✝ (finProdFinEquiv (1, i)) * T (finProdFinEquiv (1, i))) + 3 * (S (finProdFinEquiv (2, i)) * S✝ (finProdFinEquiv (2, i)) * T (finProdFinEquiv (2, i))) + 2 * (S (finProdFinEquiv (3, i)) * S✝ (finProdFinEquiv (3, i)) * T (finProdFinEquiv (3, i))) + S (finProdFinEquiv (4, i)) * S✝ (finProdFinEquiv (4, i)) * T (finProdFinEquiv (4, i)))

def SMACCs.accCube {n : ℕ} : HomogeneousCubic (SMCharges n).Charges

The cubic acc.

Equations

• SMACCs.accCube = SMACCs.cubeTriLin.toCubic

theorem SMACCs.accCube_ext {n : ℕ} {S T : (SMCharges n).Charges} (h : ∀ (j : Fin 5), ∑ i : Fin (SMSpecies n).numberCharges, ((fun (a : ℚ) => a ^ 3) ∘ (SMCharges.toSpecies j) S) i = ∑ i : Fin (SMSpecies n).numberCharges, ((fun (a : ℚ) => a ^ 3) ∘ (SMCharges.toSpecies j) T) i) : accCube S = accCube T

Extensionality lemma for accCube.