PhysLean Documentation

PhysLean.QFT.AnomalyCancellation.SMNu.PlusU1.QuadSol

Properties of Quad Sols for SM with RHN #

We give a series of properties held by solutions to the quadratic equation.

In particular given a quad solution we define a map from linear solutions to quadratic solutions and show that it is a surjection. The main reference for this is:

source
theorem SMRHN.PlusU1.QuadSol.add_AFL_quad {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) (a b : ℚ) :
SMνACCs.accQuad (a • S.val + b • C.val) = a * (a * SMνACCs.accQuad S.val + 2 * b * (SMνACCs.quadBiLin S.val) C.val)
source
def SMRHN.PlusU1.QuadSol.α₁ {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) :
ℚ

A helper function for what comes later.

Equations
Instances For
    source
    def SMRHN.PlusU1.QuadSol.α₂ {n : ℕ} (S : (PlusU1 n).LinSols) :
    ℚ

    A helper function for what comes later.

    Equations
    Instances For
      source
      theorem SMRHN.PlusU1.QuadSol.α₂_AFQ {n : ℕ} (S : (PlusU1 n).QuadSols) :
      α₂ S.toLinSols = 0
      source
      theorem SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂ {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) :
      SMνACCs.accQuad (α₁ C S • S + α₂ S • C.toLinSols).val = 0
      source
      theorem SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) (h1 : α₁ C S = 0) (h2 : α₂ S = 0) (a b : ℚ) :
      SMνACCs.accQuad (a • S + b • C.toLinSols).val = 0
      source
      def SMRHN.PlusU1.QuadSol.genericToQuad {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) :
      (PlusU1 n).QuadSols

      The construction of a QuadSol from a LinSols in the generic case.

      Equations
      Instances For
        source
        theorem SMRHN.PlusU1.QuadSol.genericToQuad_on_quad {n : ℕ} (C S : (PlusU1 n).QuadSols) :
        genericToQuad C S.toLinSols = α₁ C S.toLinSols • S
        source
        theorem SMRHN.PlusU1.QuadSol.genericToQuad_neq_zero {n : ℕ} (C S : (PlusU1 n).QuadSols) (h : α₁ C S.toLinSols ≠ 0) :
        (α₁ C S.toLinSols)⁻¹ • genericToQuad C S.toLinSols = S
        source
        def SMRHN.PlusU1.QuadSol.specialToQuad {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) (a b : ℚ) (h1 : α₁ C S = 0) (h2 : α₂ S = 0) :
        (PlusU1 n).QuadSols

        The construction of a QuadSol from a LinSols in the special case when α₁ C S = 0 and α₂ S = 0.

        Equations
        Instances For
          source
          theorem SMRHN.PlusU1.QuadSol.special_on_quad {n : ℕ} (C S : (PlusU1 n).QuadSols) (h1 : α₁ C S.toLinSols = 0) :
          specialToQuad C S.toLinSols 1 0 h1 ⋯ = S
          source
          def SMRHN.PlusU1.QuadSol.toQuad {n : ℕ} (C : (PlusU1 n).QuadSols) :
          (PlusU1 n).LinSols × ℚ × ℚ → (PlusU1 n).QuadSols

          The construction of a QuadSols from a LinSols and two rationals taking account of the generic and special cases. This function is a surjection.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def SMRHN.PlusU1.QuadSol.toQuadInv {n : ℕ} (C : (PlusU1 n).QuadSols) :
            (PlusU1 n).QuadSols → (PlusU1 n).LinSols × ℚ × ℚ

            A function from QuadSols to LinSols × ℚ × ℚ which is a right inverse to toQuad.

            Equations
            Instances For
              source
              theorem SMRHN.PlusU1.QuadSol.toQuadInv_fst {n : ℕ} (C S : (PlusU1 n).QuadSols) :
              (toQuadInv C S).1 = S.toLinSols
              source
              theorem SMRHN.PlusU1.QuadSol.toQuadInv_α₁_α₂ {n : ℕ} (C S : (PlusU1 n).QuadSols) :
              α₁ C S.toLinSols = 0 ↔ α₁ C (toQuadInv C S).1 = 0 ∧ α₂ (toQuadInv C S).1 = 0
              source
              theorem SMRHN.PlusU1.QuadSol.toQuadInv_special {n : ℕ} (C S : (PlusU1 n).QuadSols) (h : α₁ C S.toLinSols = 0) :
              specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = S
              source
              theorem SMRHN.PlusU1.QuadSol.toQuadInv_generic {n : ℕ} (C S : (PlusU1 n).QuadSols) (h : α₁ C S.toLinSols ≠ 0) :
              (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = S
              source
              theorem SMRHN.PlusU1.QuadSol.toQuad_rightInverse {n : ℕ} (C : (PlusU1 n).QuadSols) :
              Function.RightInverse (toQuadInv C) (toQuad C)
              source
              theorem SMRHN.PlusU1.QuadSol.toQuad_surjective {n : ℕ} (C : (PlusU1 n).QuadSols) :
              Function.Surjective (toQuad C)