OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourSpinCertificate.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Fixed rational certificates for the one-spin excited columns.

  1. theorem OAI.ContinuumCoulomb.qmaFourPenaltyRational_mulVec line 12
  2. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal00 line 24
  3. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen00 line 33
  4. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal01 line 45
  5. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen01 line 54
  6. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal02 line 66
  7. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen02 line 75
  8. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal10 line 87
  9. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen10 line 96
  10. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal11 line 108
  11. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen11 line 117
  12. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal12 line 129
  13. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen12 line 138
  14. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal20 line 150
  15. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen20 line 159
  16. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal21 line 171
  17. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen21 line 180
  18. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal22 line 192
  19. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen22 line 201
  20. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal30 line 213
  21. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen30 line 222
  22. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal31 line 234
  23. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen31 line 243
  24. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal32 line 255
  25. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen32 line 264
  26. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_orthogonal line 276
  27. theorem OAI.ContinuumCoulomb.qmaFourSpinRawAction_eigen line 296