OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingOutputRoutes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every edge of the actual simultaneous crossing output has a short permitted lattice route with the exact physical endpoints.

  1. abbrev OAI.ContinuumCoulomb.QMAPortRouteData.crossingOutput line 17
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingOutput_route_exists line 20
  3. def OAI.ContinuumCoulomb.QMAPortRouteData.crossingOutputRoute line 53
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingOutputRoute_spec line 58