OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingSelectProgram.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Select crossing interactions directly from the finite bond tape. Both orientations contribute to each rational coupling; every other bond is retained. All scans are literal polynomial programs.

  1. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.hits line 15
  2. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.terminalPair line 17
  3. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.pairs line 19
  4. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.contribution line 21
  5. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.weight line 22
  6. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.keep line 23
  7. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retained line 24
  8. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.crossing line 25
  9. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.crossings line 27
  10. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.hitsProgram line 29
  11. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.terminalProgram line 39
  12. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.pairsProgram line 49
  13. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.contributionProgram line 56
  14. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.weightProgram line 63
  15. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.keepProgram line 74
  16. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retainedProgram line 84
  17. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.crossingProgram line 102
  18. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.crossingsProgram line 109
  19. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.hits_iff line 113
  20. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.keep_iff line 117
  21. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retained_mem line 121
  22. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retained_bounded line 125
  23. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.retained_noLoops line 130
  24. abbrev OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.Input line 135
  25. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.inputCode line 136
  26. def OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.value line 138
  27. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.precisionProgram line 142
  28. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.packetProgram line 143
  29. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.sitesProgram line 147
  30. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.bondsProgram line 150
  31. opaque OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.program line 153