OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathTable.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The finite lists of actual routes produce a routing table with exactly the permissions of the physical graph proof. Lists may use any complete edge order; this does not change a routing decision.

  1. def OAI.ContinuumCoulomb.QMAPortRouteData.listedVisits line 16
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.listedVisits_mem line 19
  3. abbrev OAI.ContinuumCoulomb.QuantumPathTable.Input line 33
  4. def OAI.ContinuumCoulomb.QuantumPathTable.inputCode line 34
  5. def OAI.ContinuumCoulomb.QuantumPathTable.inputVisits line 37
  6. def OAI.ContinuumCoulomb.QuantumPathTable.beforeCrossings line 39
  7. def OAI.ContinuumCoulomb.QuantumPathTable.compile line 41
  8. def OAI.ContinuumCoulomb.QuantumPathTable.compileProgram line 43
  9. theorem OAI.ContinuumCoulomb.QuantumPathTable.beforeCrossings_visits line 51
  10. theorem OAI.ContinuumCoulomb.QuantumPathTable.compile_crossings line 59
  11. theorem OAI.ContinuumCoulomb.QuantumPathTable.compile_allowed line 68