OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRetainedRoutes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Assign an actual short lattice path to every retained physical interaction.

  1. theorem OAI.ContinuumCoulomb.qmaGridNeighborIndex_opposite line 12
  2. theorem OAI.ContinuumCoulomb.qmaMovedPort_local line 22
  3. def OAI.ContinuumCoulomb.QMAPortRouteData.RoutingAllowed line 32
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.geometry_route_exists line 40
  5. def OAI.ContinuumCoulomb.QMAPortRouteData.retainedRoute line 81
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.retainedRoute_spec line 86