Physlib.QFT.QED.AnomalyCancellation.LowDim.Three

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 3 fermion

We show that S is a solution only if one of its charges is zero. We define a surjective map from LinSols with a charge equal to zero to Sols.

              @[expose] public section

lemma cube_for_linSol' (S : (PureU1 3).LinSols) :
    3 * S.val (0 : Fin 3) * S.val (1 : Fin 3) * S.val (2 : Fin 3) = 0 ↔
    (PureU1 3).cubicACC S.val = 0 := byS:(PureU1 3).LinSols⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0
  have hL := pureU1_linear SS:(PureU1 3).LinSolshL:∑ i, S.val i = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0
  rw [Fin.sum_univ_threeS:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0] at hLS:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0
  change _ ↔ accCube _ _ = _S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ (accCube 3) S.val = 0
  rw [accCube_explicit,S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ ∑ i, S.val i ^ 3 = 0S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 = 0 Fin.sum_univ_threeS:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 = 0S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 = 0]S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 = 0
  rw [show S.val (0 : Fin 3) = - (S.val (1 : Fin 3) + S.val (2 : Fin 3)) byS:(PureU1 3).LinSols⊢ 3 * S.val 0 * S.val 1 * S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * -(S.val 1 + S.val 2) * S.val 1 * S.val 2 = 0 ↔ (-(S.val 1 + S.val 2)) ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 = 0
      linear_combination hLAll goals completed! 🐙S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * -(S.val 1 + S.val 2) * S.val 1 * S.val 2 = 0 ↔ (-(S.val 1 + S.val 2)) ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 = 0]S:(PureU1 3).LinSolshL:S.val 0 + S.val 1 + S.val 2 = 0⊢ 3 * -(S.val 1 + S.val 2) * S.val 1 * S.val 2 = 0 ↔ (-(S.val 1 + S.val 2)) ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 = 0
  ring_nfAll goals completed! 🐙lemma cube_for_linSol (S : (PureU1 3).LinSols) :
    (S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0 ∨ S.val (2 : Fin 3) = 0) ↔
    (PureU1 3).cubicACC S.val = 0 := byS:(PureU1 3).LinSols⊢ S.val 0 = 0 ∨ S.val 1 = 0 ∨ S.val 2 = 0 ↔ (PureU1 3).cubicACC S.val = 0
  simp only [← cube_for_linSol', Fin.isValue, _root_.mul_eq_zero, OfNat.ofNat_ne_zero,
    false_or, or_assoc]All goals completed! 🐙lemma three_sol_zero (S : (PureU1 3).Sols) : S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0
    ∨ S.val (2 : Fin 3) = 0 := (cube_for_linSol S.1.1).mpr S.cubicSol

Given a LinSol with a charge equal to zero a Sol.

def solOfLinear (S : (PureU1 3).LinSols)
    (hS : S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0 ∨ S.val (2 : Fin 3) = 0) :
    (PureU1 3).Sols :=
  ⟨⟨S, fun i => Fin.elim0 i⟩,
    (cube_for_linSol S).mp hS⟩

theorem solOfLinear_surjects (S : (PureU1 3).Sols) :
    ∃ (T : (PureU1 3).LinSols) (hT : T.val (0 : Fin 3) = 0 ∨ T.val (1 : Fin 3) = 0
    ∨ T.val (2 : Fin 3) = 0), solOfLinear T hT = S :=
  ⟨S.1.1, three_sol_zero S, rfl⟩