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.Basic
public import Mathlib.Tactic.LinearCombinationAnomaly cancellation conditions for the n-family SM.
We define the ACC system for the Standard Model withn-families and no RHN.
@[expose] public sectionAssociate to each (including RHN) SM fermion a set of charges
@[simps!]
def SMCharges (n : ℕ) : ACCSystemCharges := ⟨5 * n⟩The vector space associated with a single species of fermions.
@[simps!]
def SMSpecies (n : ℕ) : ACCSystemCharges := ⟨n⟩lemma sum_SMSpecies_numberCharges_one {M} [AddCommMonoid M]
(f : Fin (SMSpecies 1).numberCharges → M) :
∑ i, f i = f ⟨0, n:ℕM:Type ?u.4inst✝:AddCommMonoid Mf:Fin (SMSpecies 1).numberCharges → M⊢ 0 < (SMSpecies 1).numberCharges All goals completed! 🐙⟩ := M:Type u_1inst✝:AddCommMonoid Mf:Fin (SMSpecies 1).numberCharges → M⊢ ∑ i, f i = f ⟨0, ⋯⟩
M:Type u_1inst✝:AddCommMonoid Mf:Fin (SMSpecies 1).numberCharges → M⊢ ∑ i, f i = f ⟨0, ⋯⟩
M:Type u_1inst✝:AddCommMonoid Mf:Fin (SMSpecies 1).numberCharges → M⊢ f 0 = f ⟨0, ⋯⟩
All goals completed! 🐙
An equivalence between the set (SMCharges n).charges and the set
(Fin 5 → Fin n → ℚ).
@[simps!]
def toSpeciesEquiv : (SMCharges n).Charges ≃ (Fin 5 → Fin (SMSpecies n).numberCharges → ℚ) :=
((Equiv.curry _ _ _).symm.trans ((@finProdFinEquiv 5
(SMSpecies n).numberCharges).arrowCongr (Equiv.refl ℚ))).symm
For a given i ∈ Fin 5, the projection of a charge onto that species.
@[simps!]
def toSpecies (i : Fin 5) : (SMCharges n).Charges →ₗ[ℚ] (SMSpecies n).Charges where
toFun S := toSpeciesEquiv S i
map_add' _ _ := n:ℕi:Fin 5x✝¹:(SMCharges n).Chargesx✝:(SMCharges n).Charges⊢ toSpeciesEquiv (x✝¹ + x✝) i = toSpeciesEquiv x✝¹ i + toSpeciesEquiv x✝ i All goals completed! 🐙
map_smul' _ _ := n:ℕi:Fin 5x✝¹:ℚx✝:(SMCharges n).Charges⊢ toSpeciesEquiv (x✝¹ • x✝) i = (RingHom.id ℚ) x✝¹ • toSpeciesEquiv x✝ i All goals completed! 🐙lemma toSpecies_apply_eq (i : Fin 5) (S : (SMCharges n).Charges) :
toSpecies i S = fun j => toSpeciesEquiv S i j := n:ℕi:Fin 5S:(SMCharges n).Charges⊢ (toSpecies i) S = fun j => toSpeciesEquiv S i j All goals completed! 🐙lemma charges_eq_toSpecies_eq (S T : (SMCharges n).Charges) :
S = T ↔ ∀ i, toSpecies i S = toSpecies i T := n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Charges⊢ S = T ↔ ∀ (i : Fin 5), (toSpecies i) S = (toSpecies i) T
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargesh:∀ (i : Fin 5), (toSpecies i) S = (toSpecies i) T⊢ S = T
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargesh:∀ (i : Fin 5), (toSpecies i) S = (toSpecies i) T⊢ toSpeciesEquiv S = toSpeciesEquiv T
All goals completed! 🐙lemma toSMSpecies_toSpecies_inv (i : Fin 5) (f : Fin 5 → Fin n → ℚ) :
(toSpecies i) (toSpeciesEquiv.symm f) = f i := n:ℕi:Fin 5f:Fin 5 → Fin n → ℚ⊢ (toSpecies i) (toSpeciesEquiv.symm f) = f i
n:ℕi:Fin 5f:Fin 5 → Fin n → ℚ⊢ (⇑toSpeciesEquiv ∘ ⇑toSpeciesEquiv.symm) f i = f i
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 4The gravitational anomaly equation.
n:ℕa:ℚS:(SMCharges 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 *
(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)
--rw [show Rat.cast a = a from rfl]
All goals completed! 🐙
Extensionality lemma for accGrav.
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargeshj:∀ (j : Fin 5), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i⊢ 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 =
6 * ∑ i, toSpeciesEquiv T 0 i + 3 * ∑ i, toSpeciesEquiv T 1 i + 3 * ∑ i, toSpeciesEquiv T 2 i +
2 * ∑ i, toSpeciesEquiv T 3 i +
∑ x, toSpeciesEquiv T 4 x
All goals completed! 🐙
The SU(2) anomaly equation.
n:ℕa:ℚS:(SMCharges 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! 🐙
Extensionality lemma for accSU2.
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargeshj:∀ (j : Fin 5), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i⊢ 3 * ∑ i, toSpeciesEquiv S 0 i + ∑ x, toSpeciesEquiv S 3 x = 3 * ∑ i, toSpeciesEquiv T 0 i + ∑ x, toSpeciesEquiv T 3 x
All goals completed! 🐙
The SU(3) anomaly equations.
n:ℕa:ℚS:(SMCharges 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! 🐙
Extensionality lemma for accSU3.
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargeshj:∀ (j : Fin 5), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i⊢ 2 * ∑ i, toSpeciesEquiv S 0 i + ∑ x, toSpeciesEquiv S 1 x + ∑ x, toSpeciesEquiv S 2 x =
2 * ∑ i, toSpeciesEquiv T 0 i + ∑ x, toSpeciesEquiv T 1 x + ∑ x, toSpeciesEquiv T 2 x
All goals completed! 🐙
The Y² anomaly equation.
n:ℕa:ℚS:(SMCharges 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)
All goals completed! 🐙
Extensionality lemma for accYY.
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargeshj:∀ (j : Fin 5), ∑ i, (toSpecies j) S i = ∑ i, (toSpecies j) T i⊢ ∑ 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 =
∑ x, toSpeciesEquiv T 0 x + 8 * ∑ i, toSpeciesEquiv T 1 i + 2 * ∑ i, toSpeciesEquiv T 2 i +
3 * ∑ i, toSpeciesEquiv T 3 i +
6 * ∑ i, toSpeciesEquiv T 4 i
All goals completed! 🐙The quadratic bilinear map.
n:ℕS1:(SMCharges n).ChargesS2:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin (SMSpecies n).numberCharges⊢ (Q S1 + Q S2) i * Q T i + -2 * ((U S1 + U S2) i * U T i) + (D S1 + D S2) i * D T i + -1 * ((L S1 + L S2) i * L T i) +
(E S1 + E S2) i * E T i =
Q S1 i * Q T i + -2 * (U S1 i * U T i) + D S1 i * D T i + -1 * (L S1 i * L T i) + E S1 i * E T i +
(Q S2 i * Q T i + -2 * (U S2 i * U T i) + D S2 i * D T i + -1 * (L S2 i * L T i) + E S2 i * E T i)
n:ℕS1:(SMCharges n).ChargesS2:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin (SMSpecies n).numberCharges⊢ (toSpeciesEquiv S1 0 i + toSpeciesEquiv S2 0 i) * toSpeciesEquiv T 0 i +
-(2 * ((toSpeciesEquiv S1 1 i + toSpeciesEquiv S2 1 i) * toSpeciesEquiv T 1 i)) +
(toSpeciesEquiv S1 2 i + toSpeciesEquiv S2 2 i) * toSpeciesEquiv T 2 i +
-((toSpeciesEquiv S1 3 i + toSpeciesEquiv S2 3 i) * toSpeciesEquiv T 3 i) +
(toSpeciesEquiv S1 4 i + toSpeciesEquiv S2 4 i) * toSpeciesEquiv T 4 i =
toSpeciesEquiv S1 0 i * toSpeciesEquiv T 0 i + -(2 * (toSpeciesEquiv S1 1 i * toSpeciesEquiv T 1 i)) +
toSpeciesEquiv S1 2 i * toSpeciesEquiv T 2 i +
-(toSpeciesEquiv S1 3 i * toSpeciesEquiv T 3 i) +
toSpeciesEquiv S1 4 i * toSpeciesEquiv T 4 i +
(toSpeciesEquiv S2 0 i * toSpeciesEquiv T 0 i + -(2 * (toSpeciesEquiv S2 1 i * toSpeciesEquiv T 1 i)) +
toSpeciesEquiv S2 2 i * toSpeciesEquiv T 2 i +
-(toSpeciesEquiv S2 3 i * toSpeciesEquiv T 3 i) +
toSpeciesEquiv S2 4 i * toSpeciesEquiv T 4 i)
All goals completed! 🐙)
(n:ℕ⊢ ∀ (S T : (SMCharges 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:(SMCharges n).ChargesT:(SMCharges 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:(SMCharges n).ChargesT:(SMCharges 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:(SMCharges n).ChargesT:(SMCharges n).Charges⊢ ∀ (a : Fin (SMSpecies n).numberCharges),
toSpeciesEquiv S 0 a * toSpeciesEquiv T 0 a + -(2 * (toSpeciesEquiv S 1 a * toSpeciesEquiv T 1 a)) +
toSpeciesEquiv S 2 a * toSpeciesEquiv T 2 a +
-(toSpeciesEquiv S 3 a * toSpeciesEquiv T 3 a) +
toSpeciesEquiv S 4 a * toSpeciesEquiv T 4 a =
toSpeciesEquiv T 0 a * toSpeciesEquiv S 0 a + -(2 * (toSpeciesEquiv T 1 a * toSpeciesEquiv S 1 a)) +
toSpeciesEquiv T 2 a * toSpeciesEquiv S 2 a +
-(toSpeciesEquiv T 3 a * toSpeciesEquiv S 3 a) +
toSpeciesEquiv T 4 a * toSpeciesEquiv S 4 a
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargesi:Fin (SMSpecies 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! 🐙)The quadratic anomaly cancellation condition.
@[simp]
def accQuad : HomogeneousQuadratic (SMCharges n).Charges :=
(@quadBiLin n).toHomogeneousQuad
Extensionality lemma for accQuad.
set_option backward.isDefEq.respectTransparency false inn:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargesh:∀ (j : Fin 5), ∑ i, ((fun a => a ^ 2) ∘ (toSpecies j) S) i = ∑ i, ((fun a => a ^ 2) ∘ (toSpecies j) T) i⊢ ∑ x, Q S x * Q S x + -2 * ∑ i, U S i * U S i + ∑ x, D S x * D S x + -1 * ∑ i, L S i * L S i + ∑ x, E S x * E S x =
∑ x, Q T x * Q T x + -2 * ∑ i, U T i * U T i + ∑ x, D T x * D T x + -1 * ∑ i, L T i * L T i + ∑ x, E T x * E T x
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargesh:∀ (j : Fin 5), ∑ i, ((fun a => a ^ 2) ∘ (toSpecies j) S) i = ∑ i, ((fun a => a ^ 2) ∘ (toSpecies j) T) i⊢ ∑ x, Q S x ^ 2 - (∑ x, U S x ^ 2) * 2 + ∑ x, D S x ^ 2 - ∑ x, L S x ^ 2 + ∑ x, E S x ^ 2 =
∑ x, Q T x ^ 2 - (∑ x, U T x ^ 2) * 2 + ∑ x, D T x ^ 2 - ∑ x, L T x ^ 2 + ∑ x, E T x ^ 2
All goals completed! 🐙The trilinear function defining the cubic.
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).ChargesR:(SMCharges n).ChargesL:(SMCharges n).Chargesi:Fin (SMSpecies 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 * ((SMCharges.L S + SMCharges.L T) i * SMCharges.L R i * SMCharges.L L i) +
(E S + E T) i * E R i * E 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 * (SMCharges.L S i * SMCharges.L R i * SMCharges.L L i) +
E S i * E R i * E 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 * (SMCharges.L T i * SMCharges.L R i * SMCharges.L L i) +
E T i * E R i * E L i)
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).ChargesR:(SMCharges n).ChargesL:(SMCharges n).Chargesi:Fin (SMSpecies 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 =
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 +
(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)
All goals completed! 🐙)
(n:ℕ⊢ ∀ (S T L : (SMCharges 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 * (SMCharges.L (S, T, L).1 i * SMCharges.L (S, T, L).2.1 i * SMCharges.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) =
∑ 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 * (SMCharges.L (T, S, L).1 i * SMCharges.L (T, S, L).2.1 i * SMCharges.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:ℕS:(SMCharges n).ChargesT:(SMCharges n).ChargesL:(SMCharges 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 * (SMCharges.L (S, T, L).1 i * SMCharges.L (S, T, L).2.1 i * SMCharges.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) =
∑ 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 * (SMCharges.L (T, S, L).1 i * SMCharges.L (T, S, L).2.1 i * SMCharges.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:ℕS:(SMCharges n).ChargesT:(SMCharges n).ChargesL:(SMCharges 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) =
∑ 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)
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).ChargesL:(SMCharges n).Charges⊢ ∀ (a : Fin (SMSpecies n).numberCharges),
6 * (toSpeciesEquiv S 0 a * toSpeciesEquiv T 0 a * toSpeciesEquiv L 0 a) +
3 * (toSpeciesEquiv S 1 a * toSpeciesEquiv T 1 a * toSpeciesEquiv L 1 a) +
3 * (toSpeciesEquiv S 2 a * toSpeciesEquiv T 2 a * toSpeciesEquiv L 2 a) +
2 * (toSpeciesEquiv S 3 a * toSpeciesEquiv T 3 a * toSpeciesEquiv L 3 a) +
toSpeciesEquiv S 4 a * toSpeciesEquiv T 4 a * toSpeciesEquiv L 4 a =
6 * (toSpeciesEquiv T 0 a * toSpeciesEquiv S 0 a * toSpeciesEquiv L 0 a) +
3 * (toSpeciesEquiv T 1 a * toSpeciesEquiv S 1 a * toSpeciesEquiv L 1 a) +
3 * (toSpeciesEquiv T 2 a * toSpeciesEquiv S 2 a * toSpeciesEquiv L 2 a) +
2 * (toSpeciesEquiv T 3 a * toSpeciesEquiv S 3 a * toSpeciesEquiv L 3 a) +
toSpeciesEquiv T 4 a * toSpeciesEquiv S 4 a * toSpeciesEquiv L 4 a
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).ChargesL:(SMCharges n).Chargesi:Fin (SMSpecies 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 =
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
All goals completed! 🐙)
(n:ℕ⊢ ∀ (S T L : (SMCharges 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 * (SMCharges.L (S, T, L).1 i * SMCharges.L (S, T, L).2.1 i * SMCharges.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) =
∑ 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 * (SMCharges.L (S, L, T).1 i * SMCharges.L (S, L, T).2.1 i * SMCharges.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:(SMCharges n).ChargesT:(SMCharges n).ChargesL:(SMCharges 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 * (SMCharges.L (S, T, L).1 i * SMCharges.L (S, T, L).2.1 i * SMCharges.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) =
∑ 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 * (SMCharges.L (S, L, T).1 i * SMCharges.L (S, L, T).2.1 i * SMCharges.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:(SMCharges n).ChargesT:(SMCharges n).ChargesL:(SMCharges 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) =
∑ 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)
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).ChargesL:(SMCharges n).Charges⊢ ∀ (a : Fin (SMSpecies n).numberCharges),
6 * (toSpeciesEquiv S 0 a * toSpeciesEquiv T 0 a * toSpeciesEquiv L 0 a) +
3 * (toSpeciesEquiv S 1 a * toSpeciesEquiv T 1 a * toSpeciesEquiv L 1 a) +
3 * (toSpeciesEquiv S 2 a * toSpeciesEquiv T 2 a * toSpeciesEquiv L 2 a) +
2 * (toSpeciesEquiv S 3 a * toSpeciesEquiv T 3 a * toSpeciesEquiv L 3 a) +
toSpeciesEquiv S 4 a * toSpeciesEquiv T 4 a * toSpeciesEquiv L 4 a =
6 * (toSpeciesEquiv S 0 a * toSpeciesEquiv L 0 a * toSpeciesEquiv T 0 a) +
3 * (toSpeciesEquiv S 1 a * toSpeciesEquiv L 1 a * toSpeciesEquiv T 1 a) +
3 * (toSpeciesEquiv S 2 a * toSpeciesEquiv L 2 a * toSpeciesEquiv T 2 a) +
2 * (toSpeciesEquiv S 3 a * toSpeciesEquiv L 3 a * toSpeciesEquiv T 3 a) +
toSpeciesEquiv S 4 a * toSpeciesEquiv L 4 a * toSpeciesEquiv T 4 a
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).ChargesL:(SMCharges n).Chargesi:Fin (SMSpecies 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 =
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
All goals completed! 🐙)The cubic acc.
@[simp]
def accCube : HomogeneousCubic (SMCharges n).Charges := cubeTriLin.toCubic
Extensionality lemma for accCube.
set_option backward.isDefEq.respectTransparency false inn:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargesh:∀ (j : Fin 5), ∑ i, ((fun a => a ^ 3) ∘ (toSpecies j) S) i = ∑ i, ((fun a => a ^ 3) ∘ (toSpecies j) T) i⊢ 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 +
∑ x, E S x * E S x * E S x =
6 * ∑ i, Q T i * Q T i * Q T i + 3 * ∑ i, U T i * U T i * U T i + 3 * ∑ i, D T i * D T i * D T i +
2 * ∑ i, L T i * L T i * L T i +
∑ x, E T x * E T x * E T x
n:ℕS:(SMCharges n).ChargesT:(SMCharges n).Chargesh:∀ (j : Fin 5), ∑ i, ((fun a => a ^ 3) ∘ (toSpecies j) S) i = ∑ i, ((fun a => a ^ 3) ∘ (toSpecies j) T) i⊢ (∑ x, Q S x ^ 3) * 6 + (∑ x, U S x ^ 3) * 3 + (∑ x, D S x ^ 3) * 3 + (∑ x, L S x ^ 3) * 2 + ∑ x, E S x ^ 3 =
(∑ x, Q T x ^ 3) * 6 + (∑ x, U T x ^ 3) * 3 + (∑ x, D T x ^ 3) * 3 + (∑ x, L T x ^ 3) * 2 + ∑ x, E T x ^ 3
All goals completed! 🐙