OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListPathProgram.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Literal three-edge output for one selected path subdivision. Fresh spin labels are assigned in the input list order; both path parities are supported.

  1. abbrev OAI.ContinuumCoulomb.QuantumListPathProgram.Parameters line 14
  2. def OAI.ContinuumCoulomb.QuantumListPathProgram.parametersCode line 15
  3. abbrev OAI.ContinuumCoulomb.QuantumListPathProgram.Input line 17
  4. def OAI.ContinuumCoulomb.QuantumListPathProgram.inputCode line 18
  5. def OAI.ContinuumCoulomb.QuantumListPathProgram.left line 21
  6. def OAI.ContinuumCoulomb.QuantumListPathProgram.right line 23
  7. def OAI.ContinuumCoulomb.QuantumListPathProgram.coefficient line 26
  8. def OAI.ContinuumCoulomb.QuantumListPathProgram.bond line 28
  9. def OAI.ContinuumCoulomb.QuantumListPathProgram.block line 30
  10. def OAI.ContinuumCoulomb.QuantumListPathProgram.offset line 31
  11. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.countProgram line 33
  12. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.indexProgram line 36
  13. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.sourceProgram line 38
  14. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.baseProgram line 40
  15. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.nextProgram line 43
  16. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.parityProgram line 45
  17. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.leftProgram line 49
  18. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.rightProgram line 58
  19. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.coefficientProgram line 68
  20. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.bondProgram line 78
  21. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.blockProgram line 80
  22. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.offsetProgram line 82
  23. abbrev OAI.ContinuumCoulomb.QuantumListPathProgram.FamilyInput line 84
  24. def OAI.ContinuumCoulomb.QuantumListPathProgram.familyCode line 85
  25. def OAI.ContinuumCoulomb.QuantumListPathProgram.indexed line 86
  26. def OAI.ContinuumCoulomb.QuantumListPathProgram.family line 88
  27. def OAI.ContinuumCoulomb.QuantumListPathProgram.familyOffset line 90
  28. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.indexedProgram line 93
  29. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.familyProgram line 102
  30. opaque OAI.ContinuumCoulomb.QuantumListPathProgram.familyOffsetProgram line 109
  31. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.block_length line 117
  32. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.block_bounded line 119
  33. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.block_noLoops line 127
  34. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.indexed_mem line 134
  35. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.family_bounded line 143
  36. theorem OAI.ContinuumCoulomb.QuantumListPathProgram.family_noLoops line 152