OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPlanarTapeProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Merge the physical crossing bonds and compute the short planar route for every remaining pair of endpoints from the finite permission table.

  1. abbrev OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.Input line 14
  2. def OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.inputCode line 15
  3. abbrev OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.Output line 16
  4. def OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.outputCode line 17
  5. def OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.merged line 20
  6. def OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.routeInput line 21
  7. def OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.paths line 23
  8. def OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.value line 25
  9. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.packetProgram line 27
  10. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.positionsProgram line 32
  11. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.tableProgram line 37
  12. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.nProgram line 39
  13. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.bondsProgram line 41
  14. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.constantProgram line 45
  15. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.mergedProgram line 48
  16. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.routeInputProgram line 51
  17. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.routeProgram line 63
  18. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.mapPathsProgram line 67
  19. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.pathsProgram line 73
  20. opaque OAI.ContinuumCoulomb.QuantumPlanarTapeProgram.program line 77