Physlib.QFT.QED.AnomalyCancellation.LowDim.One

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.QED.AnomalyCancellation.Basic

The Pure U(1) case with 1 fermion

We show that in this case the charge must be zero.

@[expose] public section



theorem solEqZero (S : (PureU1 1).LinSols) : S = 0 := byS:(PureU1 1).LinSols⊢ S = 0
  apply ACCSystemLinear.LinSols.extS:(PureU1 1).LinSols⊢ S.val = ACCSystemLinear.LinSols.val 0
  funext iS:(PureU1 1).LinSolsi:Fin (PureU1 1).numberCharges⊢ S.val i = ACCSystemLinear.LinSols.val 0 i
  rw [Fin.fin_one_eq_zero i,S:(PureU1 1).LinSolsi:Fin (PureU1 1).numberCharges⊢ S.val 0 = ACCSystemLinear.LinSols.val 0 0S:(PureU1 1).LinSolsi:Fin (PureU1 1).numberCharges⊢ ∑ i, S.val i = ACCSystemLinear.LinSols.val 0 0 ← Fin.sum_univ_one S.valS:(PureU1 1).LinSolsi:Fin (PureU1 1).numberCharges⊢ ∑ i, S.val i = ACCSystemLinear.LinSols.val 0 0S:(PureU1 1).LinSolsi:Fin (PureU1 1).numberCharges⊢ ∑ i, S.val i = ACCSystemLinear.LinSols.val 0 0]S:(PureU1 1).LinSolsi:Fin (PureU1 1).numberCharges⊢ ∑ i, S.val i = ACCSystemLinear.LinSols.val 0 0
  exact pureU1_linear SAll goals completed! 🐙