Anomaly cancellation conditions for the Standard Model with right-handed neutrinos

This directory is related to the anomaly cancellation conditions (ACCs) for the Standard Model with right-handed neutrinos (SMν).

def SMνCharges (n : ℕ) : ACCSystemCharges

The vector space of charges corresponding to the SM fermions with RHN.

Equations

• SMνCharges n = ACCSystemChargesMk (6 * n)

@[simp]

theorem SMνCharges_numberCharges (n : ℕ) : (SMνCharges n).numberCharges = 6 * n

def SMνSpecies (n : ℕ) : ACCSystemCharges

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

Equations

• SMνSpecies n = ACCSystemChargesMk n

@[simp]

theorem SMνSpecies_numberCharges (n : ℕ) : (SMνSpecies n).numberCharges = n

def SMνCharges.toSpeciesEquiv {n : ℕ} : (SMνCharges n).Charges ≃ (Fin 6 → Fin n → ℚ)

An equivalence between (SMνCharges n).charges and (Fin 6 → Fin n → ℚ) splitting the charges into species.

Equations

• SMνCharges.toSpeciesEquiv = ((Equiv.curry (Fin 6) (Fin n) ℚ).symm.trans (finProdFinEquiv.arrowCongr (Equiv.refl ℚ))).symm

@[simp]

theorem SMνCharges.toSpeciesEquiv_apply {n : ℕ} (a✝ : Fin (6 * n) → ℚ) (a✝¹ : Fin 6) (a✝² : Fin n) : toSpeciesEquiv a✝ a✝¹ a✝² = a✝ (finProdFinEquiv (a✝¹, a✝²))

@[simp]

theorem SMνCharges.toSpeciesEquiv_symm_apply {n : ℕ} (a✝ : Fin 6 → Fin n → ℚ) (a✝¹ : Fin (6 * n)) : toSpeciesEquiv.symm a✝ a✝¹ = a✝ a✝¹.divNat a✝¹.modNat

def SMνCharges.toSpecies {n : ℕ} (i : Fin 6) : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges

Given an i ∈ Fin 6, the projection of charges onto a given species.

Equations

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

@[simp]

theorem SMνCharges.toSpecies_apply {n : ℕ} (i : Fin 6) (S : (SMνCharges n).Charges) (a✝ : Fin (SMνSpecies n).numberCharges) : (toSpecies i) S a✝ = S (finProdFinEquiv (i, a✝))

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

theorem SMνCharges.toSMSpecies_toSpecies_inv {n : ℕ} (i : Fin 6) (f : Fin 6 → Fin n → ℚ) : (toSpecies i) (toSpeciesEquiv.symm f) = f i

theorem SMνCharges.toSpecies_one (S : (SMνCharges 1).Charges) (j : Fin 6) : (toSpecies j) S ⟨0, ⋯⟩ = S j

@[reducible, inline]

abbrev SMνCharges.Q {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges

The Q charges as a map Fin n → ℚ.

Equations

• SMνCharges.Q = SMνCharges.toSpecies 0

@[reducible, inline]

abbrev SMνCharges.U {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges

The U charges as a map Fin n → ℚ.

Equations

• SMνCharges.U = SMνCharges.toSpecies 1

@[reducible, inline]

abbrev SMνCharges.D {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges

The D charges as a map Fin n → ℚ.

Equations

• SMνCharges.D = SMνCharges.toSpecies 2

@[reducible, inline]

abbrev SMνCharges.L {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges

The L charges as a map Fin n → ℚ.

Equations

• SMνCharges.L = SMνCharges.toSpecies 3

@[reducible, inline]

abbrev SMνCharges.E {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges

The E charges as a map Fin n → ℚ.

Equations

• SMνCharges.E = SMνCharges.toSpecies 4

@[reducible, inline]

abbrev SMνCharges.N {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges

The N charges as a map Fin n → ℚ.

Equations

• SMνCharges.N = SMνCharges.toSpecies 5

def SMνACCs.accGrav {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] ℚ

The gravitational anomaly equation.

Equations

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

theorem SMνACCs.accGrav_decomp {n : ℕ} (S : (SMνCharges n).Charges) : accGrav S = 6 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q S i + 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U S i + 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D S i + 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L S i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E S i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.N S i

theorem SMνACCs.accGrav_ext {n : ℕ} {S T : (SMνCharges n).Charges} (hj : ∀ (j : Fin 6), ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) S i = ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) T i) : accGrav S = accGrav T

Extensionality lemma for accGrav.

def SMνACCs.accSU2 {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] ℚ

The SU(2) anomaly equation.

Equations

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

theorem SMνACCs.accSU2_decomp {n : ℕ} (S : (SMνCharges n).Charges) : accSU2 S = 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q S i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L S i

theorem SMνACCs.accSU2_ext {n : ℕ} {S T : (SMνCharges n).Charges} (hj : ∀ (j : Fin 6), ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) S i = ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) T i) : accSU2 S = accSU2 T

Extensionality lemma for accSU2.

def SMνACCs.accSU3 {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] ℚ

The SU(3) anomaly equations.

Equations

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

theorem SMνACCs.accSU3_decomp {n : ℕ} (S : (SMνCharges n).Charges) : accSU3 S = 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q S i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U S i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D S i

theorem SMνACCs.accSU3_ext {n : ℕ} {S T : (SMνCharges n).Charges} (hj : ∀ (j : Fin 6), ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) S i = ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) T i) : accSU3 S = accSU3 T

Extensionality lemma for accSU3.

def SMνACCs.accYY {n : ℕ} : (SMνCharges n).Charges →ₗ[ℚ] ℚ

The Y² anomaly equation.

Equations

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

theorem SMνACCs.accYY_decomp {n : ℕ} (S : (SMνCharges n).Charges) : accYY S = ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q S i + 8 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U S i + 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D S i + 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L S i + 6 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E S i

theorem SMνACCs.accYY_ext {n : ℕ} {S T : (SMνCharges n).Charges} (hj : ∀ (j : Fin 6), ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) S i = ∑ i : Fin (SMνSpecies n).numberCharges, (SMνCharges.toSpecies j) T i) : accYY S = accYY T

Extensionality lemma for accYY.

def SMνACCs.quadBiLin {n : ℕ} : BiLinearSymm (SMνCharges n).Charges

The quadratic bilinear map.

Equations

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

@[simp]

theorem SMνACCs.quadBiLin_toFun_apply {n : ℕ} (S T : (SMνCharges 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)))

theorem SMνACCs.quadBiLin_decomp {n : ℕ} (S T : (SMνCharges n).Charges) : (quadBiLin S) T = ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q S i * SMνCharges.Q T i - 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U S i * SMνCharges.U T i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D S i * SMνCharges.D T i - ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L S i * SMνCharges.L T i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E S i * SMνCharges.E T i

def SMνACCs.accQuad {n : ℕ} : HomogeneousQuadratic (SMνCharges n).Charges

The quadratic anomaly cancellation condition.

Equations

• SMνACCs.accQuad = SMνACCs.quadBiLin.toHomogeneousQuad

theorem SMνACCs.accQuad_decomp {n : ℕ} (S : (SMνCharges n).Charges) : accQuad S = ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q S i ^ 2 - 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U S i ^ 2 + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D S i ^ 2 - ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L S i ^ 2 + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E S i ^ 2

theorem SMνACCs.accQuad_ext {n : ℕ} {S T : (SMνCharges n).Charges} (h : ∀ (j : Fin 6), ∑ i : Fin (SMνSpecies n).numberCharges, ((fun (a : ℚ) => a ^ 2) ∘ (SMνCharges.toSpecies j) S) i = ∑ i : Fin (SMνSpecies n).numberCharges, ((fun (a : ℚ) => a ^ 2) ∘ (SMνCharges.toSpecies j) T) i) : accQuad S = accQuad T

Extensionality lemma for accQuad.

def SMνACCs.cubeTriLin {n : ℕ} : TriLinearSymm (SMνCharges n).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 SMνACCs.cubeTriLin_toFun_apply_apply {n : ℕ} (S S✝ T : (SMνCharges 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)) + S (finProdFinEquiv (5, i)) * S✝ (finProdFinEquiv (5, i)) * T (finProdFinEquiv (5, i)))

theorem SMνACCs.cubeTriLin_decomp {n : ℕ} (S T R : (SMνCharges n).Charges) : ((cubeTriLin S) T) R = 6 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q S i * SMνCharges.Q T i * SMνCharges.Q R i + 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U S i * SMνCharges.U T i * SMνCharges.U R i + 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D S i * SMνCharges.D T i * SMνCharges.D R i + 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L S i * SMνCharges.L T i * SMνCharges.L R i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E S i * SMνCharges.E T i * SMνCharges.E R i + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.N S i * SMνCharges.N T i * SMνCharges.N R i

def SMνACCs.accCube {n : ℕ} : HomogeneousCubic (SMνCharges n).Charges

The cubic ACC.

Equations

• SMνACCs.accCube = SMνACCs.cubeTriLin.toCubic

theorem SMνACCs.accCube_decomp {n : ℕ} (S : (SMνCharges n).Charges) : accCube S = 6 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.Q S i ^ 3 + 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.U S i ^ 3 + 3 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.D S i ^ 3 + 2 * ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.L S i ^ 3 + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.E S i ^ 3 + ∑ i : Fin (SMνSpecies n).numberCharges, SMνCharges.N S i ^ 3

theorem SMνACCs.accCube_ext {n : ℕ} {S T : (SMνCharges n).Charges} (h : ∀ (j : Fin 6), ∑ i : Fin (SMνSpecies n).numberCharges, ((fun (a : ℚ) => a ^ 3) ∘ (SMνCharges.toSpecies j) S) i = ∑ i : Fin (SMνSpecies n).numberCharges, ((fun (a : ℚ) => a ^ 3) ∘ (SMνCharges.toSpecies j) T) i) : accCube S = accCube T

Extensionality lemma for accCube.