OAI/MathematicalPhysics/BFSS/GroundLine.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Irreducibility of negative modes and the unique normal fermion ground line.

  1. lemma OAI.BFSSQuantum.AlgebraData.thetaMode_zero line 16
  2. lemma OAI.BFSSQuantum.AlgebraData.thetaMode_add line 22
  3. lemma OAI.BFSSQuantum.AlgebraData.thetaMode_single line 29
  4. def OAI.BFSSQuantum.AlgebraData.NegativeFrequencyMode line 41
  5. theorem OAI.BFSSQuantum.AlgebraData.normal_negative_modes_irreducible line 45
  6. theorem OAI.BFSSQuantum.AlgebraData.normal_fermion_ground_line line 102