Imports
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.QFT.AnomalyCancellation.BasicAnomaly 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ν).
@[expose] public sectionThe vector space of charges corresponding to the SM fermions with RHN.
@[simps!]
def SMνCharges (n : ℕ) : ACCSystemCharges := ⟨6 * n⟩The vector spaces of charges of one species of fermions in the SM.
@[simps!]
def SMνSpecies (n : ℕ) : ACCSystemCharges := ⟨n⟩lemma sum_one [AddCommMonoid M] (f : Fin (SMνSpecies 1).numberCharges → M) :
∑ i, f i = f ⟨0, n:ℕM:Type ?u.4inst✝:AddCommMonoid Mf:Fin (SMνSpecies 1).numberCharges → M⊢ 0 < (SMνSpecies 1).numberCharges All goals completed! 🐙⟩ := M:Type u_1inst✝:AddCommMonoid Mf:Fin (SMνSpecies 1).numberCharges → M⊢ ∑ i, f i = f ⟨0, ⋯⟩
M:Type u_1inst✝:AddCommMonoid Mf:Fin (SMνSpecies 1).numberCharges → M⊢ ∑ i, f i = f ⟨0, ⋯⟩
M:Type u_1inst✝:AddCommMonoid Mf:Fin (SMνSpecies 1).numberCharges → M⊢ f 0 = f ⟨0, ⋯⟩
All goals completed! 🐙
An equivalence between (SMνCharges n).charges and (Fin 6 → Fin n → ℚ)
splitting the charges into species.
@[simps!]
def toSpeciesEquiv : (SMνCharges n).Charges ≃ (Fin 6 → Fin n → ℚ) :=
((Equiv.curry _ _ _).symm.trans ((@finProdFinEquiv 6 n).arrowCongr (Equiv.refl ℚ))).symm
Given an i ∈ Fin 6, the projection of charges onto a given species.
@[simps!]
def toSpecies (i : Fin 6) : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
toFun S := toSpeciesEquiv S i
map_add' _ _ := rfl
map_smul' _ _ := rfllemma charges_eq_toSpecies_eq (S T : (SMνCharges n).Charges) :
S = T ↔ ∀ i, toSpecies i S = toSpecies i T := n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ S = T ↔ ∀ (i : Fin 6), (toSpecies i) S = (toSpecies i) T
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesh:S = T⊢ ∀ (i : Fin 6), (toSpecies i) S = (toSpecies i) Tn:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesh:∀ (i : Fin 6), (toSpecies i) S = (toSpecies i) T⊢ S = T
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesh:S = T⊢ ∀ (i : Fin 6), (toSpecies i) S = (toSpecies i) T All goals completed! 🐙
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesh:∀ (i : Fin 6), (toSpecies i) S = (toSpecies i) T⊢ S = T n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesh:∀ (i : Fin 6), (toSpecies i) S = (toSpecies i) T⊢ toSpeciesEquiv S = toSpeciesEquiv T
All goals completed! 🐙lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f : Fin 6 → Fin n → ℚ) :
(toSpecies i) (toSpeciesEquiv.symm f) = f i := n:ℕi:Fin 6f:Fin 6 → Fin n → ℚ⊢ (toSpecies i) (toSpeciesEquiv.symm f) = f i
n:ℕi:Fin 6f:Fin 6 → Fin n → ℚ⊢ (⇑toSpeciesEquiv ∘ ⇑toSpeciesEquiv.symm) f i = f i
All goals completed! 🐙lemma toSpecies_one (S : (SMνCharges 1).Charges) (j : Fin 6) :
toSpecies j S ⟨0, zero_lt_succ 0⟩ = S j := S:(SMνCharges 1).Chargesj:Fin 6⊢ (toSpecies j) S ⟨0, ⋯⟩ = S j
match j with
S:(SMνCharges 1).Chargesj:Fin 6⊢ (toSpecies 0) S ⟨0, ⋯⟩ = S 0 All goals completed! 🐙
S:(SMνCharges 1).Chargesj:Fin 6⊢ (toSpecies 1) S ⟨0, ⋯⟩ = S 1 All goals completed! 🐙
S:(SMνCharges 1).Chargesj:Fin 6⊢ (toSpecies 2) S ⟨0, ⋯⟩ = S 2 All goals completed! 🐙
S:(SMνCharges 1).Chargesj:Fin 6⊢ (toSpecies 3) S ⟨0, ⋯⟩ = S 3 All goals completed! 🐙
S:(SMνCharges 1).Chargesj:Fin 6⊢ (toSpecies 4) S ⟨0, ⋯⟩ = S 4 All goals completed! 🐙
S:(SMνCharges 1).Chargesj:Fin 6⊢ (toSpecies 5) S ⟨0, ⋯⟩ = S 5 All goals completed! 🐙
The Q charges as a map Fin n → ℚ.
abbrev Q := @toSpecies n 0
The U charges as a map Fin n → ℚ.
abbrev U := @toSpecies n 1
The D charges as a map Fin n → ℚ.
abbrev D := @toSpecies n 2
The L charges as a map Fin n → ℚ.
abbrev L := @toSpecies n 3
The E charges as a map Fin n → ℚ.
abbrev E := @toSpecies n 4
The N charges as a map Fin n → ℚ.
abbrev N := @toSpecies n 5The gravitational anomaly equation.
n:ℕa:ℚS:(SMνCharges n).Charges⊢ 6 * (a * ∑ i, toSpeciesEquiv S 0 i) + 3 * (a * ∑ i, toSpeciesEquiv S 1 i) + 3 * (a * ∑ i, toSpeciesEquiv S 2 i) +
2 * (a * ∑ i, toSpeciesEquiv S 3 i) +
a * ∑ i, toSpeciesEquiv S 4 i +
a * ∑ i, toSpeciesEquiv S 5 i =
a *
(6 * ∑ i, toSpeciesEquiv S 0 i + 3 * ∑ i, toSpeciesEquiv S 1 i + 3 * ∑ i, toSpeciesEquiv S 2 i +
2 * ∑ i, toSpeciesEquiv S 3 i +
∑ x, toSpeciesEquiv S 4 x +
∑ x, toSpeciesEquiv S 5 x)
-- rw [show Rat.cast a = a from rfl]
All goals completed! 🐙All goals completed! 🐙
Extensionality lemma for accGrav.
All goals completed! 🐙
The SU(2) anomaly equation.
n:ℕa:ℚS:(SMνCharges n).Charges⊢ 3 * (a * ∑ i, toSpeciesEquiv S 0 i) + a * ∑ i, toSpeciesEquiv S 3 i =
a * (3 * ∑ i, toSpeciesEquiv S 0 i + ∑ x, toSpeciesEquiv S 3 x)
-- rw [show Rat.cast a = a from rfl]
All goals completed! 🐙All goals completed! 🐙
Extensionality lemma for accSU2.
All goals completed! 🐙
The SU(3) anomaly equations.
n:ℕa:ℚS:(SMνCharges n).Charges⊢ 2 * (a * ∑ i, toSpeciesEquiv S 0 i) + a * ∑ i, toSpeciesEquiv S 1 i + a * ∑ i, toSpeciesEquiv S 2 i =
a * (2 * ∑ i, toSpeciesEquiv S 0 i + ∑ x, toSpeciesEquiv S 1 x + ∑ x, toSpeciesEquiv S 2 x)
-- rw [show Rat.cast a = a from rfl]
All goals completed! 🐙All goals completed! 🐙
Extensionality lemma for accSU3.
All goals completed! 🐙
The Y² anomaly equation.
n:ℕa:ℚS:(SMνCharges n).Charges⊢ a * ∑ i, toSpeciesEquiv S 0 i + 8 * (a * ∑ i, toSpeciesEquiv S 1 i) + 2 * (a * ∑ i, toSpeciesEquiv S 2 i) +
3 * (a * ∑ i, toSpeciesEquiv S 3 i) +
6 * (a * ∑ i, toSpeciesEquiv S 4 i) =
a *
(∑ x, toSpeciesEquiv S 0 x + 8 * ∑ i, toSpeciesEquiv S 1 i + 2 * ∑ i, toSpeciesEquiv S 2 i +
3 * ∑ i, toSpeciesEquiv S 3 i +
6 * ∑ i, toSpeciesEquiv S 4 i)
-- rw [show Rat.cast a = a from rfl]
All goals completed! 🐙All goals completed! 🐙
Extensionality lemma for accYY.
All goals completed! 🐙The quadratic bilinear map.
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Chargesi:Fin (SMνSpecies n).numberCharges⊢ (Q S + Q T) i * Q R i + -2 * ((U S + U T) i * U R i) + (D S + D T) i * D R i + -1 * ((L S + L T) i * L R i) +
(E S + E T) i * E R i =
Q S i * Q R i + -2 * (U S i * U R i) + D S i * D R i + -1 * (L S i * L R i) + E S i * E R i +
(Q T i * Q R i + -2 * (U T i * U R i) + D T i * D R i + -1 * (L T i * L R i) + E T i * E R i)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).Chargesi:Fin (SMνSpecies n).numberCharges⊢ (toSpeciesEquiv S 0 i + toSpeciesEquiv T 0 i) * toSpeciesEquiv R 0 i +
-(2 * ((toSpeciesEquiv S 1 i + toSpeciesEquiv T 1 i) * toSpeciesEquiv R 1 i)) +
(toSpeciesEquiv S 2 i + toSpeciesEquiv T 2 i) * toSpeciesEquiv R 2 i +
-((toSpeciesEquiv S 3 i + toSpeciesEquiv T 3 i) * toSpeciesEquiv R 3 i) +
(toSpeciesEquiv S 4 i + toSpeciesEquiv T 4 i) * toSpeciesEquiv R 4 i =
toSpeciesEquiv S 0 i * toSpeciesEquiv R 0 i + -(2 * (toSpeciesEquiv S 1 i * toSpeciesEquiv R 1 i)) +
toSpeciesEquiv S 2 i * toSpeciesEquiv R 2 i +
-(toSpeciesEquiv S 3 i * toSpeciesEquiv R 3 i) +
toSpeciesEquiv S 4 i * toSpeciesEquiv R 4 i +
(toSpeciesEquiv T 0 i * toSpeciesEquiv R 0 i + -(2 * (toSpeciesEquiv T 1 i * toSpeciesEquiv R 1 i)) +
toSpeciesEquiv T 2 i * toSpeciesEquiv R 2 i +
-(toSpeciesEquiv T 3 i * toSpeciesEquiv R 3 i) +
toSpeciesEquiv T 4 i * toSpeciesEquiv R 4 i)
All goals completed! 🐙)
(n:ℕ⊢ ∀ (S T : (SMνCharges n).Charges),
∑ i,
(Q (S, T).1 i * Q (S, T).2 i + -2 * (U (S, T).1 i * U (S, T).2 i) + D (S, T).1 i * D (S, T).2 i +
-1 * (L (S, T).1 i * L (S, T).2 i) +
E (S, T).1 i * E (S, T).2 i) =
∑ i,
(Q (T, S).1 i * Q (T, S).2 i + -2 * (U (T, S).1 i * U (T, S).2 i) + D (T, S).1 i * D (T, S).2 i +
-1 * (L (T, S).1 i * L (T, S).2 i) +
E (T, S).1 i * E (T, S).2 i)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ ∑ i,
(Q (S, T).1 i * Q (S, T).2 i + -2 * (U (S, T).1 i * U (S, T).2 i) + D (S, T).1 i * D (S, T).2 i +
-1 * (L (S, T).1 i * L (S, T).2 i) +
E (S, T).1 i * E (S, T).2 i) =
∑ i,
(Q (T, S).1 i * Q (T, S).2 i + -2 * (U (T, S).1 i * U (T, S).2 i) + D (T, S).1 i * D (T, S).2 i +
-1 * (L (T, S).1 i * L (T, S).2 i) +
E (T, S).1 i * E (T, S).2 i)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ ∑ x,
(toSpeciesEquiv S 0 x * toSpeciesEquiv T 0 x + -(2 * (toSpeciesEquiv S 1 x * toSpeciesEquiv T 1 x)) +
toSpeciesEquiv S 2 x * toSpeciesEquiv T 2 x +
-(toSpeciesEquiv S 3 x * toSpeciesEquiv T 3 x) +
toSpeciesEquiv S 4 x * toSpeciesEquiv T 4 x) =
∑ x,
(toSpeciesEquiv T 0 x * toSpeciesEquiv S 0 x + -(2 * (toSpeciesEquiv T 1 x * toSpeciesEquiv S 1 x)) +
toSpeciesEquiv T 2 x * toSpeciesEquiv S 2 x +
-(toSpeciesEquiv T 3 x * toSpeciesEquiv S 3 x) +
toSpeciesEquiv T 4 x * toSpeciesEquiv S 4 x)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesi:Fin (SMνSpecies n).numberCharges⊢ toSpeciesEquiv S 0 i * toSpeciesEquiv T 0 i + -(2 * (toSpeciesEquiv S 1 i * toSpeciesEquiv T 1 i)) +
toSpeciesEquiv S 2 i * toSpeciesEquiv T 2 i +
-(toSpeciesEquiv S 3 i * toSpeciesEquiv T 3 i) +
toSpeciesEquiv S 4 i * toSpeciesEquiv T 4 i =
toSpeciesEquiv T 0 i * toSpeciesEquiv S 0 i + -(2 * (toSpeciesEquiv T 1 i * toSpeciesEquiv S 1 i)) +
toSpeciesEquiv T 2 i * toSpeciesEquiv S 2 i +
-(toSpeciesEquiv T 3 i * toSpeciesEquiv S 3 i) +
toSpeciesEquiv T 4 i * toSpeciesEquiv S 4 i
All goals completed! 🐙)n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ ∑ x, Q (S, T).1 x * Q (S, T).2 x + -2 * ∑ i, U (S, T).1 i * U (S, T).2 i + ∑ x, D (S, T).1 x * D (S, T).2 x +
-1 * ∑ i, L (S, T).1 i * L (S, T).2 i +
∑ x, E (S, T).1 x * E (S, T).2 x =
∑ i, Q S i * Q T i - 2 * ∑ i, U S i * U T i + ∑ i, D S i * D T i - ∑ i, L S i * L T i + ∑ i, E S i * E T i
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Charges⊢ ∑ x, toSpeciesEquiv S 0 x * toSpeciesEquiv T 0 x + -(2 * ∑ x, toSpeciesEquiv S 1 x * toSpeciesEquiv T 1 x) +
∑ x, toSpeciesEquiv S 2 x * toSpeciesEquiv T 2 x +
-∑ x, toSpeciesEquiv S 3 x * toSpeciesEquiv T 3 x =
∑ x, toSpeciesEquiv S 0 x * toSpeciesEquiv T 0 x - 2 * ∑ x, toSpeciesEquiv S 1 x * toSpeciesEquiv T 1 x +
∑ x, toSpeciesEquiv S 2 x * toSpeciesEquiv T 2 x -
∑ x, toSpeciesEquiv S 3 x * toSpeciesEquiv T 3 x
All goals completed! 🐙The quadratic anomaly cancellation condition.
@[simp]
def accQuad : HomogeneousQuadratic (SMνCharges n).Charges :=
(@quadBiLin n).toHomogeneousQuadn:ℕS:(SMνCharges n).Charges⊢ ∑ i, Q S i * Q S i - 2 * ∑ i, U S i * U S i + ∑ i, D S i * D S i - ∑ i, L S i * L S i + ∑ i, E S i * E S i =
∑ i, Q S i ^ 2 - 2 * ∑ i, U S i ^ 2 + ∑ i, D S i ^ 2 - ∑ i, L S i ^ 2 + ∑ i, E S i ^ 2
All goals completed! 🐙
Extensionality lemma for accQuad.
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesh:∀ (j : Fin 6), ∑ i, ((fun a => a ^ 2) ∘ (toSpecies j) S) i = ∑ i, ((fun a => a ^ 2) ∘ (toSpecies j) T) i⊢ ∑ i, Q S i ^ 2 - 2 * ∑ i, U S i ^ 2 + ∑ i, D S i ^ 2 - ∑ i, L S i ^ 2 + ∑ i, E S i ^ 2 =
∑ i, Q T i ^ 2 - 2 * ∑ i, U T i ^ 2 + ∑ i, D T i ^ 2 - ∑ i, L T i ^ 2 + ∑ i, E T i ^ 2
All goals completed! 🐙The symmetric trilinear form used to define the cubic acc.
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).ChargesL:(SMνCharges n).Chargesi:Fin (SMνSpecies n).numberCharges⊢ 6 * ((Q S + Q T) i * Q R i * Q L i) + 3 * ((U S + U T) i * U R i * U L i) + 3 * ((D S + D T) i * D R i * D L i) +
2 * ((SMνCharges.L S + SMνCharges.L T) i * SMνCharges.L R i * SMνCharges.L L i) +
(E S + E T) i * E R i * E L i +
(N S + N T) i * N R i * N L i =
6 * (Q S i * Q R i * Q L i) + 3 * (U S i * U R i * U L i) + 3 * (D S i * D R i * D L i) +
2 * (SMνCharges.L S i * SMνCharges.L R i * SMνCharges.L L i) +
E S i * E R i * E L i +
N S i * N R i * N L i +
(6 * (Q T i * Q R i * Q L i) + 3 * (U T i * U R i * U L i) + 3 * (D T i * D R i * D L i) +
2 * (SMνCharges.L T i * SMνCharges.L R i * SMνCharges.L L i) +
E T i * E R i * E L i +
N T i * N R i * N L i)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesR:(SMνCharges n).ChargesL:(SMνCharges n).Chargesi:Fin (SMνSpecies n).numberCharges⊢ 6 * ((toSpeciesEquiv S 0 i + toSpeciesEquiv T 0 i) * toSpeciesEquiv R 0 i * toSpeciesEquiv L 0 i) +
3 * ((toSpeciesEquiv S 1 i + toSpeciesEquiv T 1 i) * toSpeciesEquiv R 1 i * toSpeciesEquiv L 1 i) +
3 * ((toSpeciesEquiv S 2 i + toSpeciesEquiv T 2 i) * toSpeciesEquiv R 2 i * toSpeciesEquiv L 2 i) +
2 * ((toSpeciesEquiv S 3 i + toSpeciesEquiv T 3 i) * toSpeciesEquiv R 3 i * toSpeciesEquiv L 3 i) +
(toSpeciesEquiv S 4 i + toSpeciesEquiv T 4 i) * toSpeciesEquiv R 4 i * toSpeciesEquiv L 4 i +
(toSpeciesEquiv S 5 i + toSpeciesEquiv T 5 i) * toSpeciesEquiv R 5 i * toSpeciesEquiv L 5 i =
6 * (toSpeciesEquiv S 0 i * toSpeciesEquiv R 0 i * toSpeciesEquiv L 0 i) +
3 * (toSpeciesEquiv S 1 i * toSpeciesEquiv R 1 i * toSpeciesEquiv L 1 i) +
3 * (toSpeciesEquiv S 2 i * toSpeciesEquiv R 2 i * toSpeciesEquiv L 2 i) +
2 * (toSpeciesEquiv S 3 i * toSpeciesEquiv R 3 i * toSpeciesEquiv L 3 i) +
toSpeciesEquiv S 4 i * toSpeciesEquiv R 4 i * toSpeciesEquiv L 4 i +
toSpeciesEquiv S 5 i * toSpeciesEquiv R 5 i * toSpeciesEquiv L 5 i +
(6 * (toSpeciesEquiv T 0 i * toSpeciesEquiv R 0 i * toSpeciesEquiv L 0 i) +
3 * (toSpeciesEquiv T 1 i * toSpeciesEquiv R 1 i * toSpeciesEquiv L 1 i) +
3 * (toSpeciesEquiv T 2 i * toSpeciesEquiv R 2 i * toSpeciesEquiv L 2 i) +
2 * (toSpeciesEquiv T 3 i * toSpeciesEquiv R 3 i * toSpeciesEquiv L 3 i) +
toSpeciesEquiv T 4 i * toSpeciesEquiv R 4 i * toSpeciesEquiv L 4 i +
toSpeciesEquiv T 5 i * toSpeciesEquiv R 5 i * toSpeciesEquiv L 5 i)
All goals completed! 🐙)
(n:ℕ⊢ ∀ (S T L : (SMνCharges n).Charges),
∑ i,
(6 * (Q (S, T, L).1 i * Q (S, T, L).2.1 i * Q (S, T, L).2.2 i) +
3 * (U (S, T, L).1 i * U (S, T, L).2.1 i * U (S, T, L).2.2 i) +
3 * (D (S, T, L).1 i * D (S, T, L).2.1 i * D (S, T, L).2.2 i) +
2 * (SMνCharges.L (S, T, L).1 i * SMνCharges.L (S, T, L).2.1 i * SMνCharges.L (S, T, L).2.2 i) +
E (S, T, L).1 i * E (S, T, L).2.1 i * E (S, T, L).2.2 i +
N (S, T, L).1 i * N (S, T, L).2.1 i * N (S, T, L).2.2 i) =
∑ i,
(6 * (Q (T, S, L).1 i * Q (T, S, L).2.1 i * Q (T, S, L).2.2 i) +
3 * (U (T, S, L).1 i * U (T, S, L).2.1 i * U (T, S, L).2.2 i) +
3 * (D (T, S, L).1 i * D (T, S, L).2.1 i * D (T, S, L).2.2 i) +
2 * (SMνCharges.L (T, S, L).1 i * SMνCharges.L (T, S, L).2.1 i * SMνCharges.L (T, S, L).2.2 i) +
E (T, S, L).1 i * E (T, S, L).2.1 i * E (T, S, L).2.2 i +
N (T, S, L).1 i * N (T, S, L).2.1 i * N (T, S, L).2.2 i)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Charges⊢ ∑ i,
(6 * (Q (S, T, L).1 i * Q (S, T, L).2.1 i * Q (S, T, L).2.2 i) +
3 * (U (S, T, L).1 i * U (S, T, L).2.1 i * U (S, T, L).2.2 i) +
3 * (D (S, T, L).1 i * D (S, T, L).2.1 i * D (S, T, L).2.2 i) +
2 * (SMνCharges.L (S, T, L).1 i * SMνCharges.L (S, T, L).2.1 i * SMνCharges.L (S, T, L).2.2 i) +
E (S, T, L).1 i * E (S, T, L).2.1 i * E (S, T, L).2.2 i +
N (S, T, L).1 i * N (S, T, L).2.1 i * N (S, T, L).2.2 i) =
∑ i,
(6 * (Q (T, S, L).1 i * Q (T, S, L).2.1 i * Q (T, S, L).2.2 i) +
3 * (U (T, S, L).1 i * U (T, S, L).2.1 i * U (T, S, L).2.2 i) +
3 * (D (T, S, L).1 i * D (T, S, L).2.1 i * D (T, S, L).2.2 i) +
2 * (SMνCharges.L (T, S, L).1 i * SMνCharges.L (T, S, L).2.1 i * SMνCharges.L (T, S, L).2.2 i) +
E (T, S, L).1 i * E (T, S, L).2.1 i * E (T, S, L).2.2 i +
N (T, S, L).1 i * N (T, S, L).2.1 i * N (T, S, L).2.2 i)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Charges⊢ ∑ x,
(6 * (toSpeciesEquiv S 0 x * toSpeciesEquiv T 0 x * toSpeciesEquiv L 0 x) +
3 * (toSpeciesEquiv S 1 x * toSpeciesEquiv T 1 x * toSpeciesEquiv L 1 x) +
3 * (toSpeciesEquiv S 2 x * toSpeciesEquiv T 2 x * toSpeciesEquiv L 2 x) +
2 * (toSpeciesEquiv S 3 x * toSpeciesEquiv T 3 x * toSpeciesEquiv L 3 x) +
toSpeciesEquiv S 4 x * toSpeciesEquiv T 4 x * toSpeciesEquiv L 4 x +
toSpeciesEquiv S 5 x * toSpeciesEquiv T 5 x * toSpeciesEquiv L 5 x) =
∑ x,
(6 * (toSpeciesEquiv T 0 x * toSpeciesEquiv S 0 x * toSpeciesEquiv L 0 x) +
3 * (toSpeciesEquiv T 1 x * toSpeciesEquiv S 1 x * toSpeciesEquiv L 1 x) +
3 * (toSpeciesEquiv T 2 x * toSpeciesEquiv S 2 x * toSpeciesEquiv L 2 x) +
2 * (toSpeciesEquiv T 3 x * toSpeciesEquiv S 3 x * toSpeciesEquiv L 3 x) +
toSpeciesEquiv T 4 x * toSpeciesEquiv S 4 x * toSpeciesEquiv L 4 x +
toSpeciesEquiv T 5 x * toSpeciesEquiv S 5 x * toSpeciesEquiv L 5 x)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesi:Fin (SMνSpecies n).numberCharges⊢ 6 * (toSpeciesEquiv S 0 i * toSpeciesEquiv T 0 i * toSpeciesEquiv L 0 i) +
3 * (toSpeciesEquiv S 1 i * toSpeciesEquiv T 1 i * toSpeciesEquiv L 1 i) +
3 * (toSpeciesEquiv S 2 i * toSpeciesEquiv T 2 i * toSpeciesEquiv L 2 i) +
2 * (toSpeciesEquiv S 3 i * toSpeciesEquiv T 3 i * toSpeciesEquiv L 3 i) +
toSpeciesEquiv S 4 i * toSpeciesEquiv T 4 i * toSpeciesEquiv L 4 i +
toSpeciesEquiv S 5 i * toSpeciesEquiv T 5 i * toSpeciesEquiv L 5 i =
6 * (toSpeciesEquiv T 0 i * toSpeciesEquiv S 0 i * toSpeciesEquiv L 0 i) +
3 * (toSpeciesEquiv T 1 i * toSpeciesEquiv S 1 i * toSpeciesEquiv L 1 i) +
3 * (toSpeciesEquiv T 2 i * toSpeciesEquiv S 2 i * toSpeciesEquiv L 2 i) +
2 * (toSpeciesEquiv T 3 i * toSpeciesEquiv S 3 i * toSpeciesEquiv L 3 i) +
toSpeciesEquiv T 4 i * toSpeciesEquiv S 4 i * toSpeciesEquiv L 4 i +
toSpeciesEquiv T 5 i * toSpeciesEquiv S 5 i * toSpeciesEquiv L 5 i
All goals completed! 🐙)
(n:ℕ⊢ ∀ (S T L : (SMνCharges n).Charges),
∑ i,
(6 * (Q (S, T, L).1 i * Q (S, T, L).2.1 i * Q (S, T, L).2.2 i) +
3 * (U (S, T, L).1 i * U (S, T, L).2.1 i * U (S, T, L).2.2 i) +
3 * (D (S, T, L).1 i * D (S, T, L).2.1 i * D (S, T, L).2.2 i) +
2 * (SMνCharges.L (S, T, L).1 i * SMνCharges.L (S, T, L).2.1 i * SMνCharges.L (S, T, L).2.2 i) +
E (S, T, L).1 i * E (S, T, L).2.1 i * E (S, T, L).2.2 i +
N (S, T, L).1 i * N (S, T, L).2.1 i * N (S, T, L).2.2 i) =
∑ i,
(6 * (Q (S, L, T).1 i * Q (S, L, T).2.1 i * Q (S, L, T).2.2 i) +
3 * (U (S, L, T).1 i * U (S, L, T).2.1 i * U (S, L, T).2.2 i) +
3 * (D (S, L, T).1 i * D (S, L, T).2.1 i * D (S, L, T).2.2 i) +
2 * (SMνCharges.L (S, L, T).1 i * SMνCharges.L (S, L, T).2.1 i * SMνCharges.L (S, L, T).2.2 i) +
E (S, L, T).1 i * E (S, L, T).2.1 i * E (S, L, T).2.2 i +
N (S, L, T).1 i * N (S, L, T).2.1 i * N (S, L, T).2.2 i)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Charges⊢ ∑ i,
(6 * (Q (S, T, L).1 i * Q (S, T, L).2.1 i * Q (S, T, L).2.2 i) +
3 * (U (S, T, L).1 i * U (S, T, L).2.1 i * U (S, T, L).2.2 i) +
3 * (D (S, T, L).1 i * D (S, T, L).2.1 i * D (S, T, L).2.2 i) +
2 * (SMνCharges.L (S, T, L).1 i * SMνCharges.L (S, T, L).2.1 i * SMνCharges.L (S, T, L).2.2 i) +
E (S, T, L).1 i * E (S, T, L).2.1 i * E (S, T, L).2.2 i +
N (S, T, L).1 i * N (S, T, L).2.1 i * N (S, T, L).2.2 i) =
∑ i,
(6 * (Q (S, L, T).1 i * Q (S, L, T).2.1 i * Q (S, L, T).2.2 i) +
3 * (U (S, L, T).1 i * U (S, L, T).2.1 i * U (S, L, T).2.2 i) +
3 * (D (S, L, T).1 i * D (S, L, T).2.1 i * D (S, L, T).2.2 i) +
2 * (SMνCharges.L (S, L, T).1 i * SMνCharges.L (S, L, T).2.1 i * SMνCharges.L (S, L, T).2.2 i) +
E (S, L, T).1 i * E (S, L, T).2.1 i * E (S, L, T).2.2 i +
N (S, L, T).1 i * N (S, L, T).2.1 i * N (S, L, T).2.2 i)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Charges⊢ ∑ x,
(6 * (toSpeciesEquiv S 0 x * toSpeciesEquiv T 0 x * toSpeciesEquiv L 0 x) +
3 * (toSpeciesEquiv S 1 x * toSpeciesEquiv T 1 x * toSpeciesEquiv L 1 x) +
3 * (toSpeciesEquiv S 2 x * toSpeciesEquiv T 2 x * toSpeciesEquiv L 2 x) +
2 * (toSpeciesEquiv S 3 x * toSpeciesEquiv T 3 x * toSpeciesEquiv L 3 x) +
toSpeciesEquiv S 4 x * toSpeciesEquiv T 4 x * toSpeciesEquiv L 4 x +
toSpeciesEquiv S 5 x * toSpeciesEquiv T 5 x * toSpeciesEquiv L 5 x) =
∑ x,
(6 * (toSpeciesEquiv S 0 x * toSpeciesEquiv L 0 x * toSpeciesEquiv T 0 x) +
3 * (toSpeciesEquiv S 1 x * toSpeciesEquiv L 1 x * toSpeciesEquiv T 1 x) +
3 * (toSpeciesEquiv S 2 x * toSpeciesEquiv L 2 x * toSpeciesEquiv T 2 x) +
2 * (toSpeciesEquiv S 3 x * toSpeciesEquiv L 3 x * toSpeciesEquiv T 3 x) +
toSpeciesEquiv S 4 x * toSpeciesEquiv L 4 x * toSpeciesEquiv T 4 x +
toSpeciesEquiv S 5 x * toSpeciesEquiv L 5 x * toSpeciesEquiv T 5 x)
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).ChargesL:(SMνCharges n).Chargesi:Fin (SMνSpecies n).numberCharges⊢ 6 * (toSpeciesEquiv S 0 i * toSpeciesEquiv T 0 i * toSpeciesEquiv L 0 i) +
3 * (toSpeciesEquiv S 1 i * toSpeciesEquiv T 1 i * toSpeciesEquiv L 1 i) +
3 * (toSpeciesEquiv S 2 i * toSpeciesEquiv T 2 i * toSpeciesEquiv L 2 i) +
2 * (toSpeciesEquiv S 3 i * toSpeciesEquiv T 3 i * toSpeciesEquiv L 3 i) +
toSpeciesEquiv S 4 i * toSpeciesEquiv T 4 i * toSpeciesEquiv L 4 i +
toSpeciesEquiv S 5 i * toSpeciesEquiv T 5 i * toSpeciesEquiv L 5 i =
6 * (toSpeciesEquiv S 0 i * toSpeciesEquiv L 0 i * toSpeciesEquiv T 0 i) +
3 * (toSpeciesEquiv S 1 i * toSpeciesEquiv L 1 i * toSpeciesEquiv T 1 i) +
3 * (toSpeciesEquiv S 2 i * toSpeciesEquiv L 2 i * toSpeciesEquiv T 2 i) +
2 * (toSpeciesEquiv S 3 i * toSpeciesEquiv L 3 i * toSpeciesEquiv T 3 i) +
toSpeciesEquiv S 4 i * toSpeciesEquiv L 4 i * toSpeciesEquiv T 4 i +
toSpeciesEquiv S 5 i * toSpeciesEquiv L 5 i * toSpeciesEquiv T 5 i
All goals completed! 🐙)All goals completed! 🐙The cubic ACC.
@[simp]
def accCube : HomogeneousCubic (SMνCharges n).Charges := cubeTriLin.toCubicn:ℕS:(SMνCharges n).Charges⊢ 6 * ∑ i, Q S i * Q S i * Q S i + 3 * ∑ i, U S i * U S i * U S i + 3 * ∑ i, D S i * D S i * D S i +
2 * ∑ i, L S i * L S i * L S i +
∑ i, E S i * E S i * E S i +
∑ i, N S i * N S i * N S i =
6 * ∑ i, Q S i ^ 3 + 3 * ∑ i, U S i ^ 3 + 3 * ∑ i, D S i ^ 3 + 2 * ∑ i, L S i ^ 3 + ∑ i, E S i ^ 3 + ∑ i, N S i ^ 3
All goals completed! 🐙
Extensionality lemma for accCube.
n:ℕS:(SMνCharges n).ChargesT:(SMνCharges n).Chargesh:∀ (j : Fin 6), ∑ i, ((fun a => a ^ 3) ∘ (toSpecies j) S) i = ∑ i, ((fun a => a ^ 3) ∘ (toSpecies j) T) i⊢ 6 * ∑ i, Q S i ^ 3 + 3 * ∑ i, U S i ^ 3 + 3 * ∑ i, D S i ^ 3 + 2 * ∑ i, L S i ^ 3 + ∑ i, E S i ^ 3 + ∑ i, N S i ^ 3 =
6 * ∑ i, Q T i ^ 3 + 3 * ∑ i, U T i ^ 3 + 3 * ∑ i, D T i ^ 3 + 2 * ∑ i, L T i ^ 3 + ∑ i, E T i ^ 3 + ∑ i, N T i ^ 3
All goals completed! 🐙