HepLean Documentation

HepLean.AnomalyCancellation.PureU1.Odd.Parameterization

Parameterization in odd case #

Given maps g : Fin n → ℚ, f : Fin n → ℚ and a : ℚ we form a solution to the anomaly equations. We show that every solution can be got in this way, up to permutation, unless it is zero.

The main reference is:

source
def PureU1.Odd.parameterizationAsLinear {n : ℕ} (g f : Fin n → ℚ) (a : ℚ) :
(PureU1 (2 * n + 1)).LinSols

Given a g f : Fin n → ℚ and a a : ℚ we form a linear solution. We will later show that this can be extended to a complete solution.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PureU1.Odd.parameterizationAsLinear_val {n : ℕ} (g f : Fin n → ℚ) (a : ℚ) :
    (PureU1.Odd.parameterizationAsLinear g f a).val = a • (((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P! f)) (PureU1.VectorLikeOddPlane.P! f)) (PureU1.VectorLikeOddPlane.P g) • PureU1.VectorLikeOddPlane.P g + -((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P! f) • PureU1.VectorLikeOddPlane.P! f)
    source
    theorem PureU1.Odd.parameterizationCharge_cube {n : ℕ} (g f : Fin n → ℚ) (a : ℚ) :
    (PureU1.accCube (2 * n + 1)) (PureU1.Odd.parameterizationAsLinear g f a).val = 0

    The parameterization satisfies the cubic ACC.

    source
    def PureU1.Odd.parameterization {n : ℕ} (g f : Fin n → ℚ) (a : ℚ) :
    (PureU1 (2 * n + 1)).Sols

    Given a g f : Fin n → ℚ and a a : ℚ we form a solution.

    Equations
    Instances For
      source
      theorem PureU1.Odd.anomalyFree_param {n : ℕ} {S : (PureU1 (2 * n + 1)).Sols} (g f : Fin n → ℚ) (hS : S.val = PureU1.VectorLikeOddPlane.P g + PureU1.VectorLikeOddPlane.P! f) :
      ((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P! f) = -((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P! f)) (PureU1.VectorLikeOddPlane.P! f)) (PureU1.VectorLikeOddPlane.P g)
      source
      def PureU1.Odd.GenericCase {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) :
      Prop

      A proposition on a solution which is true if accCubeTriLinSymm (P g, P g, P! f) ≠ 0. In this case our parameterization above will be able to recover this point.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem PureU1.Odd.genericCase_exists {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n.succ → ℚ), S.val = PureU1.VectorLikeOddPlane.P g + PureU1.VectorLikeOddPlane.P! f ∧ ((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P! f) ≠ 0) :
        PureU1.Odd.GenericCase S
        source
        def PureU1.Odd.SpecialCase {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) :
        Prop

        A proposition on a solution which is true if accCubeTriLinSymm (P g, P g, P! f) ≠ 0. In this case we will show that S is zero if it is true for all permutations.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem PureU1.Odd.specialCase_exists {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n.succ → ℚ), S.val = PureU1.VectorLikeOddPlane.P g + PureU1.VectorLikeOddPlane.P! f ∧ ((PureU1.accCubeTriLinSymm (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P g)) (PureU1.VectorLikeOddPlane.P! f) = 0) :
          PureU1.Odd.SpecialCase S
          source
          theorem PureU1.Odd.generic_or_special {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).Sols) :
          PureU1.Odd.GenericCase S ∨ PureU1.Odd.SpecialCase S
          source
          theorem PureU1.Odd.generic_case {n : ℕ} {S : (PureU1 (2 * n.succ + 1)).Sols} (h : PureU1.Odd.GenericCase S) :
          ∃ (g : Fin n.succ → ℚ) (f : Fin n.succ → ℚ) (a : ℚ), S = PureU1.Odd.parameterization g f a
          source
          theorem PureU1.Odd.special_case_lineInCubic {n : ℕ} {S : (PureU1 (2 * n.succ + 1)).Sols} (h : PureU1.Odd.SpecialCase S) :
          PureU1.Odd.LineInCubic S.toLinSols
          source
          theorem PureU1.Odd.special_case_lineInCubic_perm {n : ℕ} {S : (PureU1 (2 * n.succ + 1)).Sols} (h : ∀ (M : (PureU1.FamilyPermutations (2 * n.succ + 1)).group), PureU1.Odd.SpecialCase ((MulAction.toFun (PureU1.FamilyPermutations (2 * n.succ + 1)).group (PureU1 (2 * n.succ + 1)).Sols) S M)) :
          PureU1.Odd.LineInCubicPerm S.toLinSols
          source
          theorem PureU1.Odd.special_case {n : ℕ} {S : (PureU1 (2 * n.succ.succ + 1)).Sols} (h : ∀ (M : (PureU1.FamilyPermutations (2 * n.succ.succ + 1)).group), PureU1.Odd.SpecialCase ((MulAction.toFun (PureU1.FamilyPermutations (2 * n.succ.succ + 1)).group (PureU1 (2 * n.succ.succ + 1)).Sols) S M)) :
          S.toLinSols = 0