OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialCrossingProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

A literal composition from the prepared spatial input to the crossing Hamiltonian, its physical positions, and the finite routing permission table.

  1. abbrev OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.Input line 18
  2. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.inputCode line 19
  3. abbrev OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.Output line 20
  4. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.outputCode line 21
  5. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.coarse line 25
  6. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.cells line 28
  7. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.table line 29
  8. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.oldPositions line 30
  9. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.oldPacket line 31
  10. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.sites line 34
  11. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.crossingInput line 36
  12. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.positions line 38
  13. def OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.value line 40
  14. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.coarseProgram line 43
  15. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.cellsProgram line 48
  16. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.tableProgram line 51
  17. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.oldPositionsProgram line 54
  18. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.oldPacketProgram line 60
  19. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.sitesProgram line 73
  20. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.crossingInputProgram line 77
  21. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.positionsProgram line 82
  22. opaque OAI.ContinuumCoulomb.QuantumSpatialCrossingProgram.program line 86