OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingListBlock.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

The nine ordinary exchange interactions in a crossing gadget, serialized in a fixed order. Every endpoint and rational coefficient is computed literally.

  1. abbrev OAI.ContinuumCoulomb.QuantumCrossingListBlock.Sites line 13
  2. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.sitesCode line 14
  3. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.site line 16
  4. abbrev OAI.ContinuumCoulomb.QuantumCrossingListBlock.Crossing line 17
  5. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.crossingCode line 18
  6. abbrev OAI.ContinuumCoulomb.QuantumCrossingListBlock.Parameters line 19
  7. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.parametersCode line 20
  8. abbrev OAI.ContinuumCoulomb.QuantumCrossingListBlock.Input line 21
  9. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.inputCode line 22
  10. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.base line 24
  11. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.left line 26
  12. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.right line 29
  13. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.coefficient line 32
  14. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.bond line 35
  15. def OAI.ContinuumCoulomb.QuantumCrossingListBlock.block line 36
  16. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.crossingProgram line 38
  17. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.sitesProgram line 40
  18. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.siteProgram line 42
  19. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.radiusProgram line 56
  20. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.baseProgram line 58
  21. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.nextProgram line 65
  22. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.leftProgram line 67
  23. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.rightProgram line 87
  24. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.coefficientsProgram line 107
  25. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.coefficientProgram line 111
  26. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.bondProgram line 132
  27. opaque OAI.ContinuumCoulomb.QuantumCrossingListBlock.blockProgram line 134
  28. theorem OAI.ContinuumCoulomb.QuantumCrossingListBlock.block_length line 137
  29. theorem OAI.ContinuumCoulomb.QuantumCrossingListBlock.block_bounded line 139
  30. theorem OAI.ContinuumCoulomb.QuantumCrossingListBlock.block_noLoops line 150