OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourGapCertificate.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

A rational positive factorization of the four-spin penalty above the singlet projection. Each fixed row is checked separately at default limits.

  1. def OAI.ContinuumCoulomb.qmaFourProjectionRational line 13
  2. def OAI.ContinuumCoulomb.qmaFourPenaltyRational line 16
  3. def OAI.ContinuumCoulomb.qmaFourWeight line 20
  4. def OAI.ContinuumCoulomb.qmaFourSymmetricWeights line 23
  5. def OAI.ContinuumCoulomb.qmaFourSymmetricRational line 25
  6. def OAI.ContinuumCoulomb.qmaFourGapRational line 28
  7. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row0 line 31
  8. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row1 line 39
  9. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row2 line 47
  10. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row3 line 55
  11. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row4 line 63
  12. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row5 line 71
  13. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row6 line 79
  14. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row7 line 87
  15. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row8 line 95
  16. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row9 line 103
  17. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row10 line 111
  18. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row11 line 119
  19. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row12 line 127
  20. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row13 line 135
  21. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row14 line 143
  22. theorem OAI.ContinuumCoulomb.qmaFourGapRational_row15 line 151
  23. theorem OAI.ContinuumCoulomb.qmaFourGapRational_factor line 159