Physlib.QFT.QED.AnomalyCancellation.Basic

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.LinearCombination

Anomaly cancellation of a theory with a pure U(1)-gauge group

In a pure U(1) gauge theory with n Weyl fermions carrying charges xᵢ the anomaly cancellation conditions (ACCs) which must be satisfied for a consistent gauge theory correspond to:

The linear ACC: ∑ xᵢ = 0

The cubic ACC: ∑ xᵢ³ = 0

The charges xᵢ have rational fractions with one another, here they are specified as rational numbers.

@[expose] public section

TODO "The implementation of pure U(1) anomaly cancellation conditions is done
  currently through the type `ACCSystemCharges`. This whole directory could be
  simplified by refactoring to remove `ACCSystemCharges` defining `PureU1Charges` as
  `Fin n → ℚ` directly, or this space quotiented by permutations and overall factors."

The vector space of charges.

@[simps!]
def PureU1Charges (n : ℕ) : ACCSystemCharges := ⟨n⟩

The symmetric trilinear form used to define the cubic anomaly.


@[simps!]
def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := TriLinearSymm.mk₃
  (fun S => ∑ i, S.1 i * S.2.1 i * S.2.2 i)
  (byn:ℕ⊢ ∀ (a : ℚ) (S T L : (PureU1Charges n).Charges),
  ∑ i, (a • S, T, L).1 i * (a • S, T, L).2.1 i * (a • S, T, L).2.2 i =
    a * ∑ i, (S, T, L).1 i * (S, T, L).2.1 i * (S, T, L).2.2 i
    intro a S L Tn:ℕa:ℚS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∑ i, (a • S, L, T).1 i * (a • S, L, T).2.1 i * (a • S, L, T).2.2 i =
  a * ∑ i, (S, L, T).1 i * (S, L, T).2.1 i * (S, L, T).2.2 i
    simp only [HSMul.hSMul, ACCSystemCharges.chargesModule_smul]n:ℕa:ℚS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∑ x, a * S x * L x * T x = a * ∑ x, S x * L x * T x
    rw [Finset.mul_sumn:ℕa:ℚS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∑ x, a * S x * L x * T x = ∑ i, a * (S i * L i * T i)n:ℕa:ℚS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∑ x, a * S x * L x * T x = ∑ i, a * (S i * L i * T i)]n:ℕa:ℚS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∑ x, a * S x * L x * T x = ∑ i, a * (S i * L i * T i)
    apply Fintype.sum_congrn:ℕa:ℚS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∀ (a_1 : Fin (PureU1Charges n).numberCharges), a * S a_1 * L a_1 * T a_1 = a * (S a_1 * L a_1 * T a_1)
    intro in:ℕa:ℚS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Chargesi:Fin (PureU1Charges n).numberCharges⊢ a * S i * L i * T i = a * (S i * L i * T i)
    ringAll goals completed! 🐙)
  (byn:ℕ⊢ ∀ (S1 S2 T L : (PureU1Charges n).Charges),
  ∑ i, (S1 + S2, T, L).1 i * (S1 + S2, T, L).2.1 i * (S1 + S2, T, L).2.2 i =
    ∑ i, (S1, T, L).1 i * (S1, T, L).2.1 i * (S1, T, L).2.2 i +
      ∑ i, (S2, T, L).1 i * (S2, T, L).2.1 i * (S2, T, L).2.2 i
    intro S L T Rn:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).ChargesR:(PureU1Charges n).Charges⊢ ∑ i, (S + L, T, R).1 i * (S + L, T, R).2.1 i * (S + L, T, R).2.2 i =
  ∑ i, (S, T, R).1 i * (S, T, R).2.1 i * (S, T, R).2.2 i + ∑ i, (L, T, R).1 i * (L, T, R).2.1 i * (L, T, R).2.2 i
    simp only [ACCSystemCharges.chargesAddCommMonoid_add]n:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).ChargesR:(PureU1Charges n).Charges⊢ ∑ x, (S x + L x) * T x * R x = ∑ x, S x * T x * R x + ∑ x, L x * T x * R x
    rw [← Finset.sum_add_distribn:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).ChargesR:(PureU1Charges n).Charges⊢ ∑ x, (S x + L x) * T x * R x = ∑ x, (S x * T x * R x + L x * T x * R x)n:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).ChargesR:(PureU1Charges n).Charges⊢ ∑ x, (S x + L x) * T x * R x = ∑ x, (S x * T x * R x + L x * T x * R x)]n:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).ChargesR:(PureU1Charges n).Charges⊢ ∑ x, (S x + L x) * T x * R x = ∑ x, (S x * T x * R x + L x * T x * R x)
    apply Fintype.sum_congrn:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).ChargesR:(PureU1Charges n).Charges⊢ ∀ (a : Fin (PureU1Charges n).numberCharges), (S a + L a) * T a * R a = S a * T a * R a + L a * T a * R a
    intro in:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).ChargesR:(PureU1Charges n).Chargesi:Fin (PureU1Charges n).numberCharges⊢ (S i + L i) * T i * R i = S i * T i * R i + L i * T i * R i
    ringAll goals completed! 🐙)
  (byn:ℕ⊢ ∀ (S T L : (PureU1Charges n).Charges),
  ∑ i, (S, T, L).1 i * (S, T, L).2.1 i * (S, T, L).2.2 i = ∑ i, (T, S, L).1 i * (T, S, L).2.1 i * (T, S, L).2.2 i
    intro S L Tn:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∑ i, (S, L, T).1 i * (S, L, T).2.1 i * (S, L, T).2.2 i = ∑ i, (L, S, T).1 i * (L, S, T).2.1 i * (L, S, T).2.2 i
    apply Fintype.sum_congrn:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∀ (a : Fin (PureU1Charges n).numberCharges),
  (S, L, T).1 a * (S, L, T).2.1 a * (S, L, T).2.2 a = (L, S, T).1 a * (L, S, T).2.1 a * (L, S, T).2.2 a
    intro in:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Chargesi:Fin (PureU1Charges n).numberCharges⊢ (S, L, T).1 i * (S, L, T).2.1 i * (S, L, T).2.2 i = (L, S, T).1 i * (L, S, T).2.1 i * (L, S, T).2.2 i
    ringAll goals completed! 🐙)
  (byn:ℕ⊢ ∀ (S T L : (PureU1Charges n).Charges),
  ∑ i, (S, T, L).1 i * (S, T, L).2.1 i * (S, T, L).2.2 i = ∑ i, (S, L, T).1 i * (S, L, T).2.1 i * (S, L, T).2.2 i
    intro S L Tn:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∑ i, (S, L, T).1 i * (S, L, T).2.1 i * (S, L, T).2.2 i = ∑ i, (S, T, L).1 i * (S, T, L).2.1 i * (S, T, L).2.2 i
    apply Fintype.sum_congrn:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Charges⊢ ∀ (a : Fin (PureU1Charges n).numberCharges),
  (S, L, T).1 a * (S, L, T).2.1 a * (S, L, T).2.2 a = (S, T, L).1 a * (S, T, L).2.1 a * (S, T, L).2.2 a
    intro in:ℕS:(PureU1Charges n).ChargesL:(PureU1Charges n).ChargesT:(PureU1Charges n).Chargesi:Fin (PureU1Charges n).numberCharges⊢ (S, L, T).1 i * (S, L, T).2.1 i * (S, L, T).2.2 i = (S, T, L).1 i * (S, T, L).2.1 i * (S, T, L).2.2 i
    ringAll goals completed! 🐙)

The cubic anomaly equation.

@[simp]
def accCube (n : ℕ) : HomogeneousCubic ((PureU1Charges n).Charges) :=
  (accCubeTriLinSymm).toCubic

The cubic ACC for the pure-U(1) anomaly equations is equal to the sum of the cubed charges.


lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).Charges) :
    accCube n S = ∑ i : Fin n, S i ^ 3:= byn:ℕS:(PureU1Charges n).Charges⊢ (accCube n) S = ∑ i, S i ^ 3
  rw [accCube,n:ℕS:(PureU1Charges n).Charges⊢ accCubeTriLinSymm.toCubic S = ∑ i, S i ^ 3n:ℕS:(PureU1Charges n).Charges⊢ { toFun := fun S => ((accCubeTriLinSymm S) S) S, map_smul' := ⋯ } S = ∑ i, S i ^ 3 TriLinearSymm.toCubicn:ℕS:(PureU1Charges n).Charges⊢ { toFun := fun S => ((accCubeTriLinSymm S) S) S, map_smul' := ⋯ } S = ∑ i, S i ^ 3n:ℕS:(PureU1Charges n).Charges⊢ { toFun := fun S => ((accCubeTriLinSymm S) S) S, map_smul' := ⋯ } S = ∑ i, S i ^ 3]n:ℕS:(PureU1Charges n).Charges⊢ { toFun := fun S => ((accCubeTriLinSymm S) S) S, map_smul' := ⋯ } S = ∑ i, S i ^ 3
  change accCubeTriLinSymm S S S = _n:ℕS:(PureU1Charges n).Charges⊢ ((accCubeTriLinSymm S) S) S = ∑ i, S i ^ 3
  rw [accCubeTriLinSymmn:ℕS:(PureU1Charges n).Charges⊢ (((TriLinearSymm.mk₃ (fun S => ∑ i, S.1 i * S.2.1 i * S.2.2 i) ⋯ ⋯ ⋯ ⋯) S) S) S = ∑ i, S i ^ 3n:ℕS:(PureU1Charges n).Charges⊢ (((TriLinearSymm.mk₃ (fun S => ∑ i, S.1 i * S.2.1 i * S.2.2 i) ⋯ ⋯ ⋯ ⋯) S) S) S = ∑ i, S i ^ 3]n:ℕS:(PureU1Charges n).Charges⊢ (((TriLinearSymm.mk₃ (fun S => ∑ i, S.1 i * S.2.1 i * S.2.2 i) ⋯ ⋯ ⋯ ⋯) S) S) S = ∑ i, S i ^ 3
  simp only [TriLinearSymm.mk₃_toFun_apply_apply]n:ℕS:(PureU1Charges n).Charges⊢ ∑ x, S x * S x * S x = ∑ i, S i ^ 3
  exact Finset.sum_congr rfl fun x _ => Eq.symm (pow_three' (S x))All goals completed! 🐙

The ACC system for a pure $U(1)$ gauge theory with $n$ fermions.

@[simps!]
def PureU1 (n : ℕ) : ACCSystem where
  numberCharges := n
  numberLinear := 1
  linearACCs := fun i =>
    match i with
    | 0 => PureU1.accGrav n
  numberQuadratic := 0
  quadraticACCs := Fin.elim0
  cubicACC := PureU1.accCube n

An equivalence of vector spaces of charges when the number of fermions is equal.

def pureU1EqCharges {n m : ℕ} (h : n = m) :
    (PureU1 n).Charges ≃ₗ[ℚ] (PureU1 m).Charges where
  toFun f := f ∘ Fin.cast h.symm
  invFun f := f ∘ Fin.cast h
  map_add' _ _ := rfl
  map_smul' _ _:= rfl
  left_inv _ := rfl
  right_inv _ := rfl

A solution to the pure U(1) accs satisfies the linear ACCs.

lemma pureU1_linear {n : ℕ} (S : (PureU1 n).LinSols) :
    ∑ (i : Fin n), S.val i = 0 := byn:ℕS:(PureU1 n).LinSols⊢ ∑ i, S.val i = 0
  have hS := S.linearSoln:ℕS:(PureU1 n).LinSolshS:∀ (i : Fin (PureU1 n).numberLinear), ((PureU1 n).linearACCs i) S.val = 0⊢ ∑ i, S.val i = 0
  simp only [PureU1_linearACCs] at hSn:ℕS:(PureU1 n).LinSolshS:∀ (i : Fin (PureU1 n).numberLinear),
  (match i with
      | 0 => PureU1.accGrav n)
      S.val =
    0⊢ ∑ i, S.val i = 0
  exact hS ⟨0, byn:ℕS:(PureU1 n).LinSolshS:∀ (i : Fin (PureU1 n).numberLinear),
  (match i with
      | 0 => PureU1.accGrav n)
      S.val =
    0⊢ 0 < (PureU1 n).numberLinear simpAll goals completed! 🐙⟩

A solution to the pure U(1) accs satisfies the cubic ACCs.


lemma pureU1_cube {n : ℕ} (S : (PureU1 n).Sols) :
    ∑ i, (S.val i) ^ 3 = 0 := byn:ℕS:(PureU1 n).Sols⊢ ∑ i, S.val i ^ 3 = 0
  rw [← PureU1.accCube_explicitn:ℕS:(PureU1 n).Sols⊢ (PureU1.accCube (PureU1 n).numberCharges) S.val = 0n:ℕS:(PureU1 n).Sols⊢ (PureU1.accCube (PureU1 n).numberCharges) S.val = 0]n:ℕS:(PureU1 n).Sols⊢ (PureU1.accCube (PureU1 n).numberCharges) S.val = 0
  exact S.cubicSolAll goals completed! 🐙

The last charge of a solution to the linear ACCs is equal to the negation of the sum of the other charges.


lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
    S.val (Fin.last n) = - ∑ i : Fin n, S.val i.castSucc := byn:ℕS:(PureU1 n.succ).LinSols⊢ S.val (Fin.last n) = -∑ i, S.val i.castSucc
  have hS := pureU1_linear Sn:ℕS:(PureU1 n.succ).LinSolshS:∑ i, S.val i = 0⊢ S.val (Fin.last n) = -∑ i, S.val i.castSucc
  simp only [succ_eq_add_one] at hSn:ℕS:(PureU1 n.succ).LinSolshS:∑ x, S.val x = 0⊢ S.val (Fin.last n) = -∑ i, S.val i.castSucc
  rw [Fin.sum_univ_castSuccn:ℕS:(PureU1 n.succ).LinSolshS:∑ i, S.val i.castSucc + S.val (Fin.last n) = 0⊢ S.val (Fin.last n) = -∑ i, S.val i.castSuccn:ℕS:(PureU1 n.succ).LinSolshS:∑ i, S.val i.castSucc + S.val (Fin.last n) = 0⊢ S.val (Fin.last n) = -∑ i, S.val i.castSucc] at hSn:ℕS:(PureU1 n.succ).LinSolshS:∑ i, S.val i.castSucc + S.val (Fin.last n) = 0⊢ S.val (Fin.last n) = -∑ i, S.val i.castSucc
  linear_combination hSAll goals completed! 🐙

Two solutions to the Linear ACCs for n.succ are equal if their first n charges are equal.


lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
    (h : ∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc) : S = T := byn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc⊢ S = T
  apply ACCSystemLinear.LinSols.extn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc⊢ S.val = T.val
  funext in:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberCharges⊢ S.val i = T.val i
  rcases Fin.eq_castSucc_or_eq_last i with hi | hiinln:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:∃ j, i = j.castSucc⊢ S.val i = T.val iinrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ S.val i = T.val i
  ·inln:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:∃ j, i = j.castSucc⊢ S.val i = T.val i obtain ⟨j, hj⟩ := hiinln:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargesj:Fin nhj:i = j.castSucc⊢ S.val i = T.val i
    subst hjinln:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSuccj:Fin n⊢ S.val j.castSucc = T.val j.castSucc
    exact h jAll goals completed! 🐙
  ·inrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ S.val i = T.val i rw [hi,inrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ S.val (Fin.last n) = T.val (Fin.last n)inrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ -∑ i, S.val i.castSucc = -∑ i, T.val i.castSucc pureU1_last,inrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ -∑ i, S.val i.castSucc = T.val (Fin.last n)inrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ -∑ i, S.val i.castSucc = -∑ i, T.val i.castSucc pureU1_lastinrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ -∑ i, S.val i.castSucc = -∑ i, T.val i.castSuccinrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ -∑ i, S.val i.castSucc = -∑ i, T.val i.castSucc]inrn:ℕS:(PureU1 n.succ).LinSolsT:(PureU1 n.succ).LinSolsh:∀ (i : Fin n), S.val i.castSucc = T.val i.castSucci:Fin (PureU1 n.succ).numberChargeshi:i = Fin.last n⊢ -∑ i, S.val i.castSucc = -∑ i, T.val i.castSucc
    exact neg_inj.mpr (Finset.sum_congr rfl fun j _ => h j)All goals completed! 🐙

The jth charge of a sum of pure-U(1) charges is equal to the sum of their jth charges.


lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
    (∑ i : Fin k, (f i)) j = ∑ i : Fin k, (f i) j := byk:ℕn:ℕf:Fin k → (PureU1 n).Chargesj:Fin n⊢ (∑ i, f i) j = ∑ i, f i j
  induction kzeron:ℕj:Fin nf:Fin 0 → (PureU1 n).Charges⊢ (∑ i, f i) j = ∑ i, f i jsuccn:ℕj:Fin nn✝:ℕa✝:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i) j = ∑ i, f i j
  ·zeron:ℕj:Fin nf:Fin 0 → (PureU1 n).Charges⊢ (∑ i, f i) j = ∑ i, f i j rflAll goals completed! 🐙
  ·succn:ℕj:Fin nn✝:ℕa✝:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i) j = ∑ i, f i j rename_i k hlsuccn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i) j = ∑ i, f i j
    rw [Fin.sum_univ_castSucc,succn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i.castSucc + f (Fin.last k)) j = ∑ i, f i jsuccn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i.castSucc + f (Fin.last k)) j = ∑ i, f i.castSucc j + f (Fin.last k) j Fin.sum_univ_castSuccsuccn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i.castSucc + f (Fin.last k)) j = ∑ i, f i.castSucc j + f (Fin.last k) jsuccn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i.castSucc + f (Fin.last k)) j = ∑ i, f i.castSucc j + f (Fin.last k) j]succn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i.castSucc + f (Fin.last k)) j = ∑ i, f i.castSucc j + f (Fin.last k) j
    erw [← hl (f ∘ Fin.castSucc)succn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i.castSucc + f (Fin.last k)) j = (∑ i, (f ∘ Fin.castSucc) i) j + f (Fin.last k) j]succn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).Charges), (∑ i, f i) j = ∑ i, f i jf:Fin (n✝ + 1) → (PureU1 n).Charges⊢ (∑ i, f i.castSucc + f (Fin.last k)) j = (∑ i, (f ∘ Fin.castSucc) i) j + f (Fin.last k) j
    rflAll goals completed! 🐙

The jth charge of a sum of solutions to the linear ACC is equal to the sum of their jth charges.


lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
    (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := byk:ℕn:ℕf:Fin k → (PureU1 n).LinSolsj:Fin n⊢ (∑ i, f i).val j = ∑ i, (f i).val j
  induction kzeron:ℕj:Fin nf:Fin 0 → (PureU1 n).LinSols⊢ (∑ i, f i).val j = ∑ i, (f i).val jsuccn:ℕj:Fin nn✝:ℕa✝:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i).val j = ∑ i, (f i).val j
  ·zeron:ℕj:Fin nf:Fin 0 → (PureU1 n).LinSols⊢ (∑ i, f i).val j = ∑ i, (f i).val j rflAll goals completed! 🐙
  ·succn:ℕj:Fin nn✝:ℕa✝:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i).val j = ∑ i, (f i).val j rename_i k hlsuccn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i).val j = ∑ i, (f i).val j
    rw [Fin.sum_univ_castSucc,succn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i.castSucc + f (Fin.last k)).val j = ∑ i, (f i).val jsuccn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i.castSucc + f (Fin.last k)).val j = ∑ i, (f i.castSucc).val j + (f (Fin.last k)).val j Fin.sum_univ_castSuccsuccn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i.castSucc + f (Fin.last k)).val j = ∑ i, (f i.castSucc).val j + (f (Fin.last k)).val jsuccn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i.castSucc + f (Fin.last k)).val j = ∑ i, (f i.castSucc).val j + (f (Fin.last k)).val j]succn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i.castSucc + f (Fin.last k)).val j = ∑ i, (f i.castSucc).val j + (f (Fin.last k)).val j
    erw [← hl (f ∘ Fin.castSucc)succn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i.castSucc + f (Fin.last k)).val j = (∑ i, (f ∘ Fin.castSucc) i).val j + (f (Fin.last k)).val j]succn:ℕj:Fin nk:ℕhl:∀ (f : Fin n✝ → (PureU1 n).LinSols), (∑ i, f i).val j = ∑ i, (f i).val jf:Fin (n✝ + 1) → (PureU1 n).LinSols⊢ (∑ i, f i.castSucc + f (Fin.last k)).val j = (∑ i, (f ∘ Fin.castSucc) i).val j + (f (Fin.last k)).val j
    rflAll goals completed! 🐙