Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lemmas

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.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization

Lemmas for 1 family SM Accs

The main result of this file is the conclusion of this paper: [Lohitsiri and Tong][Lohitsiri:2019fuu]

That every solution to the ACCs without gravity satisfies for free the gravitational anomaly.

@[expose] public section

For a set of 1 family SM charges satisfying all ACCs except the gravitational, the charge of Q is zero if and only if E is zero.


lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔
    E S.val (0 : Fin 1) = 0 := byS:(SMNoGrav 1).Sols⊢ Q S.val 0 = 0 ↔ E S.val 0 = 0
  let S' := linearParameters.bijection.symm S.1.1S:(SMNoGrav 1).SolsS':linearParameters := linearParameters.bijection.symm S.toLinSols⊢ Q S.val 0 = 0 ↔ E S.val 0 = 0
  have hC := cubeSol SS:(SMNoGrav 1).SolsS':linearParameters := linearParameters.bijection.symm S.toLinSolshC:accCube S.val = 0⊢ Q S.val 0 = 0 ↔ E S.val 0 = 0
  have hS' := congrArg (fun S => S.val) (linearParameters.bijection.right_inv S.1.1)S:(SMNoGrav 1).SolsS':linearParameters := linearParameters.bijection.symm S.toLinSolshC:accCube S.val = 0hS':(linearParameters.bijection.toFun (linearParameters.bijection.invFun S.toLinSols)).val = S.val⊢ Q S.val 0 = 0 ↔ E S.val 0 = 0
  change S'.asCharges = S.val at hS'S:(SMNoGrav 1).SolsS':linearParameters := linearParameters.bijection.symm S.toLinSolshC:accCube S.val = 0hS':S'.asCharges = S.val⊢ Q S.val 0 = 0 ↔ E S.val 0 = 0
  rw [← hS'S:(SMNoGrav 1).SolsS':linearParameters := linearParameters.bijection.symm S.toLinSolshC:accCube S'.asCharges = 0hS':S'.asCharges = S.val⊢ Q S.val 0 = 0 ↔ E S.val 0 = 0S:(SMNoGrav 1).SolsS':linearParameters := linearParameters.bijection.symm S.toLinSolshC:accCube S'.asCharges = 0hS':S'.asCharges = S.val⊢ Q S.val 0 = 0 ↔ E S.val 0 = 0] at hCS:(SMNoGrav 1).SolsS':linearParameters := linearParameters.bijection.symm S.toLinSolshC:accCube S'.asCharges = 0hS':S'.asCharges = S.val⊢ Q S.val 0 = 0 ↔ E S.val 0 = 0
  exact ⟨S'.cubic_zero_Q'_zero hC, S'.cubic_zero_E'_zero hC⟩All goals completed! 🐙

For a set of 1-family SM charges satisfying all ACCs except the gravitational, if the Q charge is zero then the charges satisfy the gravitational ACCs.


lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) :
    accGrav S.val = 0 := byS:(SMNoGrav 1).SolshQ:Q S.val 0 = 0⊢ accGrav S.val = 0
  rw [accGravS:(SMNoGrav 1).SolshQ:Q S.val 0 = 0⊢ { toFun := fun S => ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i), map_add' := ⋯, map_smul' := ⋯ }
    S.val =
  0S:(SMNoGrav 1).SolshQ:Q S.val 0 = 0⊢ { toFun := fun S => ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i), map_add' := ⋯, map_smul' := ⋯ }
    S.val =
  0]S:(SMNoGrav 1).SolshQ:Q S.val 0 = 0⊢ { toFun := fun S => ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i), map_add' := ⋯, map_smul' := ⋯ }
    S.val =
  0
  have hE := E_zero_iff_Q_zero.mp hQS:(SMNoGrav 1).SolshQ:Q S.val 0 = 0hE:E S.val 0 = 0⊢ { toFun := fun S => ∑ i, (6 * Q S i + 3 * U S i + 3 * D S i + 2 * L S i + E S i), map_add' := ⋯, map_smul' := ⋯ }
    S.val =
  0
  simp_all only [toSpecies_apply_eq, Fin.isValue, sum_SMSpecies_numberCharges_one, LinearMap.coe_mk,
    AddHom.coe_mk]S:(SMNoGrav 1).SolshQ:toSpeciesEquiv S.val 0 0 = 0hE:toSpeciesEquiv S.val 4 0 = 0⊢ 6 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
          3 * toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        3 * toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      2 * toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0
  have h1 := SU2Sol S.1.1S:(SMNoGrav 1).SolshQ:toSpeciesEquiv S.val 0 0 = 0hE:toSpeciesEquiv S.val 4 0 = 0h1:accSU2 S.val = 0⊢ 6 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
          3 * toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        3 * toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      2 * toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0
  have h2 := SU3Sol S.1.1S:(SMNoGrav 1).SolshQ:toSpeciesEquiv S.val 0 0 = 0hE:toSpeciesEquiv S.val 4 0 = 0h1:accSU2 S.val = 0h2:accSU3 S.val = 0⊢ 6 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
          3 * toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        3 * toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      2 * toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0
  simp only [accSU2, toSpecies_apply_eq, Fin.isValue, sum_SMSpecies_numberCharges_one,
    LinearMap.coe_mk, AddHom.coe_mk, accSU3] at h1 h2S:(SMNoGrav 1).SolshQ:toSpeciesEquiv S.val 0 0 = 0hE:toSpeciesEquiv S.val 4 0 = 0h1:3 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0h2:2 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ 6 * toSpeciesEquiv S.val 0 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
          3 * toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        3 * toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      2 * toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0
  erw [hQS:(SMNoGrav 1).SolshQ:toSpeciesEquiv S.val 0 0 = 0hE:toSpeciesEquiv S.val 4 0 = 0h1:3 * 0 + toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ = 0h2:2 * 0 + toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ 6 * 0 + 3 * toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        3 * toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      2 * toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0]S:(SMNoGrav 1).SolshQ:toSpeciesEquiv S.val 0 0 = 0hE:toSpeciesEquiv S.val 4 0 = 0h1:3 * 0 + toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ = 0h2:2 * 0 + toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ 6 * 0 + 3 * toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        3 * toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      2 * toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 4 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0 at h1 h2 ⊢
  erw [hES:(SMNoGrav 1).SolshQ:toSpeciesEquiv S.val 0 0 = 0hE:toSpeciesEquiv S.val 4 0 = 0h1:3 * 0 + toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ = 0h2:2 * 0 + toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ 6 * 0 + 3 * toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        3 * toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      2 * toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    0 =
  0]S:(SMNoGrav 1).SolshQ:toSpeciesEquiv S.val 0 0 = 0hE:toSpeciesEquiv S.val 4 0 = 0h1:3 * 0 + toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ = 0h2:2 * 0 + toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ =
  0⊢ 6 * 0 + 3 * toSpeciesEquiv S.val 1 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
        3 * toSpeciesEquiv S.val 2 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
      2 * toSpeciesEquiv S.val 3 ⟨0, sum_SMSpecies_numberCharges_one._proof_1⟩ +
    0 =
  0
  linear_combination 2 * h1 + 3 * h2All goals completed! 🐙

For a set of 1-family SM charges satisfying all ACCs except the gravitational, if the Q charge is not zero then the charges satisfy the gravitational ACCs.


lemma accGrav_Q_ne_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0) :
    accGrav S.val = 0 := byS:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0⊢ accGrav S.val = 0
  have hE := E_zero_iff_Q_zero.mpr.mt hQS:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0hE:¬E S.val 0 = 0⊢ accGrav S.val = 0
  let S' := linearParametersQENeqZero.bijection.symm ⟨S.1.1, hQ, hE⟩S:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0hE:¬E S.val 0 = 0S':linearParametersQENeqZero := linearParametersQENeqZero.bijection.symm ⟨S.toLinSols, ⋯⟩⊢ accGrav S.val = 0
  have hC := cubeSol SS:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0hE:¬E S.val 0 = 0S':linearParametersQENeqZero := linearParametersQENeqZero.bijection.symm ⟨S.toLinSols, ⋯⟩hC:accCube S.val = 0⊢ accGrav S.val = 0
  have hS' := congrArg (fun S => S.val.val)
    (linearParametersQENeqZero.bijection.right_inv ⟨S.1.1, hQ, hE⟩)S:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0hE:¬E S.val 0 = 0S':linearParametersQENeqZero := linearParametersQENeqZero.bijection.symm ⟨S.toLinSols, ⋯⟩hC:accCube S.val = 0hS':(↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val =
  (↑⟨S.toLinSols, ⋯⟩).val⊢ accGrav S.val = 0
  change _ = S.val at hS'S:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0hE:¬E S.val 0 = 0S':linearParametersQENeqZero := linearParametersQENeqZero.bijection.symm ⟨S.toLinSols, ⋯⟩hC:accCube S.val = 0hS':(↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val = S.val⊢ accGrav S.val = 0
  rw [← hS'S:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0hE:¬E S.val 0 = 0S':linearParametersQENeqZero := linearParametersQENeqZero.bijection.symm ⟨S.toLinSols, ⋯⟩hC:accCube
    (↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val =
  0hS':(↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val = S.val⊢ accGrav
    (↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val =
  0S:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0hE:¬E S.val 0 = 0S':linearParametersQENeqZero := linearParametersQENeqZero.bijection.symm ⟨S.toLinSols, ⋯⟩hC:accCube
    (↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val =
  0hS':(↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val = S.val⊢ accGrav
    (↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val =
  0] at hC ⊢S:(SMNoGrav 1).SolshQ:Q S.val 0 ≠ 0hE:¬E S.val 0 = 0S':linearParametersQENeqZero := linearParametersQENeqZero.bijection.symm ⟨S.toLinSols, ⋯⟩hC:accCube
    (↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val =
  0hS':(↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val = S.val⊢ accGrav
    (↑(linearParametersQENeqZero.bijection.toFun (linearParametersQENeqZero.bijection.invFun ⟨S.toLinSols, ⋯⟩))).val =
  0
  exact S'.grav_of_cubic hCAll goals completed! 🐙

Any solution to the 1-family ACCs without gravity satisfies the gravitational ACC.

theorem accGravSatisfied {S : (SMNoGrav 1).Sols} :
    accGrav S.val = 0 :=
  (em _).elim accGrav_Q_zero accGrav_Q_ne_zero