OAI/MathematicalPhysics/BFSS/NormalPotential.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Massive zero relations and positive normal quadratic forms.

  1. def OAI.BFSSQuantum.AlgebraData.spatialColor line 15
  2. lemma OAI.BFSSQuantum.AlgebraData.spatialColor_add line 18
  3. lemma OAI.BFSSQuantum.AlgebraData.spatialColor_smul line 20
  4. lemma OAI.BFSSQuantum.AlgebraData.colorEmbed_normSq line 23
  5. lemma OAI.BFSSQuantum.AlgebraData.colorEmbed_spatial line 28
  6. def OAI.BFSSQuantum.AlgebraData.ZeroRelations line 31
  7. lemma OAI.BFSSQuantum.AlgebraData.residual_normSq line 37
  8. theorem OAI.BFSSQuantum.AlgebraData.potential_zero_relations line 45
  9. def OAI.BFSSQuantum.AlgebraData.bracketLinearization line 59
  10. def OAI.BFSSQuantum.AlgebraData.cyclicLinearization line 63
  11. def OAI.BFSSQuantum.AlgebraData.normalQuadratic line 66
  12. lemma OAI.BFSSQuantum.AlgebraData.normalQuadratic_nonneg line 74
  13. lemma OAI.BFSSQuantum.AlgebraData.normalQuadratic_zero_components line 78
  14. def OAI.BFSSQuantum.AlgebraData.gaugeDivergence line 103
  15. lemma OAI.BFSSQuantum.AlgebraData.colorLie_zero_left line 106
  16. lemma OAI.BFSSQuantum.AlgebraData.colorLie_zero_right line 109
  17. lemma OAI.BFSSQuantum.AlgebraData.gaugeDivergence_first_three line 113
  18. theorem OAI.BFSSQuantum.AlgebraData.normalQuadratic_zero_of_normal line 142
  19. lemma OAI.BFSSNormal.positive_quadratic_lower line 187